proposition: Lemma ArcSin_def_lemma : Continuous (olor [--][1] [1]) (( [-C-][1]{-}FId{^}2) {!} [-C-] [--] ([1] [/]TwoNZ)).
proof: Proof. split. unfold FPower in |- *. apply included_FComp. apply included_FMult. Included. apply included_FComp. Included. intros; apply Log_domain. inversion_clear X. simpl in |- *; apply shift_less_minus; astepl (x[^]2). astepr (OneR[^]2). apply AbsIR_less_square. simpl in |- *; unfold ABSIR in |- *; apply Max_less; auto. apply inv_cancel_less; astepr x; auto. intros; apply Exp_domain. intros a b Hab H. apply continuous_I_power. Contin. Contin. split. Included. simpl in H. set (c := Max (AbsIR a) (AbsIR b)) in *. cut ([0] [<=] c); intros. 2: unfold c in |- *; apply leEq_transitive with (AbsIR a); [ apply AbsIR_nonneg | apply lft_leEq_Max ]. elim (H _ (compact_inc_lft _ _ Hab)); intros. elim (H _ (compact_inc_rht _ _ Hab)); intros. assert (H1 : c [<] [1]). unfold c in |- *. apply Max_less; simpl in |- *; unfold ABSIR in |- *; apply Max_less; auto; apply inv_cancel_less. astepr a; auto. astepr b; auto. assert (Hc : [--]c [<=] c). apply leEq_transitive with ZeroR; auto. astepr ( [--]ZeroR); apply inv_resp_leEq; auto. cut (included (Compact Hab) (Compact Hc)). intro H2. exists ([1][-]c[^]2). apply shift_less_minus. astepl (c[^]2); astepr (OneR[^]2). apply nexp_resp_less; auto. intros y H3 Hy. astepr ([1][-]y[^]2). apply minus_resp_leEq_both. apply leEq_reflexive. apply AbsIR_leEq_square. elim (H2 _ H3); intros. simpl in |- *; unfold ABSIR in |- *; apply Max_leEq; auto. astepr ( [--] [--]c); apply inv_resp_leEq; auto. intros x H2. inversion_clear H2; unfold c in |- *; split. astepr ( [--] [--]x); apply inv_resp_leEq. apply leEq_transitive with ( [--]a). apply inv_resp_leEq; auto. eapply leEq_transitive; [ apply inv_leEq_AbsIR | apply lft_leEq_Max ]. apply leEq_transitive with b; auto. eapply leEq_transitive; [ apply leEq_AbsIR | apply rht_leEq_Max ]. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT