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

Lm1: [*2,0*] = 2 + (0 * <i> )
by COMPLEX1:27;

definition
func sin_C -> Function of COMPLEX , COMPLEX means :Def1: :: SIN_COS3:def 1
for z being Element of COMPLEX holds it . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i> );
existence
ex b1 being Function of COMPLEX , COMPLEX st
for z being Element of COMPLEX holds b1 . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i> )
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i> ) ) & ( for z being Element of COMPLEX holds b2 . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i> ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines sin_C SIN_COS3:def 1 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = sin_C iff for z being Element of COMPLEX holds b1 . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i> ) );

definition
func cos_C -> Function of COMPLEX , COMPLEX means :Def2: :: SIN_COS3:def 2
for z being Element of COMPLEX holds it . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2;
existence
ex b1 being Function of COMPLEX , COMPLEX st
for z being Element of COMPLEX holds b1 . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines cos_C SIN_COS3:def 2 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = cos_C iff for z being Element of COMPLEX holds b1 . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 );

definition
func sinh_C -> Function of COMPLEX , COMPLEX means :Def3: :: SIN_COS3:def 3
for z being Element of COMPLEX holds it . z = ((exp z) - (exp (- z))) / 2;
existence
ex b1 being Function of COMPLEX , COMPLEX st
for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp z) - (exp (- z))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines sinh_C SIN_COS3:def 3 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = sinh_C iff for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 );

definition
func cosh_C -> Function of COMPLEX , COMPLEX means :Def4: :: SIN_COS3:def 4
for z being Element of COMPLEX holds it . z = ((exp z) + (exp (- z))) / 2;
existence
ex b1 being Function of COMPLEX , COMPLEX st
for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2
proof end;
uniqueness
for b1, b2 being Function of COMPLEX , COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 ) & ( for z being Element of COMPLEX holds b2 . z = ((exp z) + (exp (- z))) / 2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines cosh_C SIN_COS3:def 4 :
for b1 being Function of COMPLEX , COMPLEX holds
( b1 = cosh_C iff for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 );

Lm2: for z being Element of COMPLEX holds sin_C /. z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i> )
proof end;

Lm3: for z being Element of COMPLEX holds cos_C /. z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2
proof end;

Lm4: for z being Element of COMPLEX holds sinh_C /. z = ((exp z) - (exp (- z))) / 2
proof end;

Lm5: for z being Element of COMPLEX holds cosh_C /. z = ((exp z) + (exp (- z))) / 2
proof end;

Lm6: 0c = [*0,0*]
by ARYTM_0:def 7;

Lm7: 1r = [*1,0*]
by ARYTM_0:def 7, COMPLEX1:def 7;

Lm8: for z being Element of COMPLEX holds (exp z) * (exp (- z)) = 1
proof end;

theorem :: SIN_COS3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1
proof end;

theorem Th2: :: SIN_COS3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds - (sin_C /. z) = sin_C /. (- z)
proof end;

theorem Th3: :: SIN_COS3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds cos_C /. z = cos_C /. (- z)
proof end;

theorem Th4: :: SIN_COS3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
proof end;

theorem :: SIN_COS3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds sin_C /. (z1 - z2) = ((sin_C /. z1) * (cos_C /. z2)) - ((cos_C /. z1) * (sin_C /. z2))
proof end;

theorem Th6: :: SIN_COS3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2))
proof end;

theorem :: SIN_COS3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2))
proof end;

theorem Th8: :: SIN_COS3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = 1
proof end;

theorem Th9: :: SIN_COS3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds - (sinh_C /. z) = sinh_C /. (- z)
proof end;

theorem Th10: :: SIN_COS3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds cosh_C /. z = cosh_C /. (- z)
proof end;

theorem Th11: :: SIN_COS3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds sinh_C /. (z1 + z2) = ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))
proof end;

theorem Th12: :: SIN_COS3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds sinh_C /. (z1 - z2) = ((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2))
proof end;

theorem Th13: :: SIN_COS3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds cosh_C /. (z1 - z2) = ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))
proof end;

theorem Th14: :: SIN_COS3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))
proof end;

theorem Th15: :: SIN_COS3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds sin_C /. (<i> * z) = <i> * (sinh_C /. z)
proof end;

