:: 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;