proposition: Lemma exp_le_3 : exp 1 <= 3.
proof: Proof. assert (exp_1 : exp 1 <> 0). { assert (H0 := exp_pos 1); red; intro; rewrite H in H0; elim (Rlt_irrefl _ H0). } apply Rmult_le_reg_l with (/ exp 1). { apply Rinv_0_lt_compat; apply exp_pos. } rewrite Rinv_l. 2:assumption. apply Rmult_le_reg_l with (/ 3). { lra. } rewrite Rmult_1_r; rewrite <- (Rmult_comm 3); rewrite <- Rmult_assoc; rewrite Rinv_l. 2:lra. rewrite Rmult_1_l; replace (/ exp 1) with (exp (-1)). 2:{ apply Rmult_eq_reg_l with (exp 1). 2:assumption. rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; rewrite Rinv_r;trivial. } unfold exp; case (exist_exp (-1)) as (?,e); simpl in |- *; unfold exp_in in e; assert (H := alternated_series_ineq (fun i:nat => / INR (fact i)) x 1). cut (sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (S (2 * 1)) <= x <= sum_f_R0 (tg_alt (fun i:nat => / INR (fact i))) (2 * 1)). { intro; elim H0; clear H0; intros H0 _; simpl in H0; unfold tg_alt in H0; simpl in H0. replace (/ 3) with (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 + -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)) by field. apply H0. } apply H. - unfold Un_decreasing; intros; apply Rmult_le_reg_l with (INR (fact n)). { apply INR_fact_lt_0. } apply Rmult_le_reg_l with (INR (fact (S n))). { apply INR_fact_lt_0. } rewrite Rinv_r. 2:{ apply INR_fact_neq_0. } rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l. 2:{ apply INR_fact_neq_0. } rewrite Rmult_1_r; apply le_INR; apply fact_le; apply Nat.le_succ_diag_r. - assert (H0 := cv_speed_pow_fact 1); unfold Un_cv; unfold Un_cv in H0; intros; elim (H0 _ H1); intros; exists x0; intros; unfold Rdist in H2; unfold Rdist; replace (/ INR (fact n)) with (1 ^ n / INR (fact n));auto. unfold Rdiv; rewrite pow1; rewrite Rmult_1_l; reflexivity. - unfold infinite_sum in e; unfold Un_cv, tg_alt; intros; elim (e _ H0); intros; exists x0; intros; replace (sum_f_R0 (fun i:nat => (-1) ^ i * / INR (fact i)) n) with (sum_f_R0 (fun i:nat => / INR (fact i) * (-1) ^ i) n);auto. apply sum_eq; intros; apply Rmult_comm. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra