proposition: Lemma continuity_cos : continuity cos.
proof: Proof. set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)). cut (CVN_R fn). 1:intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }). 1:intro cv; cut (forall n:nat, continuity (fn n)). 1:intro; cut (forall x:R, cos x = SFL fn cv x). 1:intro; cut (continuity (SFL fn cv) -> continuity cos). - intro; apply H1. apply SFL_continuity; assumption. - unfold continuity in |- *; unfold continuity_pt in |- *; unfold continue_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; unfold Rdist in |- *; intros. elim (H1 x _ H2); intros. exists x0; intros. elim H3; intros. split. + apply H4. + intros; rewrite (H0 x); rewrite (H0 x1); apply H5; apply H6. - intro; unfold cos, SFL in |- *. case (cv x) as (x1,HUn); case (exist_cos (Rsqr x)) as (x0,Hcos); intros. symmetry; eapply UL_sequence. + apply HUn. + unfold cos_in, infinite_sum in Hcos; unfold Un_cv in |- *; intros. elim (Hcos _ H0); intros N0 H1. exists N0; intros. unfold Rdist in H1; unfold Rdist, SP in |- *. replace (sum_f_R0 (fun k:nat => fn k x) n) with (sum_f_R0 (fun i:nat => cos_n i * Rsqr x ^ i) n). * apply H1; assumption. * apply sum_eq; intros. unfold cos_n, fn in |- *; apply Rmult_eq_compat_l. unfold Rsqr in |- *; rewrite pow_sqr; reflexivity. - intro; unfold fn in |- *; replace (fun x:R => (-1) ^ n / INR (fact (2 * n)) * x ^ (2 * n)) with (fct_cte ((-1) ^ n / INR (fact (2 * n))) * pow_fct (2 * n))%F; [ idtac | reflexivity ]. apply continuity_mult. + apply derivable_continuous; apply derivable_const. + apply derivable_continuous; apply (derivable_pow (2 * n)). - apply CVN_R_CVS; apply X. - apply CVN_R_cos; unfold fn in |- *; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo_fun Rtrigo_def Rtrigo_alt Cos_rel Cos_plus ZArith_base Zcomplements Lia Lra Ranalysis1 Rsqrt_def PSeries_reg