author  hoelzl 
Thu, 09 Jun 2011 11:50:16 +0200  
changeset 43336  05aa7380f7fc 
parent 41959  b460124855b8 
child 44289  d81d09cdab9c 
permissions  rwrr 
41959  1 
(* Title: HOL/Ln.thy 
16959  2 
Author: Jeremy Avigad 
3 
*) 

4 

5 
header {* Properties of ln *} 

6 

7 
theory Ln 

8 
imports Transcendental 

9 
begin 

10 

11 
lemma exp_first_two_terms: "exp x = 1 + x + suminf (%n. 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

12 
inverse(fact (n+2)) * (x ^ (n+2)))" 
16959  13 
proof  
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

14 
have "exp x = suminf (%n. inverse(fact n) * (x ^ n))" 
19765  15 
by (simp add: exp_def) 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

16 
also from summable_exp have "... = (SUM n::nat : {0..<2}. 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

17 
inverse(fact n) * (x ^ n)) + suminf (%n. 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

18 
inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _") 
16959  19 
by (rule suminf_split_initial_segment) 
20 
also have "?a = 1 + x" 

21 
by (simp add: numerals) 

22 
finally show ?thesis . 

23 
qed 

24 

25 
lemma exp_tail_after_first_two_terms_summable: 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

26 
"summable (%n. inverse(fact (n+2)) * (x ^ (n+2)))" 
16959  27 
proof  
28 
note summable_exp 

29 
thus ?thesis 

30 
by (frule summable_ignore_initial_segment) 

31 
qed 

32 

33 
lemma aux1: assumes a: "0 <= x" and b: "x <= 1" 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

34 
shows "inverse (fact ((n::nat) + 2)) * x ^ (n + 2) <= (x^2/2) * ((1/2)^n)" 
16959  35 
proof (induct n) 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

36 
show "inverse (fact ((0::nat) + 2)) * x ^ (0 + 2) <= 
16959  37 
x ^ 2 / 2 * (1 / 2) ^ 0" 
23482  38 
by (simp add: real_of_nat_Suc power2_eq_square) 
16959  39 
next 
32038  40 
fix n :: nat 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

41 
assume c: "inverse (fact (n + 2)) * x ^ (n + 2) 
16959  42 
<= x ^ 2 / 2 * (1 / 2) ^ n" 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

43 
show "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) 
16959  44 
<= x ^ 2 / 2 * (1 / 2) ^ Suc n" 
45 
proof  

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

46 
have "inverse(fact (Suc n + 2)) <= (1/2) * inverse (fact (n+2))" 
16959  47 
proof  
48 
have "Suc n + 2 = Suc (n + 2)" by simp 

49 
then have "fact (Suc n + 2) = Suc (n + 2) * fact (n + 2)" 

50 
by simp 

51 
then have "real(fact (Suc n + 2)) = real(Suc (n + 2) * fact (n + 2))" 

52 
apply (rule subst) 

53 
apply (rule refl) 

54 
done 

55 
also have "... = real(Suc (n + 2)) * real(fact (n + 2))" 

56 
by (rule real_of_nat_mult) 

57 
finally have "real (fact (Suc n + 2)) = 

58 
real (Suc (n + 2)) * real (fact (n + 2))" . 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

59 
then have "inverse(fact (Suc n + 2)) = 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

60 
inverse(Suc (n + 2)) * inverse(fact (n + 2))" 
16959  61 
apply (rule ssubst) 
62 
apply (rule inverse_mult_distrib) 

63 
done 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

64 
also have "... <= (1/2) * inverse(fact (n + 2))" 
16959  65 
apply (rule mult_right_mono) 
66 
apply (subst inverse_eq_divide) 

67 
apply simp 

68 
apply (rule inv_real_of_nat_fact_ge_zero) 

69 
done 

70 
finally show ?thesis . 

71 
qed 

72 
moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)" 

73 
apply (simp add: mult_compare_simps) 

41550  74 
apply (simp add: assms) 
16959  75 
apply (subgoal_tac "0 <= x * (x * x^n)") 
76 
apply force 

77 
apply (rule mult_nonneg_nonneg, rule a)+ 

78 
apply (rule zero_le_power, rule a) 

79 
done 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

80 
ultimately have "inverse (fact (Suc n + 2)) * x ^ (Suc n + 2) <= 
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

