proposition: Lemma derivable_pt_lim_exp : forall x:R, derivable_pt_lim exp x (exp x).
proof: Proof. intro; assert (H0 := derivable_pt_lim_exp_0). unfold derivable_pt_lim in H0; unfold derivable_pt_lim; intros. cut (0 < eps / exp x); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ apply H | apply Rinv_0_lt_compat; apply exp_pos ] ]. elim (H0 _ H1); intros del H2. exists del; intros. assert (H5 := H2 _ H3 H4). rewrite Rplus_0_l in H5; rewrite exp_0 in H5. replace ((exp (x + h) - exp x) / h - exp x) with (exp x * ((exp h - 1) / h - 1)). - rewrite Rabs_mult; rewrite (Rabs_right (exp x)). + apply Rmult_lt_reg_l with (/ exp x). * apply Rinv_0_lt_compat; apply exp_pos. * rewrite <- Rmult_assoc; rewrite Rinv_l. -- rewrite Rmult_1_l; rewrite <- (Rmult_comm eps). apply H5. -- assert (H6 := exp_pos x); red; intro; rewrite H7 in H6; elim (Rlt_irrefl _ H6). + apply Rle_ge; left; apply exp_pos. - rewrite Rmult_minus_distr_l. rewrite Rmult_1_r; unfold Rdiv; rewrite <- Rmult_assoc; rewrite Rmult_minus_distr_l. rewrite Rmult_1_r; rewrite exp_plus; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra