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