81 
(1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)" 
16959  82 
apply (rule mult_mono) 
83 
apply (rule mult_nonneg_nonneg) 

84 
apply simp 

85 
apply (subst inverse_nonnegative_iff_nonnegative) 

27483
7c58324cd418
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
huffman
parents:
25875
diff
changeset

86 
apply (rule real_of_nat_ge_zero) 
16959  87 
apply (rule zero_le_power) 
23441  88 
apply (rule a) 
16959  89 
done 
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

90 
also have "... = 1 / 2 * (inverse (fact (n + 2)) * x ^ (n + 2))" 
16959  91 
by simp 
92 
also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)" 

93 
apply (rule mult_left_mono) 

41550  94 
apply (rule c) 
16959  95 
apply simp 
96 
done 

97 
also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)" 

98 
by auto 

99 
also have "(1::real) / 2 * (1 / 2) ^ n = (1 / 2) ^ (Suc n)" 

30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant typespecific versions of power_Suc
huffman
parents:
29667
diff
changeset

100 
by (rule power_Suc [THEN sym]) 
16959  101 
finally show ?thesis . 
102 
qed 

103 
qed 

104 

20692  105 
lemma aux2: "(%n. (x::real) ^ 2 / 2 * (1 / 2) ^ n) sums x^2" 
16959  106 
proof  
20692  107 
have "(%n. (1 / 2::real)^n) sums (1 / (1  (1/2)))" 
16959  108 
apply (rule geometric_sums) 
22998  109 
by (simp add: abs_less_iff) 
16959  110 
also have "(1::real) / (1  1/2) = 2" 
111 
by simp 

20692  112 
finally have "(%n. (1 / 2::real)^n) sums 2" . 
16959  113 
then have "(%n. x ^ 2 / 2 * (1 / 2) ^ n) sums (x^2 / 2 * 2)" 
114 
by (rule sums_mult) 

115 
also have "x^2 / 2 * 2 = x^2" 

116 
by simp 

117 
finally show ?thesis . 

118 
qed 

119 

23114  120 
lemma exp_bound: "0 <= (x::real) ==> x <= 1 ==> exp x <= 1 + x + x^2" 
16959  121 
proof  
122 
assume a: "0 <= x" 

123 
assume b: "x <= 1" 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

124 
have c: "exp x = 1 + x + suminf (%n. inverse(fact (n+2)) * 
16959  125 
(x ^ (n+2)))" 
126 
by (rule exp_first_two_terms) 

40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

127 
moreover have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= x^2" 
16959  128 
proof  
40864
4abaaadfdaf2
moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents:
36777
diff
changeset

129 
have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <= 
16959  130 
suminf (%n. (x^2/2) * ((1/2)^n))" 
131 
apply (rule summable_le) 

41550  132 
apply (auto simp only: aux1 a b) 
16959  133 
apply (rule exp_tail_after_first_two_terms_summable) 
134 
by (rule sums_summable, rule aux2) 

135 
also have "... = x^2" 

136 
by (rule sums_unique [THEN sym], rule aux2) 

137 
finally show ?thesis . 

138 
qed 

139 
ultimately show ?thesis 

140 
by auto 

141 
qed 

142 

23114  143 
lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x  x^2) <= 1 + x" 
16959  144 
proof  
145 
assume a: "0 <= x" and b: "x <= 1" 

146 
have "exp (x  x^2) = exp x / exp (x^2)" 

147 
by (rule exp_diff) 

148 
also have "... <= (1 + x + x^2) / exp (x ^2)" 

149 
apply (rule divide_right_mono) 

150 
apply (rule exp_bound) 

151 
apply (rule a, rule b) 

152 
apply simp 

153 
done 

154 
also have "... <= (1 + x + x^2) / (1 + x^2)" 

155 
apply (rule divide_left_mono) 

17013
74bc935273ea
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
avigad
parents:
16963
diff
changeset

156 
apply (auto simp add: exp_ge_add_one_self_aux) 
16959  157 
apply (rule add_nonneg_nonneg) 
41550  158 
using a apply auto 
16959  159 
apply (rule mult_pos_pos) 
160 
apply auto 

161 
apply (rule add_pos_nonneg) 

162 
apply auto 

163 
done 

164 
also from a have "... <= 1 + x" 

41550  165 
by (simp add: field_simps zero_compare_simps) 
16959  166 
finally show ?thesis . 
167 
qed 

168 

169 
lemma ln_one_plus_pos_lower_bound: "0 <= x ==> x <= 1 ==> 

170 
x  x^2 <= ln (1 + x)" 

171 
proof  

172 
assume a: "0 <= x" and b: "x <= 1" 

173 
then have "exp (x  x^2) <= 1 + x" 

174 
by (rule aux4) 

175 
also have "... = exp (ln (1 + x))" 

176 
proof  

177 
from a have "0 < 1 + x" by auto 

178 
thus ?thesis 

179 
by (auto simp only: exp_ln_iff [THEN sym]) 

180 
qed 

181 
finally have "exp (x  x ^ 2) <= exp (ln (1 + x))" . 

182 
thus ?thesis by (auto simp only: exp_le_cancel_iff) 

183 
qed 

184 

185 
lemma ln_one_minus_pos_upper_bound: "0 <= x ==> x < 1 ==> ln (1  x) <=  x" 

186 
proof  

187 
assume a: "0 <= (x::real)" and b: "x < 1" 

188 
have "(1  x) * (1 + x + x^2) = (1  x^3)" 

29667  189 
by (simp add: algebra_simps power2_eq_square power3_eq_cube) 
16959  190 
also have "... <= 1" 
25875  191 
by (auto simp add: a) 
16959  192 
finally have "(1  x) * (1 + x + x ^ 2) <= 1" . 
193 
moreover have "0 < 1 + x + x^2" 

194 
apply (rule add_pos_nonneg) 

41550  195 
using a apply auto 
16959  196 
done 
197 
ultimately have "1  x <= 1 / (1 + x + x^2)" 

198 
by (elim mult_imp_le_div_pos) 

199 
also have "... <= 1 / exp x" 

200 
apply (rule divide_left_mono) 

201 
apply (rule exp_bound, rule a) 

41550  202 
using a b apply auto 
16959  203 
apply (rule mult_pos_pos) 
204 
apply (rule add_pos_nonneg) 

205 
apply auto 

206 
done 

207 
also have "... = exp (x)" 

36777
be5461582d0f
avoid using realspecific versions of generic lemmas
huffman
parents:
33667
diff
changeset

208 
by (auto simp add: exp_minus divide_inverse) 
16959  209 
finally have "1  x <= exp ( x)" . 
210 
also have "1  x = exp (ln (1  x))" 

211 
proof  

212 
have "0 < 1  x" 

213 
by (insert b, auto) 

214 
thus ?thesis 

215 
by (auto simp only: exp_ln_iff [THEN sym]) 

216 
qed 

217 
finally have "exp (ln (1  x)) <= exp ( x)" . 

218 
thus ?thesis by (auto simp only: exp_le_cancel_iff) 

219 
qed 

220 

221 
lemma aux5: "x < 1 ==> ln(1  x) =  ln(1 + x / (1  x))" 

222 
proof  

223 
assume a: "x < 1" 

224 
have "ln(1  x) =  ln(1 / (1  x))" 

225 
proof  

226 
have "ln(1  x) =  ( ln (1  x))" 

227 
by auto 

228 
also have " ln(1  x) = ln 1  ln(1  x)" 

229 
by simp 

230 
also have "... = ln(1 / (1  x))" 

231 
apply (rule ln_div [THEN sym]) 

232 
by (insert a, auto) 

233 
finally show ?thesis . 

234 
qed 

23482  235 
also have " 1 / (1  x) = 1 + x / (1  x)" using a by(simp add:field_simps) 
16959  236 
finally show ?thesis . 
237 
qed 

238 

239 
lemma ln_one_minus_pos_lower_bound: "0 <= x ==> x <= (1 / 2) ==> 

240 
 x  2 * x^2 <= ln (1  x)" 

241 
proof  

242 
assume a: "0 <= x" and b: "x <= (1 / 2)" 

243 
from b have c: "x < 1" 

244 
by auto 

245 
then have "ln (1  x) =  ln (1 + x / (1  x))" 

246 
by (rule aux5) 

247 
also have " (x / (1  x)) <= ..." 

248 
proof  

249 
have "ln (1 + x / (1  x)) <= x / (1  x)" 

250 
apply (rule ln_add_one_self_le_self) 

251 
apply (rule divide_nonneg_pos) 

252 
by (insert a c, auto) 

253 
thus ?thesis 

254 
by auto 

255 
qed 

256 
also have " (x / (1  x)) = x / (1  x)" 

257 
by auto 

258 
finally have d: " x / (1  x) <= ln (1  x)" . 

41550  259 
have "0 < 1  x" using a b by simp 
23482  260 
hence e: "x  2 * x^2 <=  x / (1  x)" 
41550  261 
using mult_right_le_one_le[of "x*x" "2*x"] a b 
262 
by (simp add:field_simps power2_eq_square) 

16959  263 
from e d show " x  2 * x^2 <= ln (1  x)" 
264 
by (rule order_trans) 

265 
qed 

266 

23114  267 
lemma exp_ge_add_one_self [simp]: "1 + (x::real) <= exp x" 
16959  268 
apply (case_tac "0 <= x") 
17013
74bc935273ea
renamed exp_ge_add_one_self2 to exp_ge_add_one_self
avigad
parents:
16963
diff
changeset

269 
apply (erule exp_ge_add_one_self_aux) 
16959  270 
apply (case_tac "x <= 1") 
271 
apply (subgoal_tac "1 + x <= 0") 

272 
apply (erule order_trans) 

273 
apply simp 

274 
apply simp 

275 
apply (subgoal_tac "1 + x = exp(ln (1 + x))") 

276 
apply (erule ssubst) 

277 
apply (subst exp_le_cancel_iff) 

278 
apply (subgoal_tac "ln (1  ( x)) <=  ( x)") 

279 
apply simp 

280 
apply (rule ln_one_minus_pos_upper_bound) 

281 
apply auto 

282 
done 

283 

284 
lemma ln_add_one_self_le_self2: "1 < x ==> ln(1 + x) <= x" 

285 
apply (subgoal_tac "x = ln (exp x)") 

286 
apply (erule ssubst)back 

287 
apply (subst ln_le_cancel_iff) 

288 
apply auto 

289 
done 

290 

291 
lemma abs_ln_one_plus_x_minus_x_bound_nonneg: 

292 
"0 <= x ==> x <= 1 ==> abs(ln (1 + x)  x) <= x^2" 

293 
proof  

23441  294 
assume x: "0 <= x" 
41550  295 
assume x1: "x <= 1" 
23441  296 
from x have "ln (1 + x) <= x" 
16959  297 
by (rule ln_add_one_self_le_self) 
298 
then have "ln (1 + x)  x <= 0" 

299 
by simp 

300 
then have "abs(ln(1 + x)  x) =  (ln(1 + x)  x)" 

301 
by (rule abs_of_nonpos) 

302 
also have "... = x  ln (1 + x)" 

303 
by simp 

304 
also have "... <= x^2" 

305 
proof  

41550  306 
from x x1 have "x  x^2 <= ln (1 + x)" 
16959  307 
by (intro ln_one_plus_pos_lower_bound) 
308 
thus ?thesis 

309 
by simp 

310 
qed 

311 
finally show ?thesis . 

312 
qed 

313 

314 
lemma abs_ln_one_plus_x_minus_x_bound_nonpos: 

315 
"(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x)  x) <= 2 * x^2" 

316 
proof  

41550  317 
assume a: "(1 / 2) <= x" 
318 
assume b: "x <= 0" 

16959  319 
have "abs(ln (1 + x)  x) = x  ln(1  (x))" 
320 
apply (subst abs_of_nonpos) 

321 
apply simp 

322 
apply (rule ln_add_one_self_le_self2) 

41550  323 
using a apply auto 
16959  324 
done 
325 
also have "... <= 2 * x^2" 

326 
apply (subgoal_tac " (x)  2 * (x)^2 <= ln (1  (x))") 

29667  327 
apply (simp add: algebra_simps) 
16959  328 
apply (rule ln_one_minus_pos_lower_bound) 
41550  329 
using a b apply auto 
29667  330 
done 
16959  331 
finally show ?thesis . 
332 
qed 

333 

334 
lemma abs_ln_one_plus_x_minus_x_bound: 

335 
"abs x <= 1 / 2 ==> abs(ln (1 + x)  x) <= 2 * x^2" 

336 
apply (case_tac "0 <= x") 

337 
apply (rule order_trans) 

338 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) 

339 
apply auto 

