proposition: Lemma Cseq_norm_Rseq : forall (An : nat -> C), {l | Rseq_cv (fun n => sum_f_R0 (fun n =>(Cnorm (An n)))n) l} -> {l | Cseq_cv (fun n => sum_f_C0 (fun n =>((An n)))n) l}.
proof: Proof. intros An H. generalize (Rseq_norm_abs_Cim An H). generalize (Rseq_norm_abs_Cre An H). intros Hre Him. assert ( H1 : {l : R | Rseq_cv (fun n : nat => sum_f_R0 (fun n0 : nat => Cim (An n0)) n) l}). apply (Rser_abs_cv_cv (fun n0 : nat => Cim (An n0))). unfold Rser_abs_cv. unfold Rseq_abs. apply Him. assert ( H2 : {l : R | Rseq_cv (fun n : nat => sum_f_R0 (fun n0 : nat => Cre (An n0)) n) l}). apply (Rser_abs_cv_cv (fun n0 : nat => Cre (An n0))). unfold Rser_abs_cv. unfold Rseq_abs. apply Hre. destruct H1 as (lim, H1). destruct H2 as (lre, H2). exists (lre +i lim). apply <- Cseq_Rseq_Rseq_equiv. split. simpl. assert ((fun n : nat => Cre (sum_f_C0 (fun n0 : nat => An n0) n)) == (fun n : nat => sum_f_R0 (fun n0 : nat => Cre (An n0)) n)). unfold "==". intros n. rewrite <- sum_f_C0_Cre_compat. reflexivity. apply (Rseq_cv_eq_compat (fun n : nat => sum_f_R0 (fun n0 : nat => Cre (An n0)) n) (fun n : nat => Cre (sum_f_C0 (fun n0 : nat => An n0) n))). apply Rseq_eq_sym. assumption. assumption. assert ((fun n : nat => Cim (sum_f_C0 (fun n0 : nat => An n0) n)) == (fun n : nat => sum_f_R0 (fun n0 : nat => Cim (An n0)) n)). unfold "==". intros n. rewrite <- sum_f_C0_Cim_compat. reflexivity. apply (Rseq_cv_eq_compat (fun n : nat => sum_f_R0 (fun n0 : nat => Cim (An n0)) n) (fun n : nat => Cim (sum_f_C0 (fun n0 : nat => An n0) n))). apply Rseq_eq_sym. assumption. assumption. Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts