:: SIN_COS5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: SIN_COS5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cos x <> 0 holds
cosec x = (sec x) / (tan x)
proof end;

theorem Th2: :: SIN_COS5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sin x <> 0 holds
cos x = (sin x) * (cot x)
proof end;

theorem :: SIN_COS5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th5: :: SIN_COS5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds sin (2 * x) = (2 * (sin x)) * (cos x)
proof end;

theorem Th6: :: SIN_COS5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cos x <> 0 holds
sin (2 * x) = (2 * (tan x)) / (1 + ((tan x) ^2 ))
proof end;

theorem Th7: :: SIN_COS5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th8: :: SIN_COS5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cos x <> 0 holds
cos (2 * x) = (1 - ((tan x) ^2 )) / (1 + ((tan x) ^2 ))
proof end;

theorem :: SIN_COS5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cos x <> 0 holds
tan (2 * x) = (2 * (tan x)) / (1 - ((tan x) ^2 ))
proof end;

theorem :: SIN_COS5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sin x <> 0 holds
cot (2 * x) = (((cot x) ^2 ) - 1) / (2 * (cot x))
proof end;

theorem Th11: :: SIN_COS5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cos x <> 0 holds
(sec x) ^2 = 1 + ((tan x) ^2 )
proof end;

theorem Th12: :: SIN_COS5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds cot x = 1 / (tan x)
proof end;

theorem Th13: :: SIN_COS5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sin x <> 0 holds
(cosec x) ^2 = 1 + ((cot x) ^2 )
proof end;

theorem :: SIN_COS5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem Th16: :: SIN_COS5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds sin (3 * x) = (- (4 * ((sin x) |^ 3))) + (3 * (sin x))
proof end;

theorem Th17: :: SIN_COS5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds cos (3 * x) = (4 * ((cos x) |^ 3)) - (3 * (cos x))
proof end;

theorem :: SIN_COS5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds (sin x) ^2 = (1 - (cos (2 * x))) / 2
proof end;

theorem :: SIN_COS5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds (cos x) ^2 = (1 + (cos (2 * x))) / 2
proof end;

theorem :: SIN_COS5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds (sin x) |^ 3 = ((3 * (sin x)) - (sin (3 * x))) / 4
proof end;

theorem :: SIN_COS5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds (cos x) |^ 3 = ((3 * (cos x)) + (cos (3 * x))) / 4
proof end;

theorem :: SIN_COS5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds (sin x) |^ 4 = ((3 - (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
proof end;

theorem :: SIN_COS5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds (cos x) |^ 4 = ((3 + (4 * (cos (2 * x)))) + (cos (4 * x))) / 8
proof end;

theorem :: SIN_COS5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds
( sin (x / 2) = sqrt ((1 - (cos x)) / 2) or sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) )
proof end;

theorem :: SIN_COS5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds
( cos (x / 2) = sqrt ((1 + (cos x)) / 2) or cos (x / 2) = - (sqrt ((1 + (cos x)) / 2)) )
proof end;

theorem :: SIN_COS5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sin (x / 2) <> 0 holds
tan (x / 2) = (1 - (cos x)) / (sin x)
proof end;

theorem :: SIN_COS5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cos (x / 2) <> 0 holds
tan (x / 2) = (sin x) / (1 + (cos x))
proof end;

theorem :: SIN_COS5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cos (x / 2) <> 0 holds
cot (x / 2) = (1 + (cos x)) / (sin x)
proof end;

theorem :: SIN_COS5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sin (x / 2) <> 0 holds
cot (x / 2) = (sin x) / (1 - (cos x))
proof end;

theorem :: SIN_COS5:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds
( coth x = ((exp x) + (exp (- x))) / ((exp x) - (exp (- x))) & sech x = 2 / ((exp x) + (exp (- x))) & cosech x = 2 / ((exp x) - (exp (- x))) )
proof end;

theorem :: SIN_COS5:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st (exp x) - (exp (- x)) <> 0 holds
(tanh x) * (coth x) = 1
proof end;

theorem :: SIN_COS5:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds ((sech x) ^2 ) + ((tanh x) ^2 ) = 1
proof end;

theorem :: SIN_COS5:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sinh x <> 0 holds
((coth x) ^2 ) - ((cosech x) ^2 ) = 1
proof end;

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

theorem Th40: :: SIN_COS5:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

theorem :: SIN_COS5:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

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

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

theorem :: SIN_COS5:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds sinh (3 * x) = (3 * (sinh x)) + (4 * ((sinh x) |^ 3))
proof end;

theorem :: SIN_COS5:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x))
proof end;

theorem :: SIN_COS5:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sinh x <> 0 holds
coth (2 * x) = (1 + ((coth x) ^2 )) / (2 * (coth x))
proof end;

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

Lm5: sinh 0 = 0
by SIN_COS2:def 2, SIN_COS2:16;

theorem :: SIN_COS5:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st x >= 0 holds
sinh x >= 0
proof end;

theorem :: SIN_COS5:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st x <= 0 holds
sinh x <= 0
proof end;

theorem :: SIN_COS5:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number holds cosh (x / 2) = sqrt (((cosh x) + 1) / 2)
proof end;

theorem :: SIN_COS5:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sinh (x / 2) <> 0 holds
tanh (x / 2) = ((cosh x) - 1) / (sinh x)
proof end;

theorem :: SIN_COS5:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cosh (x / 2) <> 0 holds
tanh (x / 2) = (sinh x) / ((cosh x) + 1)
proof end;

theorem :: SIN_COS5:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st sinh (x / 2) <> 0 holds
coth (x / 2) = (sinh x) / ((cosh x) - 1)
proof end;

theorem :: SIN_COS5:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being real number st cosh (x / 2) <> 0 holds
coth (x / 2) = ((cosh x) + 1) / (sinh x)
proof end;