theorem Th16: :: SIN_COS3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds cos_C /. (<i> * z) = cosh_C /. z
proof end;

theorem Th17: :: SIN_COS3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds sinh_C /. (<i> * z) = <i> * (sin_C /. z)
proof end;

theorem Th18: :: SIN_COS3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds cosh_C /. (<i> * z) = cos_C /. z
proof end;

Lm9: for x, y being Element of REAL holds exp [*x,y*] = [*(exp x),0*] * [*(cos y),(sin y)*]
proof end;

theorem Th19: :: SIN_COS3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds exp [*x,y*] = [*((exp . x) * (cos . y)),((exp . x) * (sin . y))*]
proof end;

theorem Th20: :: SIN_COS3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
exp 0c = 1
proof end;

theorem Th21: :: SIN_COS3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sin_C /. 0c = 0
proof end;

theorem :: SIN_COS3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
sinh_C /. 0c = 0
proof end;

theorem Th23: :: SIN_COS3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
cos_C /. 0c = 1
proof end;

theorem :: SIN_COS3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
cosh_C /. 0c = 1
proof end;

theorem :: SIN_COS3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds exp z = (cosh_C /. z) + (sinh_C /. z)
proof end;

theorem :: SIN_COS3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds exp (- z) = (cosh_C /. z) - (sinh_C /. z)
proof end;

Lm10: for x being Element of REAL holds [*x,0*] * <i> = [*0,x*]
proof end;

theorem :: SIN_COS3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds
( exp (z + ([*(2 * PI ),0*] * <i> )) = exp z & exp (z + [*0,(2 * PI )*]) = exp z )
proof end;

theorem Th28: :: SIN_COS3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( exp [*0,((2 * PI ) * n)*] = 1 & exp ([*((2 * PI ) * n),0*] * <i> ) = 1 )
proof end;

theorem Th29: :: SIN_COS3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( exp [*0,(- ((2 * PI ) * n))*] = 1 & exp ([*(- ((2 * PI ) * n)),0*] * <i> ) = 1 )
proof end;

theorem :: SIN_COS3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( exp [*0,(((2 * n) + 1) * PI )*] = [*(- 1),0*] & exp ([*(((2 * n) + 1) * PI ),0*] * <i> ) = [*(- 1),0*] )
proof end;

theorem :: SIN_COS3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( exp [*0,(- (((2 * n) + 1) * PI ))*] = [*(- 1),0*] & exp ([*(- (((2 * n) + 1) * PI )),0*] * <i> ) = [*(- 1),0*] )
proof end;

theorem :: SIN_COS3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( exp [*0,(((2 * n) + (1 / 2)) * PI )*] = [*0,1*] & exp ([*(((2 * n) + (1 / 2)) * PI ),0*] * <i> ) = [*0,1*] )
proof end;

theorem :: SIN_COS3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat holds
( exp [*0,(- (((2 * n) + (1 / 2)) * PI ))*] = [*0,(- 1)*] & exp ([*(- (((2 * n) + (1 / 2)) * PI )),0*] * <i> ) = [*0,(- 1)*] )
proof end;

Lm11: for a, b being Element of REAL holds - [*a,b*] = [*(- a),(- b)*]
proof end;

Lm12: [*1,0*] = 1 + (0 * <i> )
by COMPLEX1:27;

theorem :: SIN_COS3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX
for n being Nat holds sin_C /. (z + ((2 * n) * PI )) = sin_C /. z
proof end;

theorem :: SIN_COS3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX
for n being Nat holds cos_C /. (z + ((2 * n) * PI )) = cos_C /. z
proof end;

theorem Th36: :: SIN_COS3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds exp (<i> * z) = (cos_C /. z) + (<i> * (sin_C /. z))
proof end;

theorem Th37: :: SIN_COS3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds exp (- (<i> * z)) = (cos_C /. z) - (<i> * (sin_C /. z))
proof end;

Lm13: for x, y being Element of REAL holds <i> * [*x,y*] = [*(- y),x*]
proof end;

theorem Th38: :: SIN_COS3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of REAL holds sin_C /. [*x,0*] = sin . x
proof end;

theorem Th39: :: SIN_COS3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of REAL holds cos_C /. [*x,0*] = cos . x
proof end;

