proposition: Lemma C1_cvg : forall x y:R, Un_cv (C1 x y) (cos (x + y)).
proof: Proof. intros. unfold cos. destruct (exist_cos (Rsqr (x + y))) as (x0,p). unfold cos_in, cos_n, infinite_sum, Rdist in p. unfold Un_cv, Rdist; intros. destruct (p eps H) as (x1,H0). exists x1; intros. unfold C1. replace (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * (x + y) ^ (2 * k)) n) with (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * ((x + y) * (x + y)) ^ i) n). - apply H0; assumption. - apply sum_eq. intros. replace (((x + y) * (x + y)) ^ i) with ((x + y) ^ (2 * i)). + reflexivity. + apply pow_sqr. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Lia Lra