Sign properties: cosine is positive in
(-π/2,π/2), sine in
(0,π) and tangent in 0,π/2).
Lemma Cos_pos : forall x, [--] (π [/]2) [<] x -> x [<] π [/]2 -> 0 [<] Cos x.
Lemma Sin_pos : forall x : IR, 0 [<] x -> x [<] π -> 0 [<] Sin x.
Lemma Tan_pos : forall x, 0 [<] x -> x [<] π [/]2 -> forall Hx, 0 [<] Tan x Hx.
Lemma Cos_nonneg : forall x, [--] (π [/]2) [<=] x -> x [<=] π [/]2 -> 0 [<=] Cos x.
Lemma Sin_nonneg : forall x, 0 [<=] x -> x [<=] π -> 0 [<=] Sin x.
Consequences.
Lemma Abs_Sin_less_One : forall x, [--] (π [/]2) [<] x -> x [<] π [/]2 -> AbsIR (Sin x) [<] 1.
Lemma Abs_Cos_less_One : forall x, 0 [<] x -> x [<] π -> AbsIR (Cos x) [<] 1.
Sine is (strictly) increasing in [ −π/2,Pi[/]2]; cosine
is (strictly) decreasing in [0,Pi].
Lemma Sin_resp_leEq : forall x y, [--] (π [/]2) [<=] x -> y [<=] π [/]2 -> x [<=] y -> Sin x [<=] Sin y.
Lemma Cos_resp_leEq : forall x y, 0 [<=] x -> y [<=] π -> x [<=] y -> Cos y [<=] Cos x.
Lemma Cos_resp_less : forall x y, 0 [<=] x -> x [<] y -> y [<=] π -> Cos y [<] Cos x.
Included.
Qed.
Lemma Sin_resp_less : forall x y, [--] (π [/]2) [<=] x -> x [<] y -> y [<=] π [/]2 -> Sin x [<] Sin y.
Lemma Sin_ap_Zero : forall x:IR, (forall z, x[#](zring z)[*]π) -> Sin x [#] 0.
Lemma Cos_ap_Zero : forall x:IR, (forall z, x[#]π[/]2[+](zring z)[*]π) -> Cos x [#] 0.
Section Tangent.
Lemma Tang_Domain : forall x:IR, (forall z, x[#]π[/]2[+](zring z)[*]π) -> Dom Tang x.
Lemma Tang_Domain' : ⊆ ((⋅,⋅) ([--](π[/]2)) (π[/]2)) (Dom Tang).
Derivative of Tangent
Finally, two formulas for the derivative of the tangent function and monotonicity properties.
Lemma bnd_Cos : bnd_away_zero_in_P Cosine ((⋅,⋅) [--] (π [/]2) (π [/]2)).
Included.
Qed.
Lemma Derivative_Tan_1 : forall H, Derivative ((⋅,⋅) [--] (π [/]2) (π [/]2)) H Tang {1/} (Cosine{^}2).
Included.
Included.
Qed.
Lemma Derivative_Tan_2 : forall H, Derivative ((⋅,⋅) [--] (π [/]2) (π [/]2)) H Tang ( [-C-]1{+}Tang{^}2).
Included.
Included.
Included.
Included.
Qed.
Lemma Tan_resp_less : forall x y,
[--] (π [/]2) [<] x -> y [<] π [/]2 -> forall Hx Hy, x [<] y -> Tan x Hx [<] Tan y Hy.
Lemma Tan_resp_leEq : forall x y,
[--] (π [/]2) [<] x -> y [<] π [/]2 -> forall Hx Hy, x [<=] y -> Tan x Hx [<=] Tan y Hy.
End Tangent.