proposition: Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }.
proof: Proof. intros; set (f := fun x:R => exp x - y). assert (H0 : 0 < y) by (apply Rlt_le_trans with 1; auto with real). cut (f 0 <= 0); [intro H1|]. - cut (continuity f); [intro H2|]. + cut (0 <= f y); [intro H3|]. * cut (f 0 * f y <= 0); [intro H4|]. -- pose proof (IVT_cor f 0 y H2 (Rlt_le _ _ H0) H4) as (t,(_,H7)); exists t; unfold f in H7; symmetry; apply Rminus_diag_uniq; exact H7. -- pattern 0 at 2; rewrite <- (Rmult_0_r (f y)); rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l; assumption. * unfold f; apply Rplus_le_reg_l with y; left; apply Rlt_trans with (1 + y). -- rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1. -- replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y); lra | ring ]. + unfold f; change (continuity (exp - fct_cte y)); apply continuity_minus; [ apply derivable_continuous; apply derivable_exp | apply derivable_continuous; apply derivable_const ]. - unfold f; rewrite exp_0; apply Rplus_le_reg_l with y; rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H | ring ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra