proposition: Lemma Sin_ArcSin : forall (x : IR) Hx, x [=] Sin (ArcSin x Hx).
proof: Proof. intros. set (y := Sin (ArcSin x Hx)) in *. cut (Dom ArcSin y). intro H. cut (ArcSin x Hx [=] ArcSin y H). intro H0. 2: unfold y in |- *; inversion_clear H. 2: apply eq_symmetric_unfolded. Transparent ArcSin. simpl in H0. unfold y in H0. cut (Continuous_I (Min_leEq_Max x y) (( [-C-][1]{-}FId{^}2) {!} [-C-] [--] ([1] [/]TwoNZ))). intro H1. cut (Integral H1 [=] [0]). intro H2. clear H0. elim H; intros H0 H3. elim Hx; clear H; intros H H4. apply Integral_eq_zero with (contF := H1) (x := x). exact (pair (Min_leEq_lft x y) (lft_leEq_Max x y)). unfold FPower in |- *; intros. astepr (Part _ _ (ProjT2 Hx0)). apply less_wdr with (Exp (Part _ _ (ProjT1 Hx0))). apply Exp_pos. simpl in |- *; algebra. unfold FPower in |- *; intros. apply less_leEq; astepr (Part _ _ (ProjT2 Hx0)). apply less_wdr with (Exp (Part _ _ (ProjT1 Hx0))). apply Exp_pos. simpl in |- *; algebra. auto. apply eq_transitive_unfolded with (ArcSin y H[-]ArcSin x Hx). rstepl (ArcSin x Hx[+]Integral H1[-]ArcSin x Hx). apply cg_minus_wd; [ simpl in |- * | algebra ]. apply eq_symmetric_unfolded; apply Integral_plus_Integral with (Min3_leEq_Max3 [0] y x). apply included_imp_Continuous with (olor [--][1] [1]). exact ArcSin_def_lemma. apply included3_interval; auto. split. astepr ( [--]ZeroR); apply inv_resp_less; apply pos_one. apply pos_one. apply x_minus_x; simpl in |- *; algebra. apply included_imp_Continuous with (olor [--][1] [1]). exact ArcSin_def_lemma. apply included_interval; auto. elim (ArcSin_range x Hx); intros; apply ArcSin_Sin; auto. elim (ArcSin_range x Hx); intros; apply ArcSin_domain. unfold y in |- *. astepr ( [--] [--] (Sin (ArcSin x Hx))); astepr ( [--] (Sin [--] (ArcSin x Hx))); apply inv_resp_less. apply Sin_less_One. apply Cos_pos. apply inv_resp_less; auto. astepr ( [--] [--] (Pi [/]TwoNZ)); apply inv_resp_less; auto. unfold y in |- *; apply Sin_less_One. apply Cos_pos; auto. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT