equal
deleted
inserted
replaced
307 apply (subst exp_le_cancel_iff) |
307 apply (subst exp_le_cancel_iff) |
308 apply (subgoal_tac "ln (1 - (- x)) <= - (- x)") |
308 apply (subgoal_tac "ln (1 - (- x)) <= - (- x)") |
309 apply simp |
309 apply simp |
310 apply (rule ln_one_minus_pos_upper_bound) |
310 apply (rule ln_one_minus_pos_upper_bound) |
311 apply auto |
311 apply auto |
312 apply (rule sym) |
|
313 apply (subst exp_ln_iff) |
|
314 apply auto |
|
315 done |
312 done |
316 |
313 |
317 lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x" |
314 lemma ln_add_one_self_le_self2: "-1 < x ==> ln(1 + x) <= x" |
318 apply (subgoal_tac "x = ln (exp x)") |
315 apply (subgoal_tac "x = ln (exp x)") |
319 apply (erule ssubst)back |
316 apply (erule ssubst)back |