proposition: Lemma Tan_ilim : forall x, {y : IR | olor [--] (Pi [/]TwoNZ) (Pi [/]TwoNZ) y | forall Hy, x [<=] Tan y Hy}.
proof: Proof. intros. set (aux_val := sqrt _ (less_leEq _ _ _ (pos_two IR)) [/]TwoNZ) in *. assert (H : [0] [<] aux_val). unfold aux_val in |- *. apply shift_less_div; [ apply pos_two | apply power_cancel_less with 2 ]. apply sqrt_nonneg. astepl (ZeroR[^]2); astepl ZeroR; astepr (Two:IR); apply pos_two. assert (H0 : sqrt _ (less_leEq _ _ _ (pos_two _)) [#] [0]). apply mult_cancel_ap_zero_lft with (OneR [/]TwoNZ). eapply ap_wdl_unfolded; [ apply pos_ap_zero; apply H | unfold aux_val in |- *; rational ]. assert (H1 : aux_val [=] ([1][/] _[//]H0)). unfold aux_val in |- *. apply eq_div; astepr (Two:IR); Step_final (sqrt _ (less_leEq _ _ _ (pos_two _)) [^]2). assert (H2 : aux_val [<] [1]). apply power_cancel_less with 2. apply less_leEq; apply pos_one. unfold aux_val in |- *; rstepl ((sqrt _ (less_leEq _ _ _ (pos_two IR)) [^]2) [/]FourNZ); astepr OneR. apply shift_div_less; [ apply pos_four | astepl (Two:IR); astepr (Four:IR) ]; apply two_less_four. elim (less_cotransitive_unfolded _ _ _ H2 x); intros. 2: exists (Pi [/]FourNZ); repeat split; PiSolve. 2: intro; astepr OneR; apply less_leEq; auto. assert (H3 : Two[*]x [#] [0]). apply mult_resp_ap_zero. apply two_ap_zero. apply pos_ap_zero; apply less_transitive_unfolded with aux_val; auto. assert (H4 : Dom ArcCos ([1][/] _[//]H3)). repeat split. apply less_transitive_unfolded with ZeroR; [ astepr ( [--]ZeroR); apply inv_resp_less; apply pos_one | apply recip_resp_pos ]. apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. apply shift_div_less. apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. astepr (Two[*]x); apply less_transitive_unfolded with (Two[*]aux_val). 2: apply mult_resp_less_lft; auto; apply pos_two. unfold aux_val in |- *; rstepr (sqrt _ (less_leEq _ _ _ (pos_two _))). apply power_cancel_less with 2. apply sqrt_nonneg. astepl OneR; astepr (Two:IR); apply one_less_two. assert (H5 : Pi [/]FourNZ [<=] ArcCos _ H4). assert (H5 : Dom ArcCos aux_val). repeat split; auto; unfold aux_val in |- *. apply less_transitive_unfolded with ZeroR; auto; astepr ( [--]ZeroR); apply inv_resp_less; apply pos_one. apply leEq_wdl with (ArcCos _ H5). 2: assert (H6 : Dom ArcCos (Cos (Pi [/]FourNZ))). 2: apply dom_wd with aux_val; auto. 2: Step_final ([1][/] _[//]H0). 2: apply eq_transitive_unfolded with (ArcCos _ H6). 3: apply ArcCos_Cos; PiSolve. 2: apply pfwdef; unfold aux_val in |- *. 2: Step_final ([1][/] _[//]H0). apply ArcCos_resp_leEq. apply less_transitive_unfolded with ZeroR. astepr ( [--]ZeroR); apply inv_resp_less; apply pos_one. apply recip_resp_pos; apply mult_resp_pos; try apply pos_two; apply less_transitive_unfolded with aux_val; auto. apply shift_div_leEq. apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. apply leEq_wdl with (aux_val[*] (Two[*]aux_val)). repeat apply mult_resp_leEq_lft; apply less_leEq; auto; apply pos_two. unfold aux_val in |- *. rstepl ((sqrt _ (less_leEq _ _ _ (pos_two _)) [^]2) [/]TwoNZ). Step_final ((Two:IR) [/]TwoNZ). auto. exists (ArcCos _ H4). Opaque iprop. unfold ArcCos in |- *; simpl in |- *. Transparent iprop. elim H4; intros H6' H7; elim H7; intros. apply iprop_wd with (Pi [/]TwoNZ[-]ArcSin _ H7). 2: algebra. elim (ArcSin_range _ H7); intros; split. apply shift_less_minus; apply shift_plus_less'. rstepr Pi; apply less_transitive_unfolded with (Pi [/]TwoNZ); PiSolve. apply shift_minus_less; apply shift_less_plus'. astepl ZeroR. assert (H6 : Dom ArcSin (Sin [0])). apply dom_wd with ZeroR; [ split | algebra ]; [ astepr ( [--]ZeroR); apply inv_resp_less | idtac ]; apply pos_one. apply less_wdl with (ArcSin _ H6). 2: apply ArcSin_Sin; PiSolve. apply leEq_not_eq. apply ArcSin_resp_leEq; auto. astepr ZeroR; astepr ( [--]ZeroR); apply inv_resp_less; apply pos_one. astepl ZeroR; apply less_leEq; apply recip_resp_pos. apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. apply pfstrx with Sine I I. apply ap_wdl_unfolded with ZeroR. apply ap_wdr_unfolded with ([1][/] _[//]H3). apply ap_symmetric_unfolded; apply pos_ap_zero; apply recip_resp_pos. apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. apply eq_transitive_unfolded with (Sin (ArcSin _ H7)); [ apply Sin_ArcSin | simpl in |- *; algebra ]. apply eq_transitive_unfolded with (Sin (ArcSin _ H6)); [ astepl (Sin [0]); apply Sin_ArcSin | simpl in |- *; algebra ]. intros; unfold Tan, Tang in |- *. assert (H6 : Cos (ArcCos _ H4) [#] [0]). eapply ap_wdl_unfolded. 2: apply Cos_ArcCos. apply recip_ap_zero; auto. apply leEq_wdr with (Sin (ArcCos _ H4) [/] _[//]H6). 2: simpl in |- *; algebra. apply shift_leEq_div. Opaque Cos. unfold ArcCos in |- *; simpl in |- *. astepr (Sin (ArcSin _ (ProjIR2 H4))). eapply less_wdr. 2: apply Sin_ArcSin. apply recip_resp_pos; apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. apply leEq_wdl with (x[*] ([1][/] _[//]H3)). 2: apply mult_wdr; apply Cos_ArcCos. rstepl (OneR [/]TwoNZ). apply leEq_transitive with ([1][/] _[//]H0). apply recip_resp_leEq. astepl (ZeroR[*]Two); apply shift_mult_less with (two_ap_zero IR); auto; apply pos_two. apply power_cancel_leEq with 2; auto. apply less_leEq; apply pos_two. astepl (Two:IR); rstepr (Four:IR); apply less_leEq; apply two_less_four. astepl (Sin (Pi [/]FourNZ)); apply Sin_resp_leEq. PiSolve. astepl (Pi [/]TwoNZ[-]ArcSin _ (ProjIR2 H4)). apply shift_minus_leEq; apply shift_leEq_plus'; astepl ZeroR. assert (H7 : Dom ArcSin (Sin [0])). apply dom_wd with ZeroR; [ split | algebra ]; [ astepr ( [--]ZeroR); apply inv_resp_less | idtac ]; apply pos_one. apply leEq_wdl with (ArcSin _ H7). 2: apply ArcSin_Sin; PiSolve. apply ArcSin_resp_leEq. astepr ZeroR; astepr ( [--]ZeroR); apply inv_resp_less; apply pos_one. astepl ZeroR; apply less_leEq; apply recip_resp_pos. apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. apply shift_div_less. apply mult_resp_pos; [ apply pos_two | apply less_transitive_unfolded with aux_val; auto ]. astepr (Two[*]x); apply less_transitive_unfolded with (Two[*]aux_val). 2: apply mult_resp_less_lft; auto; apply pos_two. unfold aux_val in |- *; rstepr (sqrt _ (less_leEq _ _ _ (pos_two _))). apply power_cancel_less with 2. apply sqrt_nonneg. astepl OneR; astepr (Two:IR); apply one_less_two. auto. Qed.
imports: CoRN.transc.RealPowers CoRN.transc.TrigMon CoRN.ftc.StrongIVT