Library Coq.Reals.Rtrigo
sin_PI2 is the only remaining axiom
Some properties of cos, sin and tan
Lemma sin2 :
forall x:
R,
Rsqr (
sin x)
= 1
- Rsqr (
cos x).
Lemma sin_2a :
forall x:
R,
sin (2
* x)
= 2
* sin x * cos x.
Lemma cos_2a :
forall x:
R,
cos (2
* x)
= cos x * cos x - sin x * sin x.
Lemma cos_2a_cos :
forall x:
R,
cos (2
* x)
= 2
* cos x * cos x - 1.
Lemma cos_2a_sin :
forall x:
R,
cos (2
* x)
= 1
- 2
* sin x * sin x.
Lemma tan_2a :
forall x:
R,
cos x <> 0 ->
cos (2
* x)
<> 0 ->
1
- tan x * tan x <> 0 ->
tan (2
* x)
= 2
* tan x / (1
- tan x * tan x).
Lemma sin_neg :
forall x:
R,
sin (
- x)
= - sin x.
Lemma cos_neg :
forall x:
R,
cos (
- x)
= cos x.
Lemma tan_0 :
tan 0
= 0.
Lemma tan_neg :
forall x:
R,
tan (
- x)
= - tan x.
Lemma tan_minus :
forall x y:
R,
cos x <> 0 ->
cos y <> 0 ->
cos (
x - y)
<> 0 ->
1
+ tan x * tan y <> 0 ->
tan (
x - y)
= (tan x - tan y) / (1
+ tan x * tan y).
Lemma cos_3PI2 :
cos (3
* (PI / 2
))
= 0.
Lemma sin_2PI :
sin (2
* PI)
= 0.
Lemma cos_2PI :
cos (2
* PI)
= 1.
Lemma neg_sin :
forall x:
R,
sin (
x + PI)
= - sin x.
Lemma sin_PI_x :
forall x:
R,
sin (
PI - x)
= sin x.
Lemma sin_period :
forall (
x:
R) (
k:
nat),
sin (
x + 2
* INR k * PI)
= sin x.
Lemma cos_period :
forall (
x:
R) (
k:
nat),
cos (
x + 2
* INR k * PI)
= cos x.
Lemma sin_shift :
forall x:
R,
sin (
PI / 2
- x)
= cos x.
Lemma cos_shift :
forall x:
R,
cos (
PI / 2
- x)
= sin x.
Lemma cos_sin :
forall x:
R,
cos x = sin (
PI / 2
+ x).
Lemma PI2_RGT_0 : 0
< PI / 2.
Lemma SIN_bound :
forall x:
R, -1
<= sin x <= 1.
Lemma COS_bound :
forall x:
R, -1
<= cos x <= 1.
Lemma cos_sin_0 :
forall x:
R,
~ (cos x = 0
/\ sin x = 0
).
Lemma cos_sin_0_var :
forall x:
R,
cos x <> 0
\/ sin x <> 0.
Using series definitions of cos and sin
Increasing and decreasing of cos and sin
Theorem sin_gt_0 :
forall x:
R, 0
< x ->
x < PI -> 0
< sin x.
Theorem cos_gt_0 :
forall x:
R,
- (PI / 2
) < x ->
x < PI / 2 -> 0
< cos x.
Lemma sin_ge_0 :
forall x:
R, 0
<= x ->
x <= PI -> 0
<= sin x.
Lemma cos_ge_0 :
forall x:
R,
- (PI / 2
) <= x ->
x <= PI / 2 -> 0
<= cos x.
Lemma sin_le_0 :
forall x:
R,
PI <= x ->
x <= 2
* PI ->
sin x <= 0.
Lemma cos_le_0 :
forall x:
R,
PI / 2
<= x ->
x <= 3
* (PI / 2
) ->
cos x <= 0.
Lemma sin_lt_0 :
forall x:
R,
PI < x ->
x < 2
* PI ->
sin x < 0.
Lemma sin_lt_0_var :
forall x:
R,
- PI < x ->
x < 0 ->
sin x < 0.
Lemma cos_lt_0 :
forall x:
R,
PI / 2
< x ->
x < 3
* (PI / 2
) ->
cos x < 0.
Lemma tan_gt_0 :
forall x:
R, 0
< x ->
x < PI / 2 -> 0
< tan x.
Lemma tan_lt_0 :
forall x:
R,
- (PI / 2
) < x ->
x < 0 ->
tan x < 0.
Lemma cos_ge_0_3PI2 :
forall x:
R, 3
* (PI / 2
) <= x ->
x <= 2
* PI -> 0
<= cos x.
Lemma form1 :
forall p q:
R,
cos p + cos q = 2
* cos (
(p - q) / 2)
* cos (
(p + q) / 2).
Lemma form2 :
forall p q:
R,
cos p - cos q = -2
* sin (
(p - q) / 2)
* sin (
(p + q) / 2).
Lemma form3 :
forall p q:
R,
sin p + sin q = 2
* cos (
(p - q) / 2)
* sin (
(p + q) / 2).
Lemma form4 :
forall p q:
R,
sin p - sin q = 2
* cos (
(p + q) / 2)
* sin (
(p - q) / 2).
Lemma sin_increasing_0 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
sin x < sin y ->
x < y.
Lemma sin_increasing_1 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
x < y ->
sin x < sin y.
Lemma sin_decreasing_0 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
sin x < sin y ->
y < x.
Lemma sin_decreasing_1 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
x < y ->
sin y < sin x.
Lemma cos_increasing_0 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
cos x < cos y ->
x < y.
Lemma cos_increasing_1 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
x < y ->
cos x < cos y.
Lemma cos_decreasing_0 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
cos x < cos y ->
y < x.
Lemma cos_decreasing_1 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
x < y ->
cos y < cos x.
Lemma tan_diff :
forall x y:
R,
cos x <> 0 ->
cos y <> 0 ->
tan x - tan y = sin (
x - y)
/ (cos x * cos y).
Lemma tan_increasing_0 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
tan x < tan y ->
x < y.
Lemma tan_increasing_1 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
x < y ->
tan x < tan y.
Lemma sin_incr_0 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
sin x <= sin y ->
x <= y.
Lemma sin_incr_1 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
x <= y ->
sin x <= sin y.
Lemma sin_decr_0 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
sin x <= sin y ->
y <= x.
Lemma sin_decr_1 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
x <= y ->
sin y <= sin x.
Lemma cos_incr_0 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
cos x <= cos y ->
x <= y.
Lemma cos_incr_1 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
x <= y ->
cos x <= cos y.
Lemma cos_decr_0 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
cos x <= cos y ->
y <= x.
Lemma cos_decr_1 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
x <= y ->
cos y <= cos x.
Lemma tan_incr_0 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
tan x <= tan y ->
x <= y.
Lemma tan_incr_1 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
x <= y ->
tan x <= tan y.
Lemma sin_eq_0_1 :
forall x:
R, (
exists k : Z, x = IZR k * PI) ->
sin x = 0.
Lemma sin_eq_0_0 :
forall x:
R,
sin x = 0 ->
exists k : Z, x = IZR k * PI.
Lemma cos_eq_0_0 :
forall x:
R,
cos x = 0 ->
exists k : Z, x = IZR k * PI + PI / 2.
ring_simplify.
rewrite <- H3; simpl;
field;repeat split; discrR.