:: by Yuzhong Ding and Xiquan Liang

::

:: Received March 18, 2004

:: Copyright (c) 2004-2021 Association of Mizar Users

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)

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))))

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 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)) )

( 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 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)) )

( 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: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 )

( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 )

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)))

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)

cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1)

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)) )

( 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)) )

( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )

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)))) )

( 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: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)))) )

( 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)))

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)))

cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1)))

proof end;

definition

let x be Real;

coherence

(cosh x) / (sinh x) is Real ;

coherence

1 / (cosh x) is Real ;

coherence

1 / (sinh x) is Real ;

end;
coherence

(cosh x) / (sinh x) is Real ;

coherence

1 / (cosh x) is Real ;

coherence

1 / (sinh x) is Real ;

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))) )

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

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))

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))

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))) )

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

Lm4: for x being Real st x > 0 holds

sinh x >= 0

proof end;