:: Formulas And Identities of Trigonometric Functions
:: by Yuzhong Ding and Xiquan Liang
::
:: Received March 18, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem Th1: :: SIN_COS5:1
for x being real number st cos x <> 0 holds
cosec x = (sec x) / (tan x)
proofend;

theorem Th2: :: SIN_COS5:2
for x being real number st sin x <> 0 holds
cos x = (sin x) * (cot x)
proofend;

theorem :: SIN_COS5:3
for x1, x2, x3 being real number st sin x1 <> 0 &amp; sin x2 <> 0 &amp; sin x3 <> 0 holds
sin ((x1 + x2) + x3) = (((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1)
proofend;

theorem :: SIN_COS5:4
for x1, x2, x3 being real number st sin x1 <> 0 &amp; sin x2 <> 0 &amp; sin x3 <> 0 holds
cos ((x1 + x2) + x3) = - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3))))
proofend;

theorem Th5: :: SIN_COS5:5
for x being real number holds sin (2 * x) = (2 * (sin x)) * (cos x)
proofend;

theorem Th6: :: SIN_COS5:6
for x being real number st cos x <> 0 holds
sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2))
proofend;

theorem Th7: :: SIN_COS5:7
for x being real number holds
( cos (2 * x) = ((cos x) ^2) - ((sin x) ^2) &amp; cos (2 * x) = (2 * ((cos x) ^2)) - 1 &amp; cos (2 * x) = 1 - (2 * ((sin x) ^2)) )
proofend;

theorem Th8: :: SIN_COS5:8
for x being real number st cos x <> 0 holds
cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2))
proofend;

theorem :: SIN_COS5:9
for x being real number st cos x <> 0 holds
tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2))
proofend;

theorem :: SIN_COS5:10
for x being real number st sin x <> 0 holds
cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x))
proofend;

theorem Th11: :: SIN_COS5:11
for x being real number st cos x <> 0 holds
(sec x) ^2 = 1 + ((tan x) ^2)
proofend;

theorem :: SIN_COS5:12
for x being real number holds cot x = 1 / (tan x) by XCMPLX_1:57;

theorem Th13: :: SIN_COS5:13
for x being real number st cos x <> 0 &amp; sin x <> 0 holds
( sec (2 * x) = ((sec x) ^2) / (1 - ((tan x) ^2)) &amp; sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) )
proofend;

theorem :: SIN_COS5:14
for x being real number st sin x <> 0 holds
(cosec x) ^2 = 1 + ((cot x) ^2)
proofend;

theorem :: SIN_COS5:15
for x being real number st cos x <> 0 &amp; sin x <> 0 holds
( cosec (2 * x) = ((sec x) * (cosec x)) / 2 &amp; cosec (2 * x) = ((tan x) + (cot x)) / 2 )
proofend;

theorem Th16: :: SIN_COS5:16
for x being real number holds sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))
proofend;

theorem Th17: :: SIN_COS5:17
for x being real number holds cos (3 * x) = (4 * ((cos x) |^ 3)) - (3 * (cos x))
proofend;

theorem :: SIN_COS5:18
for x being real number st cos x <> 0 holds
tan (3 * x) = ((3 * (tan x)) - ((tan x) |^ 3)) / (1 - (3 * ((tan x) ^2)))
proofend;

theorem :: SIN_COS5:19
for x being real number st sin x <> 0 holds
cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1)
proofend;

theorem :: SIN_COS5:20
for x being real number holds (sin x) ^2 = (1 - (cos (2 * x))) / 2
proofend;

theorem :: SIN_COS5:21
for x being real number holds (cos x) ^2 = (1 + (cos (2 * x))) / 2
proofend;

theorem :: SIN_COS5:22
for x being real number holds (sin x) |^ 3 = ((3 * (sin x)) - (sin (3 * x))) / 4
proofend;

theorem :: SIN_COS5:23
for x being real number holds (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4
proofend;

theorem :: SIN_COS5:24
for x being real number holds (sin x) |^ 4 = ((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
proofend;

theorem :: SIN_COS5:25
for x being real number holds (cos x) |^ 4 = ((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
proofend;

:: Half Angle
theorem :: SIN_COS5:26
for x being real number holds
( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) )
proofend;

theorem :: SIN_COS5:27
for x being real number holds
( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )
proofend;

theorem :: SIN_COS5:28
for x being real number st sin (x / 2) <> 0 holds
tan (x / 2) = (1 - (cos x)) / (sin x)
proofend;

theorem :: SIN_COS5:29
for x being real number st cos (x / 2) <> 0 holds
tan (x / 2) = (sin x) / (1 + (cos x))
proofend;

theorem :: SIN_COS5:30
for x being real number holds
( tan (x / 2) = sqrt ((1 - (cos x)) / (1 + (cos x))) or tan (x / 2) = - (sqrt ((1 - (cos x)) / (1 + (cos x)))) )
proofend;

theorem :: SIN_COS5:31
for x being real number st cos (x / 2) <> 0 holds
cot (x / 2) = (1 + (cos x)) / (sin x)
proofend;

theorem :: SIN_COS5:32
for x being real number st sin (x / 2) <> 0 holds
cot (x / 2) = (sin x) / (1 - (cos x))
proofend;

theorem :: SIN_COS5:33
for x being real number holds
( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) )
proofend;

theorem :: SIN_COS5:34
for x being real number st sin (x / 2) <> 0 &amp; cos (x / 2) <> 0 &amp; 1 - ((tan (x / 2)) ^2) <> 0 &amp; not sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) holds
sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1)))
proofend;