theorem Th40: :: SIN_COS3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of REAL holds sinh_C /. [*x,0*] = sinh . x
proof end;

theorem Th41: :: SIN_COS3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of REAL holds cosh_C /. [*x,0*] = cosh . x
proof end;

theorem :: SIN_COS3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds [*x,0*] + (<i> * [*y,0*]) = [*x,y*]
proof end;

theorem Th43: :: SIN_COS3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds sin_C /. [*x,y*] = [*((sin . x) * (cosh . y)),((cos . x) * (sinh . y))*]
proof end;

theorem Th44: :: SIN_COS3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds sin_C /. [*x,(- y)*] = [*((sin . x) * (cosh . y)),(- ((cos . x) * (sinh . y)))*]
proof end;

theorem Th45: :: SIN_COS3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds cos_C /. [*x,y*] = [*((cos . x) * (cosh . y)),(- ((sin . x) * (sinh . y)))*]
proof end;

theorem Th46: :: SIN_COS3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds cos_C /. [*x,(- y)*] = [*((cos . x) * (cosh . y)),((sin . x) * (sinh . y))*]
proof end;

theorem Th47: :: SIN_COS3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds sinh_C /. [*x,y*] = [*((sinh . x) * (cos . y)),((cosh . x) * (sin . y))*]
proof end;

theorem Th48: :: SIN_COS3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds sinh_C /. [*x,(- y)*] = [*((sinh . x) * (cos . y)),(- ((cosh . x) * (sin . y)))*]
proof end;

theorem Th49: :: SIN_COS3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds cosh_C /. [*x,y*] = [*((cosh . x) * (cos . y)),((sinh . x) * (sin . y))*]
proof end;

theorem Th50: :: SIN_COS3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds cosh_C /. [*x,(- y)*] = [*((cosh . x) * (cos . y)),(- ((sinh . x) * (sin . y)))*]
proof end;

theorem Th51: :: SIN_COS3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for z being Element of COMPLEX holds ((cos_C /. z) + (<i> * (sin_C /. z))) #N n = (cos_C /. ([*n,0*] * z)) + (<i> * (sin_C /. ([*n,0*] * z)))
proof end;

theorem Th52: :: SIN_COS3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for z being Element of COMPLEX holds ((cos_C /. z) - (<i> * (sin_C /. z))) #N n = (cos_C /. ([*n,0*] * z)) - (<i> * (sin_C /. ([*n,0*] * z)))
proof end;

theorem :: SIN_COS3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for z being Element of COMPLEX holds exp ((<i> * [*n,0*]) * z) = ((cos_C /. z) + (<i> * (sin_C /. z))) #N n
proof end;

theorem :: SIN_COS3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for z being Element of COMPLEX holds exp (- ((<i> * [*n,0*]) * z)) = ((cos_C /. z) - (<i> * (sin_C /. z))) #N n
proof end;

theorem :: SIN_COS3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds (([*1,(- 1)*] / 2) * (sinh_C /. [*x,y*])) + (([*1,1*] / 2) * (sinh_C /. [*x,(- y)*])) = [*(((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y))),0*]
proof end;

theorem :: SIN_COS3:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL holds (([*1,(- 1)*] / 2) * (cosh_C /. [*x,y*])) + (([*1,1*] / 2) * (cosh_C /. [*x,(- y)*])) = ((sinh . x) * (sin . y)) + ((cosh . x) * (cos . y))
proof end;

theorem :: SIN_COS3:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2
proof end;

theorem Th58: :: SIN_COS3:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2
proof end;

theorem Th59: :: SIN_COS3:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of COMPLEX holds
( sinh_C /. (2 * z) = (2 * (sinh_C /. z)) * (cosh_C /. z) & cosh_C /. (2 * z) = ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 )
proof end;

theorem Th60: :: SIN_COS3:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds
( ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) )
proof end;

theorem Th61: :: SIN_COS3:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds
( (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) & (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) )
proof end;

theorem :: SIN_COS3:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds
( (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (sinh_C /. (2 * z1)) - (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) )
proof end;

Lm14: for z1 being Element of COMPLEX holds (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1
proof end;

theorem :: SIN_COS3:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z1, z2 being Element of COMPLEX holds
( (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) = (2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (cosh_C /. (2 * z1)) - (cosh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) )
proof end;