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 (Rmult_comm PI);