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


theorem Th1: :: SIN_COS5:1
for x being Real st cos x <> 0 holds
cosec x = (sec x) / (tan x)
proof end;

theorem Th2: :: SIN_COS5:2
for x being Real st sin x <> 0 holds
cos x = (sin x) * (cot x)
proof end;

theorem :: SIN_COS5:3
for x1, x2, x3 being Real st sin x1 <> 0 & sin x2 <> 0 & 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)
proof end;

theorem :: SIN_COS5:4
for x1, x2, x3 being Real st sin x1 <> 0 & sin x2 <> 0 & 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))))
proof end;

theorem Th5: :: SIN_COS5:5
for x being Real holds sin (2 * x) = (2 * (sin x)) * (cos x)
proof end;

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

theorem Th7: :: SIN_COS5:7
for x being Real holds
( cos (2 * x) = ((cos x) ^2) - ((sin x) ^2) & cos (2 * x) = (2 * ((cos x) ^2)) - 1 & cos (2 * x) = 1 - (2 * ((sin x) ^2)) )
proof end;

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

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

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

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

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

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

theorem :: SIN_COS5:14
for x being Real st sin x <> 0 holds
(cosec x) ^2 = 1 + ((cot x) ^2)
proof end;

theorem :: SIN_COS5:15
for x being Real st cos x <> 0 & sin x <> 0 holds
( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 )
proof end;

theorem Th16: :: SIN_COS5:16
for x being Real holds sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))
proof end;

theorem Th17: :: SIN_COS5:17
for x being Real holds cos (3 * x) = (4 * ((cos x) |^ 3)) - (3 * (cos x))
proof end;

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

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

theorem :: SIN_COS5:20
for x being Real holds (sin x) ^2 = (1 - (cos (2 * x))) / 2
proof end;

theorem :: SIN_COS5:21
for x being Real holds (cos x) ^2 = (1 + (cos (2 * x))) / 2
proof end;

theorem :: SIN_COS5:22
for x being Real holds (sin x) |^ 3 = ((3 * (sin x)) - (sin (3 * x))) / 4
proof end;

theorem :: SIN_COS5:23
for x being Real holds (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4
proof end;

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

theorem :: SIN_COS5:25
for x being Real holds (cos x) |^ 4 = ((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
proof end;

:: Half Angle
theorem :: SIN_COS5:26
for x being Real holds
( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) )
proof end;

theorem :: SIN_COS5:27
for x being Real holds
( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )
proof end;

theorem :: SIN_COS5:28
for x being Real st sin (x / 2) <> 0 holds
tan (x / 2) = (1 - (cos x)) / (sin x)
proof end;

theorem :: SIN_COS5:29
for x being Real st cos (x / 2) <> 0 holds
tan (x / 2) = (sin x) / (1 + (cos x))
proof end;

theorem :: SIN_COS5:30
for x being Real holds
( tan (x / 2) = sqrt ((1 - (cos x)) / (1 + (cos x))) or tan (x / 2) = - (sqrt ((1 - (cos x)) / (1 + (cos x)))) )
proof end;

theorem :: SIN_COS5:31
for x being Real st cos (x / 2) <> 0 holds
cot (x / 2) = (1 + (cos x)) / (sin x)
proof end;

theorem :: SIN_COS5:32
for x being Real st sin (x / 2) <> 0 holds
cot (x / 2) = (sin x) / (1 - (cos x))
proof end;

theorem :: SIN_COS5:33
for x being Real holds
( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) )
proof end;

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

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

definition
let x be Real;
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 holds coth x = (cosh x) / (sinh x);

:: deftheorem defines sech SIN_COS5:def 2 :
for x being Real holds sech x = 1 / (cosh x);

:: deftheorem defines cosech SIN_COS5:def 3 :
for x being Real holds cosech x = 1 / (sinh x);

theorem Th36: :: SIN_COS5:36
for x being Real holds
( coth x = ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) & sech x = 2 / ((exp_R x) + (exp_R (- x))) & cosech x = 2 / ((exp_R x) - (exp_R (- x))) )
proof end;

theorem :: SIN_COS5:37
for x being Real st (exp_R x) - (exp_R (- x)) <> 0 holds
(tanh x) * (coth x) = 1
proof end;

theorem :: SIN_COS5:38
for x being Real holds ((sech x) ^2) + ((tanh x) ^2) = 1
proof end;

theorem :: SIN_COS5:39
for x being Real st sinh x <> 0 holds
((coth x) ^2) - ((cosech x) ^2) = 1
proof end;

Lm1: for x being Real holds coth (- x) = - (coth x)
proof end;

theorem Th40: :: SIN_COS5:40
for x1, x2 being Real st sinh x1 <> 0 & sinh x2 <> 0 holds
coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2))
proof end;

theorem :: SIN_COS5:41
for x1, x2 being Real st sinh x1 <> 0 & sinh x2 <> 0 holds
coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2))
proof end;

theorem :: SIN_COS5:42
for x1, x2 being Real st sinh x1 <> 0 & sinh x2 <> 0 holds
( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) )
proof end;

Lm2: for x being Real holds (cosh . x) ^2 = 1 + ((sinh . x) ^2)
proof end;

Lm3: for x being Real holds ((cosh . x) ^2) - 1 = (sinh . x) ^2
proof end;

theorem :: SIN_COS5:43
for x being Real holds sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3))
proof end;

theorem :: SIN_COS5:44
for x being Real holds cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x))
proof end;

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

Lm4: for x being Real st x > 0 holds
sinh x >= 0
proof end;

theorem :: SIN_COS5:46
for x being Real st x >= 0 holds
sinh x >= 0
proof end;

theorem :: SIN_COS5:47
for x being Real st x <= 0 holds
sinh x <= 0
proof end;

theorem :: SIN_COS5:48
for x being Real holds cosh (x / 2) = sqrt (((cosh x) + 1) / 2)
proof end;

theorem :: SIN_COS5:49
for x being Real st sinh (x / 2) <> 0 holds
tanh (x / 2) = ((cosh x) - 1) / (sinh x)
proof end;

theorem :: SIN_COS5:50
for x being Real st cosh (x / 2) <> 0 holds
tanh (x / 2) = (sinh x) / ((cosh x) + 1)
proof end;

theorem :: SIN_COS5:51
for x being Real st sinh (x / 2) <> 0 holds
coth (x / 2) = (sinh x) / ((cosh x) - 1)
proof end;

theorem :: SIN_COS5:52
for x being Real st cosh (x / 2) <> 0 holds
coth (x / 2) = ((cosh x) + 1) / (sinh x)
proof end;