theorem :: SIN_COS5:35
for x being real number st sin (x / 2) <> 0 &amp; cos (x / 2) <> 0 &amp; 1 - ((tan (x / 2)) ^2) <> 0 &amp; not cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) holds
cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1)))
proofend;

definition
let x be real number ;
func coth x ->  Real equals :: SIN_COS5:def 1
(cosh x) / (sinh x);
coherence
 (cosh x) / (sinh x) is Real ;
func sech x ->  Real equals :: SIN_COS5:def 2
1 / (cosh x);
coherence
 1 / (cosh x) is Real ;
func cosech x ->  Real equals :: SIN_COS5:def 3
1 / (sinh x);
coherence
 1 / (sinh x) is Real ;
end;

:: deftheorem  defines coth SIN_COS5:def_1_:_
 for x being real number holds coth x = (cosh x) / (sinh x);

:: deftheorem  defines sech SIN_COS5:def_2_:_
 for x being real number holds sech x = 1 / (cosh x);

:: deftheorem  defines cosech SIN_COS5:def_3_:_
 for x being real number holds cosech x = 1 / (sinh x);

theorem Th36: :: SIN_COS5:36
for x being real number holds
( coth x = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) &amp; sech x = 2 / ((exp_R x) + (exp_R (- x))) &amp; cosech x = 2 / ((exp_R x) - (exp_R (- x))) )
proofend;

theorem :: SIN_COS5:37
for x being real number st (exp_R x) - (exp_R (- x)) <> 0 holds
(tanh x) * (coth x) = 1
proofend;

theorem :: SIN_COS5:38
for x being real number holds ((sech x) ^2) + ((tanh x) ^2) = 1
proofend;

theorem :: SIN_COS5:39
for x being real number st sinh x <> 0 holds
((coth x) ^2) - ((cosech x) ^2) = 1
proofend;

Lm1:  for x being real number holds coth (- x) = - (coth x)
proofend;

theorem Th40: :: SIN_COS5:40
for x1, x2 being real number st sinh x1 <> 0 &amp; sinh x2 <> 0 holds
coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2))
proofend;

theorem :: SIN_COS5:41
for x1, x2 being real number st sinh x1 <> 0 &amp; sinh x2 <> 0 holds
coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2))
proofend;

theorem :: SIN_COS5:42
for x1, x2 being real number st sinh x1 <> 0 &amp; sinh x2 <> 0 holds
( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) &amp; (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) )
proofend;

Lm2:  for x being real number holds (cosh . x) ^2 = 1 + ((sinh . x) ^2)
proofend;

Lm3:  for x being real number holds ((cosh . x) ^2) - 1 = (sinh . x) ^2
proofend;

theorem :: SIN_COS5:43
for x being real number holds sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3))
proofend;

theorem :: SIN_COS5:44
for x being real number holds cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x))
proofend;

theorem :: SIN_COS5:45
for x being real number st sinh x <> 0 holds
coth (2 * x) = (1 + ((coth x) ^2)) / (2 * (coth x))
proofend;

Lm4:  for x being real number st x > 0 holds
sinh x >= 0
proofend;

theorem :: SIN_COS5:46
for x being real number st x >= 0 holds
sinh x >= 0
proofend;

theorem :: SIN_COS5:47
for x being real number st x <= 0 holds
sinh x <= 0
proofend;

theorem :: SIN_COS5:48
for x being real number holds cosh (x / 2) = sqrt (((cosh x) + 1) / 2)
proofend;

theorem :: SIN_COS5:49
for x being real number st sinh (x / 2) <> 0 holds
tanh (x / 2) = ((cosh x) - 1) / (sinh x)
proofend;

theorem :: SIN_COS5:50
for x being real number st cosh (x / 2) <> 0 holds
tanh (x / 2) = (sinh x) / ((cosh x) + 1)
proofend;

theorem :: SIN_COS5:51
for x being real number st sinh (x / 2) <> 0 holds
coth (x / 2) = (sinh x) / ((cosh x) - 1)
proofend;

theorem :: SIN_COS5:52
for x being real number st cosh (x / 2) <> 0 holds
coth (x / 2) = ((cosh x) + 1) / (sinh x)
proofend;