proposition: Theorem Dln : forall y:R, 0 < y -> D_in ln Rinv (fun x:R => 0 < x) y.
proof: Proof. intros y Hy; unfold D_in. apply limit1_ext with (f := fun x:R => / ((exp (ln x) - exp (ln y)) / (ln x - ln y))). { intros x [HD1 HD2]; repeat rewrite exp_ln. 2,3:assumption. unfold Rdiv; rewrite Rinv_mult. rewrite Rinv_inv. apply Rmult_comm. } apply limit_inv with (f := fun x:R => (exp (ln x) - exp (ln y)) / (ln x - ln y)). 2:lra. apply limit1_imp with (f := fun x:R => (fun x:R => (exp x - exp (ln y)) / (x - ln y)) (ln x)) (D := Dgf (D_x (fun x:R => 0 < x) y) (D_x (fun x:R => True) (ln y)) ln). { intros x [H1 H2]; split. - split; auto. - split; auto. red; intros H3; case H2; apply ln_inv; auto. } apply limit_comp with (l := ln y) (g := fun x:R => (exp x - exp (ln y)) / (x - ln y)) (f := ln). { apply ln_continue; auto. } assert (H0 := derivable_pt_lim_exp (ln y)); unfold derivable_pt_lim in H0; unfold limit1_in; unfold limit_in; simpl; unfold Rdist; intros; elim (H0 _ H); intros; exists (pos x); split. { apply (cond_pos x). } intros; pattern y at 3; rewrite <- exp_ln. 2:assumption. pattern x0 at 1; replace x0 with (ln y + (x0 - ln y)); [ idtac | ring ]. apply H1. { elim H2; intros H3 _; unfold D_x in H3; elim H3; clear H3; intros _ H3; apply Rminus_eq_contra; apply (not_eq_sym (A:=R)); apply H3. } elim H2; clear H2; intros _ H2; apply H2. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra