Section Sum_and_so_on.
Lemma Sin_plus : forall x y : IR, Sin (x[+]y) [=] Sin x[*]Cos y[+]Cos x[*]Sin y.
Lemma Cos_plus : forall x y : IR, Cos (x[+]y) [=] Cos x[*]Cos y[-]Sin x[*]Sin y.
As a corollary we get the rule for the tangent of the sum.
Lemma Tan_plus : forall x y Hx Hy Hxy H,
Tan (x[+]y) Hxy [=] (Tan x Hx[+]Tan y Hy[/] 1[-]Tan x Hx[*]Tan y Hy[//]H).
Sine, cosine and tangent of −x.
Lemma Cos_inv : forall x : IR, Cos [--]x [=] Cos x.
Lemma Sin_inv : forall x : IR, Sin [--]x [=] [--] (Sin x).
Lemma Tan_inv : forall x Hx Hx', Tan [--]x Hx' [=] [--] (Tan x Hx).
The fundamental formulas of trigonometry: cos(x)2+sin(x)2=1 and, equivalently, 1+tan(x)2=1/(cos(x)2).
Theorem FFT : forall x : IR, Cos x[^]2[+]Sin x[^]2 [=] 1.
Lemma FFT' : forall x Hx H, 1[+]Tan x Hx[^]2 [=] (1[/] Cos x[^]2[//]H).
End Sum_and_so_on.
Section Basic_Properties.
Basic properties
We now prove most of the usual trigonometric (in)equalities.
Sine, cosine and tangent are strongly extensional and well defined.
Lemma Sin_strext : forall x y : IR, Sin x [#] Sin y -> x [#] y.
Lemma Cos_strext : forall x y : IR, Cos x [#] Cos y -> x [#] y.
Lemma Tan_strext : forall x y Hx Hy, Tan x Hx [#] Tan y Hy -> x [#] y.
Lemma Sin_wd : forall x y : IR, x [=] y -> Sin x [=] Sin y.
Lemma Cos_wd : forall x y : IR, x [=] y -> Cos x [=] Cos y.
Lemma Tan_wd : forall x y Hx Hy, x [=] y -> Tan x Hx [=] Tan y Hy.
Lemma Tan_Sin_over_Cos : forall x Hx H, Tan x Hx[=](Sin x[/]Cos x[//]H).
The sine and cosine produce values in [-1,1].
Lemma AbsIR_Sin_leEq_One : forall x : IR, AbsIR (Sin x) [<=] 1.
Lemma AbsIR_Cos_leEq_One : forall x : IR, AbsIR (Cos x) [<=] 1.
Lemma Sin_leEq_One : forall x : IR, Sin x [<=] 1.
Lemma Cos_leEq_One : forall x : IR, Cos x [<=] 1.
If the cosine is positive then the sine is in (-1,1).
Lemma Sin_less_One : forall x : IR, 0 [<] Cos x -> Sin x [<] 1.
Lemma AbsIR_Sin_less_One : forall x : IR, 0 [<] Cos x -> AbsIR (Sin x) [<] 1.
End Basic_Properties.