proposition: Lemma ArcSin_range : forall x Hx, [--] (Pi [/]TwoNZ) [<] ArcSin x Hx and ArcSin x Hx [<] Pi [/]TwoNZ.
proof: Proof. intros. Transparent ArcSin. cut {y : IR | olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ) y | forall Hy, Sine y Hy [=] x}. intros H; elim H; clear H; intros y H H0. elim H; clear H; intros H1 H2. assert (H : Sin y [=] x). simpl in |- *; algebra. assert (H3 : Dom ArcSin (Sin y)). apply dom_wd with x; algebra. split. astepr (ArcSin _ H3). apply less_wdr with y; auto. apply eq_symmetric_unfolded; apply ArcSin_Sin; auto. astepl (ArcSin _ H3). apply less_wdl with y; auto. apply eq_symmetric_unfolded; apply ArcSin_Sin; auto. elim Hx; intros H H0. set (H1 := less_leEq _ _ _ invHalfPi_less_HalfPi) in *. cut (Continuous_I H1 Sine). intro H2. apply IVT'_I with H1 H2; auto. PiSolve. intros x0 y H3 H4 H5 Hx0 Hy. 2: astepl (Sine [--] (Pi [/]TwoNZ) I); astepl (Sin [--] (Pi [/]TwoNZ)); astepl ( [--] (Sin (Pi [/]TwoNZ))); astepl ( [--]OneR); auto. 2: astepr (Sine (Pi [/]TwoNZ) I); astepr (Sin (Pi [/]TwoNZ)); astepr OneR; auto. 2: apply included_imp_Continuous with realline; Contin. apply less_wdl with (Sin x0). 2: simpl in |- *; algebra. apply less_wdr with (Sin y). 2: simpl in |- *; algebra. inversion_clear H3; inversion_clear H4; apply Sin_resp_less; auto. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT