proposition: Lemma derivable_pt_lim_sin_0 : derivable_pt_lim sin 0 1.
proof: Proof. unfold derivable_pt_lim; intros. set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)). assert (CVN_R fn) by (apply CVN_R_sin; unfold fn; reflexivity). assert (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }) by apply (CVN_R_CVS _ X). set (r := mkposreal _ Rlt_0_1). assert (CVN_r fn r) by apply (X r). assert (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y). { intros; unfold fn; replace (fun x:R => (-1) ^ n / INR (fact (2 * n + 1)) * x ^ (2 * n)) with (fct_cte ((-1) ^ n / INR (fact (2 * n + 1))) * pow_fct (2 * n))%F; [ idtac | reflexivity ]. apply continuity_pt_mult. - apply derivable_continuous_pt. apply derivable_pt_const. - apply derivable_continuous_pt. apply (derivable_pt_pow (2 * n) y). } assert (Boule 0 r 0). { unfold Boule; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_R0; apply (cond_pos r). } assert (H2 := SFL_continuity_pt _ cv _ X0 H0 _ H1). unfold continuity_pt in H2; unfold continue_in in H2; unfold limit1_in in H2; unfold limit_in in H2; simpl in H2; unfold Rdist in H2. elim (H2 _ H); intros alp H3. elim H3; intros. exists (mkposreal _ H4). simpl; intros. rewrite sin_0; rewrite Rplus_0_l; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. assert (Rabs (SFL fn cv h - SFL fn cv 0) < eps). { apply H5. split. - unfold D_x, no_cond; split. + trivial. + apply (not_eq_sym (A:=R)); apply H6. - unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply H7. } assert (SFL fn cv 0 = 1). { unfold SFL, sin. case (cv 0) as (?,HUn). eapply UL_sequence. - apply HUn. - unfold SP, fn; unfold Un_cv; intros; exists 1%nat; intros. unfold Rdist; replace (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * 0 ^ (2 * k)) n) with 1. + unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. + rewrite decomp_sum. * simpl; rewrite Rmult_1_r; unfold Rdiv; rewrite Rinv_1; rewrite Rmult_1_r; pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_eq_compat_l. symmetry ; apply sum_eq_R0; intros. rewrite Rmult_0_l; rewrite Rmult_0_r; reflexivity. * unfold ge in H10; apply Nat.lt_le_trans with 1%nat; [ apply Nat.lt_succ_diag_r | apply H10 ]. } cut (SFL fn cv h = sin h / h). { intro; rewrite H9 in H8; rewrite H10 in H8. apply H8. } unfold SFL, sin. case (cv h) as (x,HUn). case (exist_sin (Rsqr h)) as (x0,Hsin). unfold Rdiv; rewrite (Rmult_inv_r_id_m h x0 H6). eapply UL_sequence. - apply HUn. - unfold sin_in in Hsin; unfold sin_n, infinite_sum in Hsin; unfold SP, fn, Un_cv; intros. elim (Hsin _ H10); intros N0 H11. exists N0; intros. unfold Rdist; unfold Rdist in H11. replace (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * h ^ (2 * k)) n) with (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * Rsqr h ^ i) n). + apply H11; assumption. + apply sum_eq; intros; apply Rmult_eq_compat_l; unfold Rsqr; rewrite pow_sqr; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra