:: SIN_COS5 semantic presentation

begin


theorem Th1: :: SIN_COS5:1
for x being real number st cos x <> 0 holds
cosec x = (sec x) / (tan x)
proof
let x be real number ; ::_thesis: ( cos x <> 0 implies cosec x = (sec x) / (tan x) )
assume A1: cos x <> 0 ; ::_thesis: cosec x = (sec x) / (tan x)
then (sec x) / (tan x) = ((1 / (cos x)) * (cos x)) / (((sin x) / (cos x)) * (cos x)) by XCMPLX_1:91
.= 1 / (((sin x) / (cos x)) * (cos x)) by A1, XCMPLX_1:87
.= 1 / (sin x) by A1, XCMPLX_1:87 ;
hence  cosec x = (sec x) / (tan x) ; ::_thesis: verum
end;

theorem Th2: :: SIN_COS5:2
for x being real number st sin x <> 0 holds
cos x = (sin x) * (cot x)
proof
let x be real number ; ::_thesis: ( sin x <> 0 implies cos x = (sin x) * (cot x) )
assume  sin x <> 0 ; ::_thesis: cos x = (sin x) * (cot x)
then  cos x = ((sin x) / (sin x)) * (cos x) by XCMPLX_1:88
.= (sin x) * (cot x) by XCMPLX_1:75 ;
hence  cos x = (sin x) * (cot x) ; ::_thesis: verum
end;

theorem :: SIN_COS5:3
for x1, x2, x3 being real number 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
let x1, x2, x3 be real number ; ::_thesis: ( sin x1 <> 0 & sin x2 <> 0 & sin x3 <> 0 implies sin ((x1 + x2) + x3) = (((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1) )
assume that
A1: sin x1 <> 0 and
A2: sin x2 <> 0 and
A3: sin x3 <> 0 ; ::_thesis: 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 + (x2 + x3))
.= ((sin x1) * (cos (x2 + x3))) + ((cos x1) * (sin (x2 + x3))) by SIN_COS:75
.= ((sin x1) * (((cos x2) * (cos x3)) - ((sin x2) * (sin x3)))) + ((cos x1) * (sin (x2 + x3))) by SIN_COS:75
.= (((sin x1) * ((cos x2) * (cos x3))) - ((sin x1) * ((sin x2) * (sin x3)))) + ((cos x1) * (((sin x2) * (cos x3)) + ((cos x2) * (sin x3)))) by SIN_COS:75
.= ((((sin x1) * (cos x2)) * (cos x3)) - (((sin x1) * (sin x2)) * (sin x3))) + ((((cos x1) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3)))
.= ((((sin x1) * ((sin x2) * (cot x2))) * (cos x3)) - (((sin x1) * (sin x2)) * (sin x3))) + ((((cos x1) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3))) by A2, Th2
.= ((((sin x1) * ((sin x2) * (cot x2))) * ((sin x3) * (cot x3))) - (((sin x1) * (sin x2)) * (sin x3))) + ((((cos x1) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3))) by A3, Th2
.= ((((sin x1) * (sin x2)) * (sin x3)) * (((cot x2) * (cot x3)) - 1)) + (((((sin x1) * (cot x1)) * (sin x2)) * (cos x3)) + (((cos x1) * (cos x2)) * (sin x3))) by A1, Th2
.= ((((sin x1) * (sin x2)) * (sin x3)) * (((cot x2) * (cot x3)) - 1)) + (((((sin x1) * (cot x1)) * (sin x2)) * ((sin x3) * (cot x3))) + (((cos x1) * (cos x2)) * (sin x3))) by A3, Th2
.= (((((sin x1) * (sin x2)) * (sin x3)) * (((cot x2) * (cot x3)) - 1)) + (((((sin x1) * (sin x2)) * (sin x3)) * (cot x1)) * (cot x3))) + (((cos x1) * (cos x2)) * (sin x3))
.= ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x2) * (cot x3)) - 1) + ((cot x1) * (cot x3)))) + ((((sin x1) * (cot x1)) * (cos x2)) * (sin x3)) by A1, Th2
.= ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x2) * (cot x3)) - 1) + ((cot x1) * (cot x3)))) + ((((sin x1) * (cot x1)) * ((sin x2) * (cot x2))) * (sin x3)) by A2, Th2
.= (((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1) ;
hence  sin ((x1 + x2) + x3) = (((sin x1) * (sin x2)) * (sin x3)) * (((((cot x2) * (cot x3)) + ((cot x1) * (cot x3))) + ((cot x1) * (cot x2))) - 1) ; ::_thesis: verum
end;

theorem :: SIN_COS5:4
for x1, x2, x3 being real number 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
let x1, x2, x3 be real number ; ::_thesis: ( sin x1 <> 0 & sin x2 <> 0 & sin x3 <> 0 implies cos ((x1 + x2) + x3) = - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3)))) )
assume that
A1: sin x1 <> 0 and
A2: sin x2 <> 0 and
A3: sin x3 <> 0 ; ::_thesis: 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) = cos (x1 + (x2 + x3))
.= ((cos x1) * (cos (x2 + x3))) - ((sin x1) * (sin (x2 + x3))) by SIN_COS:75
.= ((cos x1) * (((cos x2) * (cos x3)) - ((sin x2) * (sin x3)))) - ((sin x1) * (sin (x2 + x3))) by SIN_COS:75
.= (((cos x1) * ((cos x2) * (cos x3))) - ((cos x1) * ((sin x2) * (sin x3)))) - ((sin x1) * (((sin x2) * (cos x3)) + ((cos x2) * (sin x3)))) by SIN_COS:75
.= ((((cos x1) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (cos x3)) + (((sin x1) * (sin x3)) * (cos x2)))
.= ((((cos x1) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * ((sin x3) * (cot x3))) + (((sin x1) * (sin x3)) * (cos x2))) by A3, Th2
.= ((((cos x1) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * ((sin x3) * (cot x3))) + (((sin x1) * (sin x3)) * ((sin x2) * (cot x2)))) by A2, Th2
.= (((((sin x1) * (cot x1)) * (cos x2)) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A1, Th2
.= (((((sin x1) * (cot x1)) * ((sin x2) * (cot x2))) * (cos x3)) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A2, Th2
.= (((((sin x1) * (cot x1)) * ((sin x2) * (cot x2))) * ((sin x3) * (cot x3))) - (((cos x1) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A3, Th2
.= (((((sin x1) * (sin x2)) * (sin x3)) * (((cot x1) * (cot x2)) * (cot x3))) - ((((sin x1) * (cot x1)) * (sin x2)) * (sin x3))) - ((((sin x1) * (sin x2)) * (sin x3)) * ((cot x3) + (cot x2))) by A1, Th2
.= - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3)))) ;
hence  cos ((x1 + x2) + x3) = - ((((sin x1) * (sin x2)) * (sin x3)) * ((((cot x1) + (cot x2)) + (cot x3)) - (((cot x1) * (cot x2)) * (cot x3)))) ; ::_thesis: verum
end;

theorem Th5: :: SIN_COS5:5
for x being real number holds sin (2 * x) = (2 * (sin x)) * (cos x)
proof
let x be real number ; ::_thesis: sin (2 * x) = (2 * (sin x)) * (cos x)
sin (2 * x) = sin (x + x)
.= ((sin x) * (cos x)) + ((cos x) * (sin x)) by SIN_COS:75
.= (2 * (sin x)) * (cos x) ;
hence  sin (2 * x) = (2 * (sin x)) * (cos x) ; ::_thesis: verum
end;

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))
proof
let x be real number ; ::_thesis: ( cos x <> 0 implies sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2)) )
assume A1: cos x <> 0 ; ::_thesis: sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2))
then A2: (cos x) ^2 <> 0 by SQUARE_1:12;
sin (2 * x) = ((2 * (sin x)) * (cos x)) * 1 by Th5
.= ((2 * (sin x)) * (cos x)) * ((cos x) / (cos x)) by A1, XCMPLX_1:60
.= (((2 * (sin x)) * (cos x)) * (cos x)) / (cos x) by XCMPLX_1:74
.= ((2 * ((cos x) ^2)) * (sin x)) / (cos x)
.= ((2 * ((cos x) ^2)) * (tan x)) / 1 by XCMPLX_1:74
.= ((2 * (tan x)) * ((cos x) ^2)) / (((sin x) ^2) + ((cos x) ^2)) by SIN_COS:29
.= (2 * (tan x)) / ((((sin x) ^2) + ((cos x) ^2)) / ((cos x) ^2)) by XCMPLX_1:77
.= (2 * (tan x)) / ((((sin x) ^2) / ((cos x) ^2)) + (((cos x) ^2) / ((cos x) ^2))) by XCMPLX_1:62
.= (2 * (tan x)) / ((((sin x) ^2) / ((cos x) ^2)) + 1) by A2, XCMPLX_1:60
.= (2 * (tan x)) / (((tan x) ^2) + 1) by XCMPLX_1:76 ;
hence  sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2)) ; ::_thesis: verum
end;

theorem Th7: :: SIN_COS5:7
for x being real number 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
let x be real number ; ::_thesis: ( 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)) )
A1: cos (2 * x) = cos (x + x)
.= ((cos x) ^2) - ((sin x) ^2) by SIN_COS:75 ;
then  cos (2 * x) = ((((cos x) ^2) - ((sin x) ^2)) - 1) + 1
.= ((((cos x) ^2) - ((sin x) ^2)) - (((cos x) ^2) + ((sin x) ^2))) + 1 by SIN_COS:29
.= - ((- 1) + (2 * ((sin x) ^2))) ;
hence  ( 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)) ) by A1; ::_thesis: verum
end;

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))
proof
let x be real number ; ::_thesis: ( cos x <> 0 implies cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) )
assume  cos x <> 0 ; ::_thesis: cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2))
then A1: (cos x) ^2 <> 0 by SQUARE_1:12;
cos (2 * x) = (((cos x) ^2) - ((sin x) ^2)) * 1 by Th7
.= (((cos x) ^2) - ((sin x) ^2)) * (((cos x) ^2) / ((cos x) ^2)) by A1, XCMPLX_1:60
.= ((((cos x) ^2) - ((sin x) ^2)) / ((cos x) ^2)) * ((cos x) ^2) by XCMPLX_1:75
.= ((((cos x) ^2) / ((cos x) ^2)) - (((sin x) ^2) / ((cos x) ^2))) * ((cos x) ^2) by XCMPLX_1:120
.= (1 - (((sin x) ^2) / ((cos x) ^2))) * ((cos x) ^2) by A1, XCMPLX_1:60
.= ((1 - ((tan x) ^2)) * ((cos x) ^2)) / 1 by XCMPLX_1:76
.= ((1 - ((tan x) ^2)) * ((cos x) ^2)) / (((cos x) ^2) + ((sin x) ^2)) by SIN_COS:29
.= (1 - ((tan x) ^2)) / ((((cos x) ^2) + ((sin x) ^2)) / ((cos x) ^2)) by XCMPLX_1:77
.= (1 - ((tan x) ^2)) / ((((cos x) ^2) / ((cos x) ^2)) + (((sin x) ^2) / ((cos x) ^2))) by XCMPLX_1:62
.= (1 - ((tan x) ^2)) / (1 + (((sin x) ^2) / ((cos x) ^2))) by A1, XCMPLX_1:60
.= (1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) by XCMPLX_1:76 ;
hence  cos (2 * x) = (1 - ((tan x) ^2)) / (1 + ((tan x) ^2)) ; ::_thesis: verum
end;

theorem :: SIN_COS5:9
for x being real number st cos x <> 0 holds
tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2))
proof
let x be real number ; ::_thesis: ( cos x <> 0 implies tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2)) )
assume A1: cos x <> 0 ; ::_thesis: tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2))
tan (2 * x) = tan (x + x)
.= ((tan x) + (tan x)) / (1 - ((tan x) * (tan x))) by A1, SIN_COS4:7
.= (2 * (tan x)) / (1 - ((tan x) * (tan x))) ;
hence  tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2)) ; ::_thesis: verum
end;

theorem :: SIN_COS5:10
for x being real number st sin x <> 0 holds
cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x))
proof
let x be real number ; ::_thesis: ( sin x <> 0 implies cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x)) )
assume A1: sin x <> 0 ; ::_thesis: cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x))
cot (2 * x) = cot (x + x)
.= (((cot x) * (cot x)) - 1) / ((cot x) + (cot x)) by A1, SIN_COS4:9
.= (((cot x) * (cot x)) - 1) / (2 * (cot x)) ;
hence  cot (2 * x) = (((cot x) ^2) - 1) / (2 * (cot x)) ; ::_thesis: verum
end;

theorem Th11: :: SIN_COS5:11
for x being real number st cos x <> 0 holds
(sec x) ^2 = 1 + ((tan x) ^2)
proof
let x be real number ; ::_thesis: ( cos x <> 0 implies (sec x) ^2 = 1 + ((tan x) ^2) )
assume  cos x <> 0 ; ::_thesis: (sec x) ^2 = 1 + ((tan x) ^2)
then A1: (cos x) ^2 <> 0 by SQUARE_1:12;
(sec x) ^2 = (1 ^2) / ((cos x) ^2) by XCMPLX_1:76
.= (((sin x) ^2) + ((cos x) ^2)) / ((cos x) ^2) by SIN_COS:29
.= (((sin x) ^2) / ((cos x) ^2)) + (((cos x) ^2) / ((cos x) ^2)) by XCMPLX_1:62
.= (((sin x) ^2) / ((cos x) ^2)) + 1 by A1, XCMPLX_1:60
.= (((sin x) / (cos x)) ^2) + 1 by XCMPLX_1:76 ;
hence  (sec x) ^2 = 1 + ((tan x) ^2) ; ::_thesis: verum
end;

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 & 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
let x be real number ; ::_thesis: ( cos x <> 0 & sin x <> 0 implies ( sec (2 * x) = ((sec x) ^2) / (1 - ((tan x) ^2)) & sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) ) )
assume that
A1: cos x <> 0 and
A2: sin x <> 0 ; ::_thesis: ( sec (2 * x) = ((sec x) ^2) / (1 - ((tan x) ^2)) & sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) )
A3: sec (2 * x) = 1 / ((1 - ((tan x) ^2)) / (1 + ((tan x) ^2))) by A1, Th8
.= (1 + ((tan x) ^2)) / (1 - ((tan x) ^2)) by XCMPLX_1:57
.= ((sec x) ^2) / (1 - ((tan x) ^2)) by A1, Th11 ;
then  sec (2 * x) = (1 + ((tan x) ^2)) / (1 - ((tan x) ^2)) by A1, Th11
.= ((1 + ((tan x) ^2)) / (tan x)) / ((1 - ((tan x) ^2)) / (tan x)) by A1, A2, XCMPLX_1:50, XCMPLX_1:55
.= ((1 / (tan x)) + (((tan x) ^2) / (tan x))) / ((1 - ((tan x) ^2)) / (tan x)) by XCMPLX_1:62
.= ((cot x) + (((tan x) ^2) / (tan x))) / ((1 - ((tan x) ^2)) / (tan x)) by XCMPLX_1:57
.= ((cot x) + (((tan x) ^2) / (tan x))) / ((1 / (tan x)) - (((tan x) ^2) / (tan x))) by XCMPLX_1:120
.= ((cot x) + (((tan x) * (tan x)) / (tan x))) / ((cot x) - (((tan x) ^2) / (tan x))) by XCMPLX_1:57
.= ((cot x) + (tan x)) / ((cot x) - (((tan x) * (tan x)) / (tan x))) by A1, A2, XCMPLX_1:50, XCMPLX_1:89 ;
hence  ( sec (2 * x) = ((sec x) ^2) / (1 - ((tan x) ^2)) & sec (2 * x) = ((cot x) + (tan x)) / ((cot x) - (tan x)) ) by A1, A2, A3, XCMPLX_1:50, XCMPLX_1:89; ::_thesis: verum
end;

theorem :: SIN_COS5:14
for x being real number st sin x <> 0 holds
(cosec x) ^2 = 1 + ((cot x) ^2)
proof
let x be real number ; ::_thesis: ( sin x <> 0 implies (cosec x) ^2 = 1 + ((cot x) ^2) )
assume  sin x <> 0 ; ::_thesis: (cosec x) ^2 = 1 + ((cot x) ^2)
then A1: (sin x) ^2 <> 0 by SQUARE_1:12;
(cosec x) ^2 = (1 ^2) / ((sin x) ^2) by XCMPLX_1:76
.= (((sin x) ^2) + ((cos x) ^2)) / ((sin x) ^2) by SIN_COS:29
.= (((sin x) ^2) / ((sin x) ^2)) + (((cos x) ^2) / ((sin x) ^2)) by XCMPLX_1:62
.= 1 + (((cos x) ^2) / ((sin x) ^2)) by A1, XCMPLX_1:60
.= 1 + (((cos x) / (sin x)) ^2) by XCMPLX_1:76 ;
hence  (cosec x) ^2 = 1 + ((cot x) ^2) ; ::_thesis: verum
end;

theorem :: SIN_COS5:15
for x being real number 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
let x be real number ; ::_thesis: ( cos x <> 0 & sin x <> 0 implies ( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 ) )
assume that
A1: cos x <> 0 and
A2: sin x <> 0 ; ::_thesis: ( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 )
A3: cosec (2 * x) = 1 / ((2 * (tan x)) / (1 + ((tan x) ^2))) by A1, Th6
.= (1 + ((tan x) ^2)) / (2 * (tan x)) by XCMPLX_1:57
.= ((1 + ((tan x) ^2)) / (tan x)) / 2 by XCMPLX_1:78
.= ((1 / ((sin x) / (cos x))) + (((tan x) ^2) / (tan x))) / 2 by XCMPLX_1:62
.= ((cot x) + (((tan x) * (tan x)) / (tan x))) / 2 by XCMPLX_1:57
.= ((cot x) + (tan x)) / 2 by A1, A2, XCMPLX_1:50, XCMPLX_1:89 ;
cosec (2 * x) = 1 / ((2 * (tan x)) / (1 + ((tan x) ^2))) by A1, Th6
.= (1 + ((tan x) ^2)) / (2 * (tan x)) by XCMPLX_1:57
.= ((sec x) ^2) / (2 * (tan x)) by A1, Th11
.= (((sec x) * (sec x)) / (tan x)) / 2 by XCMPLX_1:78
.= ((sec x) * ((sec x) / ((sin x) / (cos x)))) / 2 by XCMPLX_1:74
.= ((sec x) * (((sec x) * (cos x)) / (sin x))) / 2 by XCMPLX_1:77
.= ((sec x) * (cosec x)) / 2 by A1, XCMPLX_1:106 ;
hence  ( cosec (2 * x) = ((sec x) * (cosec x)) / 2 & cosec (2 * x) = ((tan x) + (cot x)) / 2 ) by A3; ::_thesis: verum
end;

theorem Th16: :: SIN_COS5:16
for x being real number holds sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))
proof
let x be real number ; ::_thesis: sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))
sin (3 * x) = sin ((x + x) + x)
.= ((sin (2 * x)) * (cos x)) + ((cos (x + x)) * (sin x)) by SIN_COS:75
.= (((2 * (sin x)) * (cos x)) * (cos x)) + ((cos (2 * x)) * (sin x)) by Th5
.= ((2 * (sin x)) * ((cos x) * (cos x))) + ((1 - (2 * ((sin x) ^2))) * (sin x)) by Th7
.= ((2 * (sin x)) * (1 - ((sin x) ^2))) + ((1 - (2 * ((sin x) ^2))) * (sin x)) by SIN_COS4:5
.= (((2 * (sin x)) * 1) - ((2 * (sin x)) * ((sin x) * (sin x)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)))
.= (((2 * (sin x)) * 1) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) by NEWTON:5
.= (((2 * (sin x)) * 1) - ((2 * ((sin x) |^ (1 + 1))) * (sin x))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) by NEWTON:6
.= (((2 * (sin x)) * 1) - (2 * (((sin x) |^ 2) * (sin x)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x)))
.= (((2 * (sin x)) * 1) - (2 * ((sin x) |^ (2 + 1)))) + ((1 * (sin x)) - ((2 * ((sin x) ^2)) * (sin x))) by NEWTON:6
.= ((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - ((2 * (((sin x) |^ 1) * (sin x))) * (sin x))) by NEWTON:5
.= ((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - ((2 * ((sin x) |^ (1 + 1))) * (sin x))) by NEWTON:6
.= ((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - (2 * (((sin x) |^ (1 + 1)) * (sin x))))
.= ((2 * (sin x)) - (2 * ((sin x) |^ 3))) + ((sin x) - (2 * ((sin x) |^ (2 + 1)))) by NEWTON:6
.= - ((- (3 * (sin x))) + (4 * ((sin x) |^ 3))) ;
hence  sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x)) ; ::_thesis: verum
end;

theorem Th17: :: SIN_COS5:17
for x being real number holds cos (3 * x) = (4 * ((cos x) |^ 3)) - (3 * (cos x))
proof
let x be real number ; ::_thesis: cos (3 * x) = (4 * ((cos x) |^ 3)) - (3 * (cos x))
cos (3 * x) = cos ((x + x) + x)
.= ((cos (2 * x)) * (cos x)) - ((sin (x + x)) * (sin x)) by SIN_COS:75
.= (((2 * ((cos x) ^2)) - 1) * (cos x)) - ((sin (2 * x)) * (sin x)) by Th7
.= ((2 * (((cos x) * (cos x)) * (cos x))) - (1 * (cos x))) - ((sin (2 * x)) * (sin x))
.= ((2 * ((((cos x) |^ 1) * (cos x)) * (cos x))) - (1 * (cos x))) - ((sin (2 * x)) * (sin x)) by NEWTON:5
.= ((2 * (((cos x) |^ (1 + 1)) * (cos x))) - (1 * (cos x))) - ((sin (2 * x)) * (sin x)) by NEWTON:6
.= ((2 * ((cos x) |^ (2 + 1))) - (cos x)) - ((sin (2 * x)) * (sin x)) by NEWTON:6
.= ((2 * ((cos x) |^ 3)) - (cos x)) - (((2 * (sin x)) * (cos x)) * (sin x)) by Th5
.= ((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) * ((sin x) * (sin x)))
.= ((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) * (1 - ((cos x) * (cos x)))) by SIN_COS4:4
.= ((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * (((cos x) * (cos x)) * (cos x))))
.= ((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * ((((cos x) |^ 1) * (cos x)) * (cos x)))) by NEWTON:5
.= ((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * (((cos x) |^ (1 + 1)) * (cos x)))) by NEWTON:6
.= ((2 * ((cos x) |^ 3)) - (cos x)) - ((2 * (cos x)) - (2 * ((cos x) |^ (2 + 1)))) by NEWTON:6
.= ((2 * ((cos x) |^ 3)) + (2 * ((cos x) |^ 3))) - (3 * (cos x)) ;
hence  cos (3 * x) = (4 * ((cos x) |^ 3)) - (3 * (cos x)) ; ::_thesis: verum
end;

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)))
proof
let x be real number ; ::_thesis: ( cos x <> 0 implies tan (3 * x) = ((3 * (tan x)) - ((tan x) |^ 3)) / (1 - (3 * ((tan x) ^2))) )
assume A1: cos x <> 0 ; ::_thesis: tan (3 * x) = ((3 * (tan x)) - ((tan x) |^ 3)) / (1 - (3 * ((tan x) ^2)))
tan (3 * x) = tan ((x + x) + x)
.= ((((tan x) + (tan x)) + (tan x)) - (((tan x) * (tan x)) * (tan x))) / (((1 - ((tan x) * (tan x))) - ((tan x) * (tan x))) - ((tan x) * (tan x))) by A1, SIN_COS4:13
.= ((3 * (tan x)) - ((((tan x) |^ 1) * (tan x)) * (tan x))) / (1 - ((3 * (tan x)) * (tan x))) by NEWTON:5
.= ((3 * (tan x)) - (((tan x) |^ (1 + 1)) * (tan x))) / (1 - ((3 * (tan x)) * (tan x))) by NEWTON:6
.= ((3 * (tan x)) - ((tan x) |^ (2 + 1))) / (1 - (3 * ((tan x) * (tan x)))) by NEWTON:6 ;
hence  tan (3 * x) = ((3 * (tan x)) - ((tan x) |^ 3)) / (1 - (3 * ((tan x) ^2))) ; ::_thesis: verum
end;

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)
proof
let x be real number ; ::_thesis: ( sin x <> 0 implies cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) )
assume A1: sin x <> 0 ; ::_thesis: cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1)
cot (3 * x) = cot ((x + x) + x)
.= ((((((cot x) * (cot x)) * (cot x)) - (cot x)) - (cot x)) - (cot x)) / (((((cot x) * (cot x)) + ((cot x) * (cot x))) + ((cot x) * (cot x))) - 1) by A1, SIN_COS4:14
.= ((((cot x) * (cot x)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1)
.= (((((cot x) |^ 1) * (cot x)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) by NEWTON:5
.= ((((cot x) |^ (1 + 1)) * (cot x)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) by NEWTON:6
.= (((cot x) |^ (2 + 1)) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) by NEWTON:6 ;
hence  cot (3 * x) = (((cot x) |^ 3) - (3 * (cot x))) / ((3 * ((cot x) ^2)) - 1) ; ::_thesis: verum
end;

theorem :: SIN_COS5:20
for x being real number holds (sin x) ^2 = (1 - (cos (2 * x))) / 2
proof
let x be real number ; ::_thesis: (sin x) ^2 = (1 - (cos (2 * x))) / 2
(1 - (cos (2 * x))) / 2 = (1 - (1 - (2 * ((sin x) ^2)))) / 2 by Th7
.= (((sin x) ^2) * 2) / 2 ;
hence  (sin x) ^2 = (1 - (cos (2 * x))) / 2 ; ::_thesis: verum
end;

theorem :: SIN_COS5:21
for x being real number holds (cos x) ^2 = (1 + (cos (2 * x))) / 2
proof
let x be real number ; ::_thesis: (cos x) ^2 = (1 + (cos (2 * x))) / 2
(1 + (cos (2 * x))) / 2 = (1 + ((2 * ((cos x) ^2)) - 1)) / 2 by Th7
.= (((cos x) ^2) * 2) / 2 ;
hence  (cos x) ^2 = (1 + (cos (2 * x))) / 2 ; ::_thesis: verum
end;

theorem :: SIN_COS5:22
for x being real number holds (sin x) |^ 3 = ((3 * (sin x)) - (sin (3 * x))) / 4
proof
let x be real number ; ::_thesis: (sin x) |^ 3 = ((3 * (sin x)) - (sin (3 * x))) / 4
((3 * (sin x)) - (sin (3 * x))) / 4 = ((3 * (sin x)) - ((- (4 * ((sin x) |^ 3))) + (3 * (sin x)))) / 4 by Th16
.= (4 * ((sin x) |^ 3)) / 4 ;
hence  (sin x) |^ 3 = ((3 * (sin x)) - (sin (3 * x))) / 4 ; ::_thesis: verum
end;

theorem :: SIN_COS5:23
for x being real number holds (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4
proof
let x be real number ; ::_thesis: (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4
((3 * (cos x)) + (cos (3 * x))) / 4 = ((3 * (cos x)) + ((4 * ((cos x) |^ 3)) - (3 * (cos x)))) / 4 by Th17
.= (4 * ((cos x) |^ 3)) / 4 ;
hence  (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4 ; ::_thesis: verum
end;

theorem :: SIN_COS5:24
for x being real number holds (sin x) |^ 4 = ((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
proof
let x be real number ; ::_thesis: (sin x) |^ 4 = ((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
((3 - (4 * (cos (2 * x)))) + (cos ((2 * 2) * x))) / 8 = ((3 - (4 * (cos (2 * x)))) + (cos (2 * (2 * x)))) / 8
.= ((3 - (4 * (cos (2 * x)))) + (1 - (2 * ((sin (2 * x)) ^2)))) / 8 by Th7
.= ((3 - (4 * (cos (2 * x)))) + (1 - (2 * (((2 * (sin x)) * (cos x)) ^2)))) / 8 by Th5
.= ((3 - (4 * (1 - (2 * ((sin x) ^2))))) + (1 - ((8 * ((sin x) ^2)) * ((cos x) ^2)))) / 8 by Th7
.= ((sin x) ^2) * (1 - ((cos x) * (cos x)))
.= ((sin x) * (sin x)) * ((sin x) * (sin x)) by SIN_COS4:4
.= (((sin x) |^ 1) * (sin x)) * ((sin x) * (sin x)) by NEWTON:5
.= ((sin x) |^ (1 + 1)) * ((sin x) * (sin x)) by NEWTON:6
.= (((sin x) |^ (1 + 1)) * (sin x)) * (sin x)
.= ((sin x) |^ (2 + 1)) * (sin x) by NEWTON:6
.= (sin x) |^ (3 + 1) by NEWTON:6 ;
hence  (sin x) |^ 4 = ((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8 ; ::_thesis: verum
end;

theorem :: SIN_COS5:25
for x being real number holds (cos x) |^ 4 = ((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
proof
let x be real number ; ::_thesis: (cos x) |^ 4 = ((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8 = ((3 + (4 * (cos (2 * x)))) + (cos (2 * (2 * x)))) / 8
.= ((3 + (4 * (cos (2 * x)))) + (1 - (2 * ((sin (2 * x)) ^2)))) / 8 by Th7
.= ((3 + (4 * (cos (2 * x)))) + (1 - (2 * (((2 * (sin x)) * (cos x)) ^2)))) / 8 by Th5
.= ((3 + (4 * (1 - (2 * ((sin x) ^2))))) + (1 - ((8 * ((sin x) ^2)) * ((cos x) ^2)))) / 8 by Th7
.= 1 - (((sin x) * (sin x)) * (1 + ((cos x) ^2)))
.= 1 - (((1 ^2) - ((cos x) ^2)) * ((1 ^2) + ((cos x) ^2))) by SIN_COS4:4
.= (((cos x) * (cos x)) * (cos x)) * (cos x)
.= ((((cos x) |^ 1) * (cos x)) * (cos x)) * (cos x) by NEWTON:5
.= (((cos x) |^ (1 + 1)) * (cos x)) * (cos x) by NEWTON:6
.= ((cos x) |^ (2 + 1)) * (cos x) by NEWTON:6
.= (cos x) |^ (3 + 1) by NEWTON:6 ;
hence  (cos x) |^ 4 = ((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8 ; ::_thesis: verum
end;

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)) )
proof
let x be real number ; ::_thesis: ( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) )
A1: sqrt ((1 - (cos x)) / 2) = sqrt ((1 - (cos (2 * (x / 2)))) / 2)
.= sqrt ((1 - (1 - (2 * ((sin (x / 2)) ^2)))) / 2) by Th7
.= abs (sin (x / 2)) by COMPLEX1:72 ;
percases ( sin (x / 2) >= 0 or sin (x / 2) < 0 ) ;
suppose sin (x / 2) >= 0 ; ::_thesis: ( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) )
hence  ( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) ) by A1, ABSVALUE:def_1; ::_thesis: verum
end;
suppose sin (x / 2) < 0 ; ::_thesis: ( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) )
then  (sqrt ((1 - (cos x)) / 2)) * (- 1) = (- (sin (x / 2))) * (- 1) by A1, ABSVALUE:def_1;
hence  ( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) ) ; ::_thesis: verum
end;
end;
end;

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)) )
proof
let x be real number ; ::_thesis: ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )
A1: sqrt ((1 + (cos x)) / 2) = sqrt ((1 + (cos (2 * (x / 2)))) / 2)
.= sqrt ((1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / 2) by Th7
.= abs (cos (x / 2)) by COMPLEX1:72 ;
percases ( cos (x / 2) >= 0 or cos (x / 2) < 0 ) ;
suppose cos (x / 2) >= 0 ; ::_thesis: ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )
hence  ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) ) by A1, ABSVALUE:def_1; ::_thesis: verum
end;
suppose cos (x / 2) < 0 ; ::_thesis: ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )
then  (sqrt ((1 + (cos x)) / 2)) * (- 1) = (- (cos (x / 2))) * (- 1) by A1, ABSVALUE:def_1;
hence  ( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) ) ; ::_thesis: verum
end;
end;
end;

theorem :: SIN_COS5:28
for x being real number st sin (x / 2) <> 0 holds
tan (x / 2) = (1 - (cos x)) / (sin x)
proof
let x be real number ; ::_thesis: ( sin (x / 2) <> 0 implies tan (x / 2) = (1 - (cos x)) / (sin x) )
assume  sin (x / 2) <> 0 ; ::_thesis: tan (x / 2) = (1 - (cos x)) / (sin x)
then A1: 2 * (sin (x / 2)) <> 0 ;
(1 - (cos x)) / (sin x) = (1 - (1 - (2 * ((sin (x / 2)) ^2)))) / (sin (2 * (x / 2))) by Th7
.= ((2 * (sin (x / 2))) * (sin (x / 2))) / ((2 * (sin (x / 2))) * (cos (x / 2))) by Th5
.= tan (x / 2) by A1, XCMPLX_1:91 ;
hence  tan (x / 2) = (1 - (cos x)) / (sin x) ; ::_thesis: verum
end;

theorem :: SIN_COS5:29
for x being real number st cos (x / 2) <> 0 holds
tan (x / 2) = (sin x) / (1 + (cos x))
proof
let x be real number ; ::_thesis: ( cos (x / 2) <> 0 implies tan (x / 2) = (sin x) / (1 + (cos x)) )
assume  cos (x / 2) <> 0 ; ::_thesis: tan (x / 2) = (sin x) / (1 + (cos x))
then A1: 2 * (cos (x / 2)) <> 0 ;
(sin x) / (1 + (cos x)) = ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 + (cos (2 * (x / 2)))) by Th5
.= ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 + ((2 * ((cos (x / 2)) ^2)) - 1)) by Th7
.= ((2 * (cos (x / 2))) * (sin (x / 2))) / ((2 * (cos (x / 2))) * (cos (x / 2)))
.= (sin (x / 2)) / (cos (x / 2)) by A1, XCMPLX_1:91 ;
hence  tan (x / 2) = (sin x) / (1 + (cos x)) ; ::_thesis: verum
end;

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)))) )
proof
let x be real number ; ::_thesis: ( tan (x / 2) = sqrt ((1 - (cos x)) / (1 + (cos x))) or tan (x / 2) = - (sqrt ((1 - (cos x)) / (1 + (cos x)))) )
A1: sqrt ((1 - (cos x)) / (1 + (cos x))) = sqrt ((1 - (1 - (2 * ((sin (x / 2)) ^2)))) / (1 + (cos (2 * (x / 2))))) by Th7
.= sqrt (((1 - 1) + (2 * ((sin (x / 2)) ^2))) / (1 + ((2 * ((cos (x / 2)) ^2)) - 1))) by Th7
.= sqrt (((sin (x / 2)) ^2) / ((cos (x / 2)) ^2)) by XCMPLX_1:91
.= sqrt ((tan (x / 2)) ^2) by XCMPLX_1:76
.= abs (tan (x / 2)) by COMPLEX1:72 ;
percases ( tan (x / 2) >= 0 or tan (x / 2) < 0 ) ;
suppose tan (x / 2) >= 0 ; ::_thesis: ( tan (x / 2) = sqrt ((1 - (cos x)) / (1 + (cos x))) or tan (x / 2) = - (sqrt ((1 - (cos x)) / (1 + (cos x)))) )
hence  ( tan (x / 2) = sqrt ((1 - (cos x)) / (1 + (cos x))) or tan (x / 2) = - (sqrt ((1 - (cos x)) / (1 + (cos x)))) ) by A1, ABSVALUE:def_1; ::_thesis: verum
end;
suppose tan (x / 2) < 0 ; ::_thesis: ( tan (x / 2) = sqrt ((1 - (cos x)) / (1 + (cos x))) or tan (x / 2) = - (sqrt ((1 - (cos x)) / (1 + (cos x)))) )
then  (sqrt ((1 - (cos x)) / (1 + (cos x)))) * (- 1) = (- (tan (x / 2))) * (- 1) by A1, ABSVALUE:def_1;
hence  ( tan (x / 2) = sqrt ((1 - (cos x)) / (1 + (cos x))) or tan (x / 2) = - (sqrt ((1 - (cos x)) / (1 + (cos x)))) ) ; ::_thesis: verum
end;
end;
end;

theorem :: SIN_COS5:31
for x being real number st cos (x / 2) <> 0 holds
cot (x / 2) = (1 + (cos x)) / (sin x)
proof
let x be real number ; ::_thesis: ( cos (x / 2) <> 0 implies cot (x / 2) = (1 + (cos x)) / (sin x) )
assume  cos (x / 2) <> 0 ; ::_thesis: cot (x / 2) = (1 + (cos x)) / (sin x)
then A1: 2 * (cos (x / 2)) <> 0 ;
(1 + (cos x)) / (sin x) = (1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / (sin (2 * (x / 2))) by Th7
.= (2 * ((cos (x / 2)) * (cos (x / 2)))) / ((2 * (sin (x / 2))) * (cos (x / 2))) by Th5
.= ((2 * (cos (x / 2))) * (cos (x / 2))) / ((2 * (cos (x / 2))) * (sin (x / 2)))
.= cot (x / 2) by A1, XCMPLX_1:91 ;
hence  cot (x / 2) = (1 + (cos x)) / (sin x) ; ::_thesis: verum
end;

theorem :: SIN_COS5:32
for x being real number st sin (x / 2) <> 0 holds
cot (x / 2) = (sin x) / (1 - (cos x))
proof
let x be real number ; ::_thesis: ( sin (x / 2) <> 0 implies cot (x / 2) = (sin x) / (1 - (cos x)) )
assume  sin (x / 2) <> 0 ; ::_thesis: cot (x / 2) = (sin x) / (1 - (cos x))
then A1: 2 * (sin (x / 2)) <> 0 ;
(sin x) / (1 - (cos x)) = ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (cos (2 * (x / 2)))) by Th5
.= ((2 * (sin (x / 2))) * (cos (x / 2))) / (1 - (1 - (2 * ((sin (x / 2)) ^2)))) by Th7
.= ((2 * (sin (x / 2))) * (cos (x / 2))) / ((2 * (sin (x / 2))) * (sin (x / 2)))
.= (cos (x / 2)) / (sin (x / 2)) by A1, XCMPLX_1:91 ;
hence  cot (x / 2) = (sin x) / (1 - (cos x)) ; ::_thesis: verum
end;

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)))) )
proof
let x be real number ; ::_thesis: ( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) )
A1: sqrt ((1 + (cos x)) / (1 - (cos x))) = sqrt ((1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / (1 - (cos (2 * (x / 2))))) by Th7
.= sqrt ((1 - (1 - (2 * ((cos (x / 2)) ^2)))) / (1 - (1 - (2 * ((sin (x / 2)) ^2))))) by Th7
.= sqrt (((cos (x / 2)) ^2) / ((sin (x / 2)) ^2)) by XCMPLX_1:91
.= sqrt ((cot (x / 2)) ^2) by XCMPLX_1:76
.= abs (cot (x / 2)) by COMPLEX1:72 ;
percases ( cot (x / 2) >= 0 or cot (x / 2) < 0 ) ;
suppose cot (x / 2) >= 0 ; ::_thesis: ( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) )
hence  ( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) ) by A1, ABSVALUE:def_1; ::_thesis: verum
end;
suppose cot (x / 2) < 0 ; ::_thesis: ( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) )
then  (sqrt ((1 + (cos x)) / (1 - (cos x)))) * (- 1) = (- (cot (x / 2))) * (- 1) by A1, ABSVALUE:def_1;
hence  ( cot (x / 2) = sqrt ((1 + (cos x)) / (1 - (cos x))) or cot (x / 2) = - (sqrt ((1 + (cos x)) / (1 - (cos x)))) ) ; ::_thesis: verum
end;
end;
end;

theorem :: SIN_COS5:34
for x being real number 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
let x be real number ; ::_thesis: ( 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)) implies sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )
assume that
A1: sin (x / 2) <> 0 and
A2: cos (x / 2) <> 0 and
A3: 1 - ((tan (x / 2)) ^2) <> 0 ; ::_thesis: ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )
set b = (sec (x / 2)) ^2 ;
set a = 1 - ((tan (x / 2)) ^2);
A4: (1 - ((tan (x / 2)) ^2)) + ((sec (x / 2)) ^2) = (1 + ((tan (x / 2)) ^2)) + (1 - ((tan (x / 2)) ^2)) by A2, Th11
.= 1 + 1 ;
sqrt ((2 * (sec x)) / ((sec x) + 1)) = sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) + 1)) by A1, A2, Th13
.= sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1)) by A1, A2, Th13 ;
then A5: sqrt ((2 * (sec x)) / ((sec x) + 1)) = sqrt (((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1) * (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:91
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) + (1 * (1 - ((tan (x / 2)) ^2)))))
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) + (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:87
.= sqrt ((2 * ((sec (x / 2)) ^2)) / 2) by A3, A4, XCMPLX_1:87
.= abs (sec (x / 2)) by COMPLEX1:72 ;
percases ( sec (x / 2) >= 0 or sec (x / 2) < 0 ) ;
suppose sec (x / 2) >= 0 ; ::_thesis: ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )
hence  ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) ) by A5, ABSVALUE:def_1; ::_thesis: verum
end;
suppose sec (x / 2) < 0 ; ::_thesis: ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )
then  (sqrt ((2 * (sec x)) / ((sec x) + 1))) * (- 1) = (- (sec (x / 2))) * (- 1) by A5, ABSVALUE:def_1;
hence  ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) ) ; ::_thesis: verum
end;
end;
end;

theorem :: SIN_COS5:35
for x being real number 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
let x be real number ; ::_thesis: ( 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)) implies cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
assume that
A1: sin (x / 2) <> 0 and
A2: cos (x / 2) <> 0 and
A3: 1 - ((tan (x / 2)) ^2) <> 0 ; ::_thesis: ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
set b = (sec (x / 2)) ^2 ;
set a = 1 - ((tan (x / 2)) ^2);
A4: ((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2)) = (1 + ((tan (x / 2)) ^2)) - (1 - ((tan (x / 2)) ^2)) by A2, Th11
.= 2 * ((tan (x / 2)) ^2) ;
sqrt ((2 * (sec x)) / ((sec x) - 1)) = sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) - 1)) by A1, A2, Th13
.= sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1)) by A1, A2, Th13 ;
then A5: sqrt ((2 * (sec x)) / ((sec x) - 1)) = sqrt (((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) - 1) * (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:91
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) - (1 * (1 - ((tan (x / 2)) ^2)))))
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) - (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:87
.= sqrt ((2 * ((sec (x / 2)) ^2)) / (2 * ((tan (x / 2)) ^2))) by A3, A4, XCMPLX_1:87
.= sqrt (((sec (x / 2)) ^2) / ((tan (x / 2)) ^2)) by XCMPLX_1:91
.= sqrt (((sec (x / 2)) / (tan (x / 2))) ^2) by XCMPLX_1:76
.= sqrt ((cosec (x / 2)) ^2) by A2, Th1
.= abs (cosec (x / 2)) by COMPLEX1:72 ;
percases ( cosec (x / 2) >= 0 or cosec (x / 2) < 0 ) ;
suppose cosec (x / 2) >= 0 ; ::_thesis: ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
hence  ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) ) by A5, ABSVALUE:def_1; ::_thesis: verum
end;
suppose cosec (x / 2) < 0 ; ::_thesis: ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) )
then  (sqrt ((2 * (sec x)) / ((sec x) - 1))) * (- 1) = (- (cosec (x / 2))) * (- 1) by A5, ABSVALUE:def_1;
hence  ( cosec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) - 1)) or cosec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) - 1))) ) ; ::_thesis: verum
end;
end;
end;

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))) & sech x = 2 / ((exp_R x) + (exp_R (- x))) & cosech x = 2 / ((exp_R x) - (exp_R (- x))) )
proof
let x be real number ; ::_thesis: ( 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))) )
A1: sech x = 1 / (cosh . x) by SIN_COS2:def_4
.= 1 / (((exp_R . x) + (exp_R . (- x))) / 2) by SIN_COS2:def_3
.= (1 * 2) / ((((exp_R . x) + (exp_R . (- x))) / 2) * 2) by XCMPLX_1:91
.= 2 / ((exp_R . x) + (exp_R (- x))) by SIN_COS:def_23
.= 2 / ((exp_R x) + (exp_R (- x))) by SIN_COS:def_23 ;
A2: cosech x = 1 / (sinh . x) by SIN_COS2:def_2
.= 1 / (((exp_R . x) - (exp_R . (- x))) / 2) by SIN_COS2:def_1
.= (1 * 2) / ((((exp_R . x) - (exp_R . (- x))) / 2) * 2) by XCMPLX_1:91
.= 2 / ((exp_R . x) - (exp_R (- x))) by SIN_COS:def_23 ;
coth x = (cosh . x) / (sinh x) by SIN_COS2:def_4
.= (cosh . x) / (sinh . x) by SIN_COS2:def_2
.= (((exp_R . x) + (exp_R . (- x))) / 2) / (sinh . x) by SIN_COS2:def_3
.= (((exp_R . x) + (exp_R . (- x))) / 2) / (((exp_R . x) - (exp_R . (- x))) / 2) by SIN_COS2:def_1
.= ((((exp_R . x) + (exp_R . (- x))) / 2) * 2) / ((((exp_R . x) - (exp_R . (- x))) / 2) * 2) by XCMPLX_1:91
.= ((exp_R . x) + (exp_R . (- x))) / ((exp_R . x) - (exp_R (- x))) by SIN_COS:def_23
.= ((exp_R . x) + (exp_R . (- x))) / ((exp_R x) - (exp_R (- x))) by SIN_COS:def_23
.= ((exp_R . x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) by SIN_COS:def_23
.= ((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) by SIN_COS:def_23 ;
hence  ( 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))) ) by A1, A2, SIN_COS:def_23; ::_thesis: verum
end;

theorem :: SIN_COS5:37
for x being real number st (exp_R x) - (exp_R (- x)) <> 0 holds
(tanh x) * (coth x) = 1
proof
let x be real number ; ::_thesis: ( (exp_R x) - (exp_R (- x)) <> 0 implies (tanh x) * (coth x) = 1 )
assume A1: (exp_R x) - (exp_R (- x)) <> 0 ; ::_thesis: (tanh x) * (coth x) = 1
 exp_R x > 0 by SIN_COS:55;
then A2: (exp_R x) + (exp_R (- x)) > 0 + 0 by SIN_COS:55, XREAL_1:8;
(tanh x) * (coth x) = (tanh . x) * (coth x) by SIN_COS2:def_6
.= (((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R . (- x)))) * (coth x) by SIN_COS2:def_5
.= (((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R . (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by Th36
.= (((exp_R . x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def_23
.= (((exp_R x) - (exp_R . (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def_23
.= (((exp_R x) - (exp_R (- x))) / ((exp_R . x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def_23
.= (((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))) * (((exp_R x) + (exp_R (- x))) / ((exp_R x) - (exp_R (- x)))) by SIN_COS:def_23
.= ((((exp_R x) - (exp_R (- x))) / ((exp_R x) + (exp_R (- x)))) * ((exp_R x) + (exp_R (- x)))) / ((exp_R x) - (exp_R (- x))) by XCMPLX_1:74 ;
then (tanh x) * (coth x) = ((exp_R x) - (exp_R (- x))) / ((exp_R x) - (exp_R (- x))) by A2, XCMPLX_1:87
.= 1 by A1, XCMPLX_1:60 ;
hence  (tanh x) * (coth x) = 1 ; ::_thesis: verum
end;

theorem :: SIN_COS5:38
for x being real number holds ((sech x) ^2) + ((tanh x) ^2) = 1
proof
let x be real number ; ::_thesis: ((sech x) ^2) + ((tanh x) ^2) = 1
 cosh . x <> 0 by SIN_COS2:15;
then A1: (cosh . x) ^2 <> 0 by SQUARE_1:12;
((sech x) ^2) + ((tanh x) ^2) = ((1 / (cosh x)) ^2) + ((tanh . x) ^2) by SIN_COS2:def_6
.= ((1 / (cosh . x)) ^2) + ((tanh . x) ^2) by SIN_COS2:def_4
.= ((1 ^2) / ((cosh . x) ^2)) + ((tanh . x) ^2) by XCMPLX_1:76
.= ((1 ^2) / ((cosh . x) ^2)) + (((sinh . x) / (cosh . x)) ^2) by SIN_COS2:17
.= (1 / ((cosh . x) ^2)) + (((sinh . x) ^2) / ((cosh . x) ^2)) by XCMPLX_1:76
.= (1 + ((sinh . x) ^2)) / ((cosh . x) ^2) by XCMPLX_1:62
.= ((((cosh . x) ^2) - ((sinh . x) ^2)) + ((sinh . x) ^2)) / ((cosh . x) ^2) by SIN_COS2:14
.= ((cosh . x) ^2) / ((cosh . x) ^2) ;
hence  ((sech x) ^2) + ((tanh x) ^2) = 1 by A1, XCMPLX_1:60; ::_thesis: verum
end;

theorem :: SIN_COS5:39
for x being real number st sinh x <> 0 holds
((coth x) ^2) - ((cosech x) ^2) = 1
proof
let x be real number ; ::_thesis: ( sinh x <> 0 implies ((coth x) ^2) - ((cosech x) ^2) = 1 )
assume  sinh x <> 0 ; ::_thesis: ((coth x) ^2) - ((cosech x) ^2) = 1
then A1: (sinh x) ^2 <> 0 by SQUARE_1:12;
((coth x) ^2) - ((cosech x) ^2) = (((cosh x) ^2) / ((sinh x) ^2)) - ((1 / (sinh x)) ^2) by XCMPLX_1:76
.= (((cosh x) ^2) / ((sinh x) ^2)) - ((1 ^2) / ((sinh x) ^2)) by XCMPLX_1:76
.= (((cosh x) ^2) - 1) / ((sinh x) ^2) by XCMPLX_1:120
.= (((cosh x) ^2) - (((cosh . x) ^2) - ((sinh . x) ^2))) / ((sinh x) ^2) by SIN_COS2:14
.= ((((cosh x) ^2) - ((cosh . x) ^2)) + ((sinh . x) ^2)) / ((sinh x) ^2)
.= ((((cosh x) ^2) - ((cosh x) ^2)) + ((sinh . x) ^2)) / ((sinh x) ^2) by SIN_COS2:def_4
.= (0 + ((sinh x) ^2)) / ((sinh x) ^2) by SIN_COS2:def_2 ;
hence  ((coth x) ^2) - ((cosech x) ^2) = 1 by A1, XCMPLX_1:60; ::_thesis: verum
end;

Lm1:  for x being real number holds coth (- x) = - (coth x)
proof
let x be real number ; ::_thesis: coth (- x) = - (coth x)
coth (- x) = (cosh . (- x)) / (sinh (- x)) by SIN_COS2:def_4
.= (cosh . (- x)) / (sinh . (- x)) by SIN_COS2:def_2
.= (cosh . x) / (sinh . (- x)) by SIN_COS2:19
.= (cosh . x) / (- (sinh . x)) by SIN_COS2:19
.= - ((cosh . x) / (sinh . x)) by XCMPLX_1:188
.= - ((cosh x) / (sinh . x)) by SIN_COS2:def_4
.= - (coth x) by SIN_COS2:def_2 ;
hence  coth (- x) = - (coth x) ; ::_thesis: verum
end;

theorem Th40: :: SIN_COS5:40
for x1, x2 being real number st sinh x1 <> 0 & sinh x2 <> 0 holds
coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2))
proof
let x1, x2 be real number ; ::_thesis: ( sinh x1 <> 0 & sinh x2 <> 0 implies coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2)) )
assume that
A1: sinh x1 <> 0 and
A2: sinh x2 <> 0 ; ::_thesis: coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2))
A3: sinh . x1 <> 0 by A1, SIN_COS2:def_2;
A4: sinh . x2 <> 0 by A2, SIN_COS2:def_2;
coth (x1 + x2) = (cosh . (x1 + x2)) / (sinh (x1 + x2)) by SIN_COS2:def_4
.= (cosh . (x1 + x2)) / (sinh . (x1 + x2)) by SIN_COS2:def_2
.= (((cosh . x1) * (cosh . x2)) + ((sinh . x1) * (sinh . x2))) / (sinh . (x1 + x2)) by SIN_COS2:20
.= (((cosh . x1) * (cosh . x2)) + ((sinh . x1) * (sinh . x2))) / (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) by SIN_COS2:21
.= ((((cosh . x1) * (cosh . x2)) + ((sinh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by A3, A4, XCMPLX_1:6, XCMPLX_1:55
.= ((((cosh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + (((sinh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:62
.= ((((cosh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by A3, A4, XCMPLX_1:6, XCMPLX_1:60
.= (((((cosh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:83
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:74
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / ((((sinh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:62
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:83
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + ((((cosh . x1) / (sinh . x1)) * (sinh . x2)) / (sinh . x2))) by XCMPLX_1:83
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((1 * (cosh . x2)) / (sinh . x2)) + ((((cosh . x1) / (sinh . x1)) * (sinh . x2)) / (sinh . x2))) by A3, XCMPLX_1:60
.= ((((cosh . x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by A4, XCMPLX_1:89
.= ((((cosh x1) / (sinh . x1)) * ((cosh . x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by SIN_COS2:def_4
.= ((((cosh x1) / (sinh . x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by SIN_COS2:def_4
.= ((((cosh x1) / (sinh . x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh . x1) / (sinh . x1))) by SIN_COS2:def_4
.= ((((cosh x1) / (sinh . x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh x1) / (sinh . x1))) by SIN_COS2:def_4
.= ((((cosh x1) / (sinh x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh . x2)) + ((cosh x1) / (sinh . x1))) by SIN_COS2:def_2
.= ((((cosh x1) / (sinh x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh x2)) + ((cosh x1) / (sinh . x1))) by SIN_COS2:def_2
.= ((((cosh x1) / (sinh x1)) * ((cosh x2) / (sinh . x2))) + 1) / (((cosh x2) / (sinh x2)) + ((cosh x1) / (sinh x1))) by SIN_COS2:def_2
.= (((coth x1) * (coth x2)) + 1) / ((coth x2) + (coth x1)) by SIN_COS2:def_2 ;
hence  coth (x1 + x2) = (1 + ((coth x1) * (coth x2))) / ((coth x1) + (coth x2)) ; ::_thesis: verum
end;

theorem :: SIN_COS5:41
for x1, x2 being real number st sinh x1 <> 0 & sinh x2 <> 0 holds
coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2))
proof
let x1, x2 be real number ; ::_thesis: ( sinh x1 <> 0 & sinh x2 <> 0 implies coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2)) )
assume that
A1: sinh x1 <> 0 and
A2: sinh x2 <> 0 ; ::_thesis: coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2))
 - (sinh . x2) <> 0 by A2, SIN_COS2:def_2;
then  sinh . (- x2) <> 0 by SIN_COS2:19;
then A3: sinh (- x2) <> 0 by SIN_COS2:def_2;
coth (x1 - x2) = coth (x1 + (- x2))
.= (1 + ((coth x1) * (coth (- x2)))) / ((coth x1) + (coth (- x2))) by A1, A3, Th40
.= (1 + ((coth x1) * (- (coth x2)))) / ((coth x1) + (coth (- x2))) by Lm1
.= (1 - ((coth x1) * (coth x2))) / ((coth x1) + (- (coth x2))) by Lm1
.= (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2)) ;
hence  coth (x1 - x2) = (1 - ((coth x1) * (coth x2))) / ((coth x1) - (coth x2)) ; ::_thesis: verum
end;

theorem :: SIN_COS5:42
for x1, x2 being real number 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
let x1, x2 be real number ; ::_thesis: ( sinh x1 <> 0 & sinh x2 <> 0 implies ( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) ) )
assume that
A1: sinh x1 <> 0 and
A2: sinh x2 <> 0 ; ::_thesis: ( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) )
A3: sinh . x1 <> 0 by A1, SIN_COS2:def_2;
A4: sinh . x2 <> 0 by A2, SIN_COS2:def_2;
A5: - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) = - ((sinh . (x1 - x2)) / ((sinh x1) * (sinh x2))) by SIN_COS2:def_2
.= - ((sinh . (x1 - x2)) / ((sinh . x1) * (sinh x2))) by SIN_COS2:def_2
.= - ((sinh . (x1 - x2)) / ((sinh . x1) * (sinh . x2))) by SIN_COS2:def_2
.= - ((((sinh . x1) * (cosh . x2)) - ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2))) by SIN_COS2:21
.= - ((((sinh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) - (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:120
.= - (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) - (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2)))) by XCMPLX_1:83
.= - (((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x1)) / (sinh . x1))) by XCMPLX_1:83
.= - (((1 * (cosh . x2)) / (sinh . x2)) - ((((sinh . x2) / (sinh . x2)) * (cosh . x1)) / (sinh . x1))) by A3, XCMPLX_1:60
.= - (((cosh . x2) / (sinh . x2)) - ((1 * (cosh . x1)) / (sinh . x1))) by A4, XCMPLX_1:60
.= - (((cosh x2) / (sinh . x2)) - ((cosh . x1) / (sinh . x1))) by SIN_COS2:def_4
.= - (((cosh x2) / (sinh . x2)) - ((cosh x1) / (sinh . x1))) by SIN_COS2:def_4
.= - (((cosh x2) / (sinh x2)) - ((cosh x1) / (sinh . x1))) by SIN_COS2:def_2
.= - ((coth x2) - ((cosh x1) / (sinh x1))) by SIN_COS2:def_2
.= (coth x1) - (coth x2) ;
(sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) = (sinh . (x1 + x2)) / ((sinh x1) * (sinh x2)) by SIN_COS2:def_2
.= (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh x1) * (sinh x2)) by SIN_COS2:21
.= (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh x2)) by SIN_COS2:def_2
.= (((sinh . x1) * (cosh . x2)) + ((cosh . x1) * (sinh . x2))) / ((sinh . x1) * (sinh . x2)) by SIN_COS2:def_2
.= (((sinh . x1) * (cosh . x2)) / ((sinh . x1) * (sinh . x2))) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:62
.= ((((sinh . x1) / (sinh . x1)) * (cosh . x2)) / (sinh . x2)) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2))) by XCMPLX_1:83
.= ((1 * (cosh . x2)) / (sinh . x2)) + (((cosh . x1) * (sinh . x2)) / ((sinh . x1) * (sinh . x2))) by A3, XCMPLX_1:60
.= ((cosh . x2) / (sinh . x2)) + ((((cosh . x1) / (sinh . x1)) * (sinh . x2)) / (sinh . x2)) by XCMPLX_1:83
.= ((cosh . x2) / (sinh . x2)) + (((cosh . x1) / (sinh . x1)) * ((sinh . x2) / (sinh . x2))) by XCMPLX_1:74
.= ((cosh . x2) / (sinh . x2)) + (((cosh . x1) / (sinh . x1)) * 1) by A4, XCMPLX_1:60
.= ((cosh . x2) / (sinh . x2)) + ((cosh . x1) / (sinh x1)) by SIN_COS2:def_2
.= ((cosh . x2) / (sinh x2)) + ((cosh . x1) / (sinh x1)) by SIN_COS2:def_2
.= ((cosh x2) / (sinh x2)) + ((cosh . x1) / (sinh x1)) by SIN_COS2:def_4
.= (coth x2) + (coth x1) by SIN_COS2:def_4 ;
hence  ( (coth x1) + (coth x2) = (sinh (x1 + x2)) / ((sinh x1) * (sinh x2)) & (coth x1) - (coth x2) = - ((sinh (x1 - x2)) / ((sinh x1) * (sinh x2))) ) by A5; ::_thesis: verum
end;

Lm2:  for x being real number holds (cosh . x) ^2 = 1 + ((sinh . x) ^2)
proof
let x be real number ; ::_thesis: (cosh . x) ^2 = 1 + ((sinh . x) ^2)
 (((cosh . x) ^2) - ((sinh . x) ^2)) + ((sinh . x) ^2) = 1 + ((sinh . x) ^2) by SIN_COS2:14;
hence  (cosh . x) ^2 = 1 + ((sinh . x) ^2) ; ::_thesis: verum
end;

Lm3:  for x being real number holds ((cosh . x) ^2) - 1 = (sinh . x) ^2
proof
let x be real number ; ::_thesis: ((cosh . x) ^2) - 1 = (sinh . x) ^2
 (((cosh . x) ^2) - ((sinh . x) ^2)) + ((sinh . x) ^2) = 1 + ((sinh . x) ^2) by SIN_COS2:14;
hence  ((cosh . x) ^2) - 1 = (sinh . x) ^2 ; ::_thesis: verum
end;

theorem :: SIN_COS5:43
for x being real number holds sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3))
proof
let x be real number ; ::_thesis: sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3))
sinh (3 * x) = sinh . ((x + x) + x) by SIN_COS2:def_2
.= ((sinh . (2 * x)) * (cosh . x)) + ((cosh . (2 * x)) * (sinh . x)) by SIN_COS2:21
.= (((2 * (sinh . x)) * (cosh . x)) * (cosh . x)) + ((cosh . (2 * x)) * (sinh . x)) by SIN_COS2:23
.= ((2 * (sinh . x)) * ((cosh . x) ^2)) + (((2 * ((cosh . x) ^2)) - 1) * (sinh . x)) by SIN_COS2:23
.= ((2 * (sinh . x)) * (1 + ((sinh . x) ^2))) + (((2 * ((cosh . x) ^2)) - 1) * (sinh . x)) by Lm2
.= ((2 * (sinh . x)) * (1 + ((sinh . x) ^2))) + (((2 * (1 + ((sinh . x) ^2))) - 1) * (sinh . x)) by Lm2
.= ((2 * (sinh . x)) + (((2 + 2) * (sinh . x)) * ((sinh . x) ^2))) + (sinh . x)
.= ((2 * (sinh . x)) + ((4 * ((sinh . x) |^ 1)) * ((sinh . x) ^2))) + (sinh . x) by NEWTON:5
.= (3 * (sinh . x)) + (4 * ((((sinh . x) |^ 1) * (sinh . x)) * (sinh . x)))
.= (3 * (sinh . x)) + (4 * (((sinh . x) |^ (1 + 1)) * (sinh . x))) by NEWTON:6
.= (3 * (sinh . x)) + (4 * ((sinh . x) |^ (2 + 1))) by NEWTON:6
.= (3 * (sinh x)) + (4 * ((sinh . x) |^ 3)) by SIN_COS2:def_2 ;
hence  sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3)) by SIN_COS2:def_2; ::_thesis: verum
end;

theorem :: SIN_COS5:44
for x being real number holds cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x))
proof
let x be real number ; ::_thesis: cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x))
cosh (3 * x) = cosh . ((x + x) + x) by SIN_COS2:def_4
.= ((cosh . (2 * x)) * (cosh . x)) + ((sinh . (2 * x)) * (sinh . x)) by SIN_COS2:20
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((sinh . (2 * x)) * (sinh . x)) by SIN_COS2:23
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + (((2 * (sinh . x)) * (cosh . x)) * (sinh . x)) by SIN_COS2:23
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((2 * ((sinh . x) ^2)) * (cosh . x))
.= (((2 * ((cosh . x) ^2)) - 1) * (cosh . x)) + ((2 * (((cosh . x) ^2) - 1)) * (cosh . x)) by Lm3
.= (4 * (((cosh . x) * (cosh . x)) * (cosh . x))) - (3 * (cosh . x))
.= (4 * ((((cosh . x) |^ 1) * (cosh . x)) * (cosh . x))) - (3 * (cosh . x)) by NEWTON:5
.= (4 * (((cosh . x) |^ (1 + 1)) * (cosh . x))) - (3 * (cosh . x)) by NEWTON:6
.= (4 * ((cosh . x) |^ (2 + 1))) - (3 * (cosh . x)) by NEWTON:6
.= (4 * ((cosh . x) |^ 3)) - (3 * (cosh x)) by SIN_COS2:def_4 ;
hence  cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x)) by SIN_COS2:def_4; ::_thesis: verum
end;

theorem :: SIN_COS5:45
for x being real number st sinh x <> 0 holds
coth (2 * x) = (1 + ((coth x) ^2)) / (2 * (coth x))
proof
let x be real number ; ::_thesis: ( sinh x <> 0 implies coth (2 * x) = (1 + ((coth x) ^2)) / (2 * (coth x)) )
assume  sinh x <> 0 ; ::_thesis: coth (2 * x) = (1 + ((coth x) ^2)) / (2 * (coth x))
then A1: sinh . x <> 0 by SIN_COS2:def_2;
then A2: (sinh . x) ^2 <> 0 by SQUARE_1:12;
coth (2 * x) = (cosh . (2 * x)) / (sinh (2 * x)) by SIN_COS2:def_4
.= (cosh . (2 * x)) / (sinh . (2 * x)) by SIN_COS2:def_2
.= ((2 * ((cosh . x) ^2)) - 1) / (sinh . (2 * x)) by SIN_COS2:23
.= ((2 * ((cosh . x) ^2)) - 1) / ((2 * (sinh . x)) * (cosh . x)) by SIN_COS2:23
.= (((2 * ((cosh . x) ^2)) - 1) / ((sinh . x) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) by A2, XCMPLX_1:55
.= (((2 * ((cosh . x) ^2)) - (((cosh . x) ^2) - ((sinh . x) ^2))) / ((sinh . x) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) by SIN_COS2:14
.= ((((2 - 1) * ((cosh . x) ^2)) + ((sinh . x) ^2)) / ((sinh . x) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2))
.= ((((cosh . x) ^2) / ((sinh . x) ^2)) + (((sinh . x) ^2) / ((sinh . x) ^2))) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) by XCMPLX_1:62
.= ((((cosh . x) / (sinh . x)) ^2) + (((sinh . x) ^2) / ((sinh . x) ^2))) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) by XCMPLX_1:76
.= ((((cosh . x) / (sinh . x)) ^2) + (((sinh . x) / (sinh . x)) ^2)) / (((2 * (sinh . x)) * (cosh . x)) / ((sinh . x) ^2)) by XCMPLX_1:76
.= ((((cosh . x) / (sinh . x)) ^2) + (1 ^2)) / (((2 * (cosh . x)) * (sinh . x)) / ((sinh . x) * (sinh . x))) by A1, XCMPLX_1:60
.= ((((cosh . x) / (sinh . x)) ^2) + 1) / ((((2 * (cosh . x)) * (sinh . x)) / (sinh . x)) / (sinh . x)) by XCMPLX_1:78
.= ((((cosh . x) / (sinh . x)) ^2) + 1) / ((2 * (cosh . x)) / (sinh . x)) by A1, XCMPLX_1:89
.= ((((cosh . x) / (sinh . x)) ^2) + 1) / (2 * ((cosh . x) / (sinh . x))) by XCMPLX_1:74
.= ((((cosh x) / (sinh . x)) ^2) + 1) / (2 * ((cosh . x) / (sinh . x))) by SIN_COS2:def_4
.= ((((cosh x) / (sinh . x)) ^2) + 1) / (2 * ((cosh x) / (sinh . x))) by SIN_COS2:def_4
.= ((((cosh x) / (sinh x)) ^2) + 1) / (2 * ((cosh x) / (sinh . x))) by SIN_COS2:def_2
.= (((coth x) ^2) + 1) / (2 * ((cosh x) / (sinh x))) by SIN_COS2:def_2 ;
hence  coth (2 * x) = (1 + ((coth x) ^2)) / (2 * (coth x)) ; ::_thesis: verum
end;

Lm4:  for x being real number st x > 0 holds
sinh x >= 0
proof
let x be real number ; ::_thesis: ( x > 0 implies sinh x >= 0 )
assume A1: x > 0 ; ::_thesis: sinh x >= 0
then  x + (- x) > 0 + (- x) by XREAL_1:8;
then A2: exp_R . (- x) <= 1 by SIN_COS:53;
 exp_R . x >= 1 by A1, SIN_COS:52;
then  (exp_R . x) - (exp_R . (- x)) >= 1 - 1 by A2, XREAL_1:13;
then  ((exp_R . x) - (exp_R . (- x))) / 2 >= 0 by XREAL_1:136;
then  sinh . x >= 0 by SIN_COS2:def_1;
hence  sinh x >= 0 by SIN_COS2:def_2; ::_thesis: verum
end;

theorem :: SIN_COS5:46
for x being real number st x >= 0 holds
sinh x >= 0
proof
let x be real number ; ::_thesis: ( x >= 0 implies sinh x >= 0 )
assume A1: x >= 0 ; ::_thesis: sinh x >= 0
percases ( x > 0 or x = 0 ) by A1, XXREAL_0:1;
suppose x > 0 ; ::_thesis: sinh x >= 0
hence  sinh x >= 0 by Lm4; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: sinh x >= 0
hence  sinh x >= 0 by SIN_COS2:16, SIN_COS2:def_2; ::_thesis: verum
end;
end;
end;

theorem :: SIN_COS5:47
for x being real number st x <= 0 holds
sinh x <= 0
proof
let x be real number ; ::_thesis: ( x <= 0 implies sinh x <= 0 )
assume A1: x <= 0 ; ::_thesis: sinh x <= 0
percases ( x < 0 or x = 0 ) by A1, XXREAL_0:1;
supposeA2: x < 0 ; ::_thesis: sinh x <= 0
then  - x > 0 by XREAL_1:58;
then A3: exp_R . (- x) >= 1 by SIN_COS:52;
 exp_R . x <= 1 by A2, SIN_COS:53;
then  (exp_R . x) - (exp_R . (- x)) <= 1 - 1 by A3, XREAL_1:13;
then  ((exp_R . x) - (exp_R . (- x))) / 2 <= 0 by XREAL_1:138;
then  sinh . x <= 0 by SIN_COS2:def_1;
hence  sinh x <= 0 by SIN_COS2:def_2; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: sinh x <= 0
hence  sinh x <= 0 by SIN_COS2:16, SIN_COS2:def_2; ::_thesis: verum
end;
end;
end;

theorem :: SIN_COS5:48
for x being real number holds cosh (x / 2) = sqrt (((cosh x) + 1) / 2)
proof
let x be real number ; ::_thesis: cosh (x / 2) = sqrt (((cosh x) + 1) / 2)
A1: cosh . (x / 2) > 0 by SIN_COS2:15;
sqrt (((cosh x) + 1) / 2) = sqrt (((cosh . (2 * (x / 2))) + 1) / 2) by SIN_COS2:def_4
.= sqrt ((((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) / 2) by SIN_COS2:23
.= cosh . (x / 2) by A1, SQUARE_1:22 ;
hence  cosh (x / 2) = sqrt (((cosh x) + 1) / 2) by SIN_COS2:def_4; ::_thesis: verum
end;

theorem :: SIN_COS5:49
for x being real number st sinh (x / 2) <> 0 holds
tanh (x / 2) = ((cosh x) - 1) / (sinh x)
proof
let x be real number ; ::_thesis: ( sinh (x / 2) <> 0 implies tanh (x / 2) = ((cosh x) - 1) / (sinh x) )
assume  sinh (x / 2) <> 0 ; ::_thesis: tanh (x / 2) = ((cosh x) - 1) / (sinh x)
then A1: 2 * (sinh . (x / 2)) <> 0 by SIN_COS2:def_2;
((cosh x) - 1) / (sinh x) = ((cosh . (2 * (x / 2))) - 1) / (sinh (2 * (x / 2))) by SIN_COS2:def_4
.= (((2 * ((cosh . (x / 2)) ^2)) - 1) - 1) / (sinh (2 * (x / 2))) by SIN_COS2:23
.= (2 * (((cosh . (x / 2)) ^2) - 1)) / (sinh (2 * (x / 2)))
.= (2 * ((sinh . (x / 2)) ^2)) / (sinh (2 * (x / 2))) by Lm3
.= (2 * ((sinh . (x / 2)) ^2)) / (sinh . (2 * (x / 2))) by SIN_COS2:def_2
.= ((2 * (sinh . (x / 2))) * (sinh . (x / 2))) / ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) by SIN_COS2:23
.= (sinh . (x / 2)) / (cosh . (x / 2)) by A1, XCMPLX_1:91
.= tanh . (x / 2) by SIN_COS2:17
.= tanh (x / 2) by SIN_COS2:def_6 ;
hence  tanh (x / 2) = ((cosh x) - 1) / (sinh x) ; ::_thesis: verum
end;

theorem :: SIN_COS5:50
for x being real number st cosh (x / 2) <> 0 holds
tanh (x / 2) = (sinh x) / ((cosh x) + 1)
proof
let x be real number ; ::_thesis: ( cosh (x / 2) <> 0 implies tanh (x / 2) = (sinh x) / ((cosh x) + 1) )
assume  cosh (x / 2) <> 0 ; ::_thesis: tanh (x / 2) = (sinh x) / ((cosh x) + 1)
then A1: 2 * (cosh . (x / 2)) <> 0 by SIN_COS2:def_4;
(sinh x) / ((cosh x) + 1) = (sinh . (2 * (x / 2))) / ((cosh (2 * (x / 2))) + 1) by SIN_COS2:def_2
.= (sinh . (2 * (x / 2))) / ((cosh . (2 * (x / 2))) + 1) by SIN_COS2:def_4
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((cosh . (2 * (x / 2))) + 1) by SIN_COS2:23
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) by SIN_COS2:23
.= ((2 * (cosh . (x / 2))) * (sinh . (x / 2))) / ((2 * (cosh . (x / 2))) * (cosh . (x / 2)))
.= (sinh . (x / 2)) / (cosh . (x / 2)) by A1, XCMPLX_1:91
.= tanh . (x / 2) by SIN_COS2:17 ;
hence  tanh (x / 2) = (sinh x) / ((cosh x) + 1) by SIN_COS2:def_6; ::_thesis: verum
end;

theorem :: SIN_COS5:51
for x being real number st sinh (x / 2) <> 0 holds
coth (x / 2) = (sinh x) / ((cosh x) - 1)
proof
let x be real number ; ::_thesis: ( sinh (x / 2) <> 0 implies coth (x / 2) = (sinh x) / ((cosh x) - 1) )
assume  sinh (x / 2) <> 0 ; ::_thesis: coth (x / 2) = (sinh x) / ((cosh x) - 1)
then A1: 2 * (sinh . (x / 2)) <> 0 by SIN_COS2:def_2;
(sinh x) / ((cosh x) - 1) = (sinh . (2 * (x / 2))) / ((cosh (2 * (x / 2))) - 1) by SIN_COS2:def_2
.= (sinh . (2 * (x / 2))) / ((cosh . (2 * (x / 2))) - 1) by SIN_COS2:def_4
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((cosh . (2 * (x / 2))) - 1) by SIN_COS2:23
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (((2 * ((cosh . (x / 2)) ^2)) - 1) - 1) by SIN_COS2:23
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (2 * (((cosh . (x / 2)) ^2) - 1))
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / (2 * ((sinh . (x / 2)) ^2)) by Lm3
.= ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) / ((2 * (sinh . (x / 2))) * (sinh . (x / 2)))
.= (cosh . (x / 2)) / (sinh . (x / 2)) by A1, XCMPLX_1:91
.= (cosh (x / 2)) / (sinh . (x / 2)) by SIN_COS2:def_4
.= (cosh (x / 2)) / (sinh (x / 2)) by SIN_COS2:def_2 ;
hence  coth (x / 2) = (sinh x) / ((cosh x) - 1) ; ::_thesis: verum
end;

theorem :: SIN_COS5:52
for x being real number st cosh (x / 2) <> 0 holds
coth (x / 2) = ((cosh x) + 1) / (sinh x)
proof
let x be real number ; ::_thesis: ( cosh (x / 2) <> 0 implies coth (x / 2) = ((cosh x) + 1) / (sinh x) )
assume  cosh (x / 2) <> 0 ; ::_thesis: coth (x / 2) = ((cosh x) + 1) / (sinh x)
then A1: 2 * (cosh . (x / 2)) <> 0 by SIN_COS2:def_4;
((cosh x) + 1) / (sinh x) = ((cosh . (2 * (x / 2))) + 1) / (sinh (2 * (x / 2))) by SIN_COS2:def_4
.= (((2 * ((cosh . (x / 2)) ^2)) - 1) + 1) / (sinh (2 * (x / 2))) by SIN_COS2:23
.= (2 * ((cosh . (x / 2)) ^2)) / (sinh . (2 * (x / 2))) by SIN_COS2:def_2
.= (2 * ((cosh . (x / 2)) * (cosh . (x / 2)))) / ((2 * (sinh . (x / 2))) * (cosh . (x / 2))) by SIN_COS2:23
.= ((2 * (cosh . (x / 2))) * (cosh . (x / 2))) / ((2 * (cosh . (x / 2))) * (sinh . (x / 2)))
.= (cosh . (x / 2)) / (sinh . (x / 2)) by A1, XCMPLX_1:91
.= (cosh (x / 2)) / (sinh . (x / 2)) by SIN_COS2:def_4
.= (cosh (x / 2)) / (sinh (x / 2)) by SIN_COS2:def_2 ;
hence  coth (x / 2) = ((cosh x) + 1) / (sinh x) ; ::_thesis: verum
end;