proposition: Lemma exp_pos_pos : forall x:R, 0 < x -> 0 < exp x.
proof: Proof. intros; set (An := fun N:nat => / INR (fact N) * x ^ N). cut (Un_cv (fun n:nat => sum_f_R0 An n) (exp x)). - intro; apply Rlt_le_trans with (sum_f_R0 An 0). + unfold An; simpl; rewrite Rinv_1; rewrite Rmult_1_r; apply Rlt_0_1. + apply sum_incr. * assumption. * intro; unfold An; left; apply Rmult_lt_0_compat. -- apply Rinv_0_lt_compat; apply INR_fact_lt_0. -- apply (pow_lt _ n H). - unfold exp; unfold projT1; case (exist_exp x); intro. unfold exp_in; unfold infinite_sum, Un_cv; trivial. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra