proposition: Lemma A1_cvg : forall x:R, Un_cv (A1 x) (cos x).
proof: Proof. intro. unfold cos; destruct (exist_cos (Rsqr x)) 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 A1. replace (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) n) with (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * (x * x) ^ i) n). - apply H0; assumption. - apply sum_eq. intros. replace ((x * x) ^ i) with (x ^ (2 * i)). + reflexivity. + apply pow_sqr. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_def Lia Lra