proposition: Lemma cv_cauchy_1 : forall An:nat -> R, { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } -> Cauchy_crit_series An.
proof: Proof. intros An (x,p). unfold Un_cv in p. unfold Cauchy_crit_series; unfold Cauchy_crit. intros. cut (0 < eps / 2). - intro. elim (p (eps / 2) H0); intros. exists x0. intros. apply Rle_lt_trans with (Rdist (sum_f_R0 An n) x + Rdist (sum_f_R0 An m) x). + unfold Rdist. replace (sum_f_R0 An n - sum_f_R0 An m) with (sum_f_R0 An n - x + - (sum_f_R0 An m - x)); [ idtac | ring ]. rewrite <- (Rabs_Ropp (sum_f_R0 An m - x)). apply Rabs_triang. + apply Rlt_le_trans with (eps / 2 + eps / 2). * apply Rplus_lt_compat. -- apply H1; assumption. -- apply H1; assumption. * right; apply Rplus_half_diag. - unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. Qed.
imports: Rbase Rfunctions Rseries Rcomplete