proposition: Lemma ArcSin_Sin_inv : Feq (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ)) (ArcSin[o]Sine) FId.
proof: Proof. set (HPi1 := pos_HalfPi) in *. set (HPi2 := neg_invHalfPi) in *. set (H := invHalfPi_less_HalfPi:proper (olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ))) in *. apply Feq_criterium with H ( [-C-][1]:PartIR) ZeroR. assert (H0 : Derivative _ H Sine Cosine). apply Included_imp_Derivative with realline I; Deriv. assert (H1 : [--][1] [<] OneR). set (H' := pos_one IR) in *; apply less_transitive_unfolded with ZeroR; auto. astepr ( [--]ZeroR); apply inv_resp_less; auto. set (H2 := Derivative_ArcSin H1) in *. eapply Derivative_wdr. 2: apply (Derivative_comp _ _ _ _ _ _ _ _ maps_Sin H0 H2). apply eq_imp_Feq. apply included_FMult. apply included_FComp. Included. intros. unfold FPower in |- *. cut (Dom ( [-C-] [--] ([1] [/]TwoNZ) {*} (Logarithm[o] [-C-][1]{-}FId{^}2)) (Part _ _ Hx)). intro H3. exists H3; apply Exp_domain. split. auto. exists (I, I). apply Log_domain. astepr ([1][-]Sine x Hx[^]2). astepl (OneR[-][1]). unfold cg_minus in |- *; apply plus_resp_less_lft. apply inv_resp_less. astepr (OneR[^]2); apply AbsIR_less_square. apply less_wdl with (AbsIR (Sin x)). inversion_clear X; apply Abs_Sin_less_One; auto. apply AbsIR_wd; simpl in |- *; algebra. split. split. intros x H3 Hx Hx'. astepr OneR. cut ([0] [<] [1][-]Sin x[^]2). intro H4. apply eq_transitive_unfolded with (([1][-]Sin x[^]2) [!] [--] ([1] [/]TwoNZ) [//]H4[*]Cos x). unfold power, FPower in |- *. unfold FPower in Hx. astepl (Part _ _ (ProjIR1 Hx) [*]Part _ _ (ProjIR2 Hx)). apply mult_wd. 2: simpl in |- *; algebra. elim Hx; clear Hx; intros Hx Hx1. astepl (Part _ _ Hx); clear Hx1. astepl (Part _ _ (ProjT2 Hx)). elim Hx; clear Hx; intros Hx1 Hx2. astepl (Part _ _ Hx2). astepl (Part _ _ (ProjT2 Hx2)). simpl in |- *; apply pfwdef. elim Hx2; intros Hx3 Hx4. astepl (Part _ _ Hx3). clear Hx4 Hx2. astepl ( [--] ([1] [/]TwoNZ) [*]Part _ _ (ProjIR2 Hx3)). elim Hx3; clear Hx3; intros Hx2 Hx3. astepl ( [--] ([1] [/]TwoNZ) [*]Part _ _ Hx3). apply mult_wdr. astepl (Part _ _ (ProjT2 Hx3)). unfold Log in |- *; apply pfwdef. elim Hx3; intros Hx4 Hx5. astepl (Part _ _ Hx4). astepl (Part _ _ (ProjIR1 Hx4) [-]Part _ _ (ProjIR2 Hx4)). elim Hx4; clear Hx5 Hx4 Hx3 Hx2; intros Hx2 Hx3. astepl (Part _ _ Hx2[-]Part _ _ Hx3). apply cg_minus_wd. algebra. simpl in |- *; algebra. unfold RealPowers.power in |- *. astepl (Exp [--] ([1] [/]TwoNZ[*]Log _ H4) [*]Cos x). astepl (([1][/] _[//]Exp_ap_zero ([1] [/]TwoNZ[*]Log _ H4)) [*]Cos x). astepr (Exp ([1] [/]TwoNZ[*]Log _ H4) [/] _[//]Exp_ap_zero ([1] [/]TwoNZ[*]Log _ H4)). rstepl (Cos x[/] _[//]Exp_ap_zero ([1] [/]TwoNZ[*]Log _ H4)). apply div_wd. 2: algebra. astepr (Exp (Log _ H4[*][1] [/]TwoNZ)). assert (H5 : [0] [<] Cos x). inversion_clear H3; apply Cos_pos; auto. astepl (Exp (Log _ H5)). apply Exp_wd. rstepl ((Log _ H5[+]Log _ H5) [/]TwoNZ). rstepr (Log _ H4 [/]TwoNZ). apply div_wd. 2: algebra. astepl (Log _ (mult_resp_pos _ _ _ H5 H5)). astepl (Log _ (pos_square _ _ (pos_ap_zero _ _ H5))). apply Log_wd. astepr (Cos x[^]2[+]Sin x[^]2[-]Sin x[^]2); rational. astepl (OneR[-][1]). unfold cg_minus in |- *. apply plus_resp_less_lft. apply inv_resp_less. astepr (OneR[^]2); apply AbsIR_less_square. inversion_clear H3; apply Abs_Sin_less_One; auto. Deriv. split; auto. intros; simpl in |- *; apply Integral_empty. astepl (Sin [0]); simpl in |- *; algebra. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT