proposition: Lemma exp_plus : forall x y:R, exp (x + y) = exp x * exp y.
proof: Proof. intros; assert (H0 := E1_cvg x). assert (H := E1_cvg y). assert (H1 := E1_cvg (x + y)). eapply UL_sequence. - apply H1. - assert (H2 := CV_mult _ _ _ _ H0 H). assert (H3 := CV_minus _ _ _ _ H2 (Reste_E_cv x y)). unfold Un_cv; unfold Un_cv in H3; intros. elim (H3 _ H4); intros. exists (S x0); intros. rewrite <- (exp_form x y n). + rewrite Rminus_0_r in H5. apply H5. unfold ge; apply Nat.le_trans with (S x0). * apply Nat.le_succ_diag_r. * apply H6. + apply Nat.lt_le_trans with (S x0). * apply Nat.lt_0_succ. * apply H6. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lia Lra