proposition: Lemma arctan_series : forall c : IR, forall (Hs:fun_series_convergent_IR (olor ([--][1]) [1]) (fun (i:nat) => (([--][1])[^]i[/]nring (S (2*i))[//]nringS_ap_zero _ (2*i)){**}Fid IR{^}(2*i+1))) Hc, FSeries_Sum Hs c Hc[=]ArcTan c.
proof: Proof. intros c Hs Hc. set (J:=olor [--][1] [1]). assert (HJ:proper J). simpl. apply shift_zero_less_minus'. rstepr (Two:IR). apply pos_nring_S. assert (Y0 : included J realline). intros a b; constructor. assert (Y1 : J [0]). split;[rstepr ([--][0]:IR);apply inv_resp_less|]; apply pos_one. stepl (([-S-] Included_imp_Continuous realline {1/}([-C-][1]{+}FId{^}2) ArcTan_def_lemma J Y0) [0] Y1 c Hc). apply: Integral_wd. apply Feq_reflexive. intros d Hd. eapply Continuous_imp_inc. apply ArcTan_def_lemma. constructor. apply cg_inv_unique_2. cut (Derivative J HJ (FSeries_Sum Hs) {1/}([-C-][1]{+}FId{^}2)). intros X. destruct (FTC2 J _ (Included_imp_Continuous _ _ ArcTan_def_lemma J Y0) [0] Y1 _ _ X) as [z Hz]. clear X. apply eq_transitive with z. eapply eq_transitive; [|apply (Feq_imp_eq _ _ _ Hz _ Hc (Hc, Hc) I)]. apply: bin_op_wd_unfolded;[|apply un_op_wd_unfolded]; apply pfwdef; apply eq_reflexive. apply eq_symmetric. eapply eq_transitive; [|apply (Feq_imp_eq _ _ _ Hz _ Y1 (Y1, Y1) I)]. rstepl ([0][-][0]:IR). apply: cg_minus_wd. stepr (ArcTan [0]). assert (Z:Dom Tang [0]). repeat split; try constructor. intros []. stepl ([1]:IR). apply ring_non_triv. apply eq_symmetric. apply Cos_zero. stepl (ArcTan (Tan _ Z)). apply pfwdef. apply Tan_zero. apply ArcTan_Tan; [rstepr ([--][0]:IR); apply inv_resp_less|]; apply pos_HalfPi. unfold ArcTan, ArcTang. apply: Integral_wd. apply Feq_reflexive. intros d Hd. eapply Continuous_imp_inc. apply ArcTan_def_lemma. constructor. eapply eq_transitive. apply eq_symmetric. eapply (series_sum_zero conv_zero_series). simpl; apply series_sum_wd. intros n. eapply eq_transitive. apply eq_symmetric. apply cring_mult_zero. apply mult_wdr. apply eq_symmetric. apply (zero_nexp IR (2*n+1)). auto with *. clear -J. eapply Derivative_wdr. apply (bellcurve_series bellcurve_series_convergent_IR). apply Derivative_FSeries. intros n. rewrite Nat.add_comm. simpl. Derivative_Help; [|apply Derivative_scal;apply Derivative_nth;Deriv..]. FEQ. Qed.
imports: CoRN.transc.InvTrigonom CoRN.tactics.CornTac