340 
apply (rule abs_ln_one_plus_x_minus_x_bound_nonpos) 

341 
apply auto 

342 
done 

343 

344 
lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)" 

345 
proof  

41550  346 
assume x: "exp 1 <= x" "x <= y" 
16959  347 
have a: "0 < x" and b: "0 < y" 
41550  348 
apply (insert x) 
23114  349 
apply (subgoal_tac "0 < exp (1::real)") 
16959  350 
apply arith 
351 
apply auto 

23114  352 
apply (subgoal_tac "0 < exp (1::real)") 
16959  353 
apply arith 
354 
apply auto 

355 
done 

356 
have "x * ln y  x * ln x = x * (ln y  ln x)" 

29667  357 
by (simp add: algebra_simps) 
16959  358 
also have "... = x * ln(y / x)" 
359 
apply (subst ln_div) 

360 
apply (rule b, rule a, rule refl) 

361 
done 

362 
also have "y / x = (x + (y  x)) / x" 

363 
by simp 

41550  364 
also have "... = 1 + (y  x) / x" using x a by (simp add: field_simps) 
16959  365 
also have "x * ln(1 + (y  x) / x) <= x * ((y  x) / x)" 
366 
apply (rule mult_left_mono) 

367 
apply (rule ln_add_one_self_le_self) 

368 
apply (rule divide_nonneg_pos) 

41550  369 
using x a apply simp_all 
16959  370 
done 
23482  371 
also have "... = y  x" using a by simp 
372 
also have "... = (y  x) * ln (exp 1)" by simp 

16959  373 
also have "... <= (y  x) * ln x" 
374 
apply (rule mult_left_mono) 

375 
apply (subst ln_le_cancel_iff) 

376 
apply force 

377 
apply (rule a) 

41550  378 
apply (rule x) 
379 
using x apply simp 

16959  380 
done 
381 
also have "... = y * ln x  x * ln x" 

382 
by (rule left_diff_distrib) 

383 
finally have "x * ln y <= y * ln x" 

384 
by arith 

41550  385 
then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps) 
386 
also have "... = y * (ln x / x)" by simp 

387 
finally show ?thesis using b by (simp add: field_simps) 

16959  388 
qed 
389 

43336  390 
lemma ln_le_minus_one: 
391 
"0 < x \<Longrightarrow> ln x \<le> x  1" 

392 
using exp_ge_add_one_self[of "ln x"] by simp 

393 

394 
lemma ln_eq_minus_one: 

395 
assumes "0 < x" "ln x = x  1" shows "x = 1" 

396 
proof  

397 
let "?l y" = "ln y  y + 1" 

398 
have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x  1)" 

399 
by (auto intro!: DERIV_intros) 

400 

401 
show ?thesis 

402 
proof (cases rule: linorder_cases) 

403 
assume "x < 1" 

404 
from dense[OF `x < 1`] obtain a where "x < a" "a < 1" by blast 

405 
from `x < a` have "?l x < ?l a" 

406 
proof (rule DERIV_pos_imp_increasing, safe) 

407 
fix y assume "x \<le> y" "y \<le> a" 

408 
with `0 < x` `a < 1` have "0 < 1 / y  1" "0 < y" 

409 
by (auto simp: field_simps) 

410 
with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z" 

411 
by auto 

412 
qed 

413 
also have "\<dots> \<le> 0" 

414 
using ln_le_minus_one `0 < x` `x < a` by (auto simp: field_simps) 

415 
finally show "x = 1" using assms by auto 

416 
next 

417 
assume "1 < x" 

418 
from dense[OF `1 < x`] obtain a where "1 < a" "a < x" by blast 

419 
from `a < x` have "?l x < ?l a" 

420 
proof (rule DERIV_neg_imp_decreasing, safe) 

421 
fix y assume "a \<le> y" "y \<le> x" 

422 
with `1 < a` have "1 / y  1 < 0" "0 < y" 

423 
by (auto simp: field_simps) 

424 
with D show "\<exists>z. DERIV ?l y :> z \<and> z < 0" 

425 
by blast 

426 
qed 

427 
also have "\<dots> \<le> 0" 

428 
using ln_le_minus_one `1 < a` by (auto simp: field_simps) 

429 
finally show "x = 1" using assms by auto 

430 
qed simp 

431 
qed 

432 

16959  433 
end 