:: Trigonometric Functions on Complex Space
:: by Takashi Mitsuishi , Noboru Endou and Keiji Ohkubo
::
:: Received October 10, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

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>)
proofend;
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>) ) &amp; ( for z being Element of COMPLEX holds b2 . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>) ) holds
b1 = b2
proofend;
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
proofend;
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 ) &amp; ( for z being Element of COMPLEX holds b2 . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ) holds
b1 = b2
proofend;
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
proofend;
uniqueness
 for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) - (exp (- z))) / 2 ) &amp; ( for z being Element of COMPLEX holds b2 . z = ((exp z) - (exp (- z))) / 2 ) holds
b1 = b2
proofend;
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
proofend;
uniqueness
 for b1, b2 being Function of COMPLEX,COMPLEX st ( for z being Element of COMPLEX holds b1 . z = ((exp z) + (exp (- z))) / 2 ) &amp; ( for z being Element of COMPLEX holds b2 . z = ((exp z) + (exp (- z))) / 2 ) holds
b1 = b2
proofend;
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 );

Lm1:  for z being complex number holds sinh_C /. z = ((exp z) - (exp (- z))) / 2
proofend;

Lm2:  for z being complex number holds cosh_C /. z = ((exp z) + (exp (- z))) / 2
proofend;

Lm3:  for z being Element of COMPLEX holds (exp z) * (exp (- z)) = 1
proofend;

begin

theorem :: SIN_COS3:1
for z being Element of COMPLEX holds ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1
proofend;

theorem Th2: :: SIN_COS3:2
for z being complex number holds - (sin_C /. z) = sin_C /. (- z)
proofend;

theorem Th3: :: SIN_COS3:3
for z being complex number holds cos_C /. z = cos_C /. (- z)
proofend;

theorem Th4: :: SIN_COS3:4
for z1, z2 being complex number holds sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))
proofend;

theorem :: SIN_COS3:5
for z1, z2 being Element of COMPLEX holds sin_C /. (z1 - z2) = ((sin_C /. z1) * (cos_C /. z2)) - ((cos_C /. z1) * (sin_C /. z2))
proofend;

theorem Th6: :: SIN_COS3:6
for z1, z2 being complex number holds cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2))
proofend;

theorem :: SIN_COS3:7
for z1, z2 being Element of COMPLEX holds cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2))
proofend;

theorem Th8: :: SIN_COS3:8
for z being Element of COMPLEX holds ((cosh_C /. z) * (cosh_C /. z)) - ((sinh_C /. z) * (sinh_C /. z)) = 1
proofend;

theorem Th9: :: SIN_COS3:9
for z being Element of COMPLEX holds - (sinh_C /. z) = sinh_C /. (- z)
proofend;

theorem Th10: :: SIN_COS3:10
for z being Element of COMPLEX holds cosh_C /. z = cosh_C /. (- z)
proofend;

theorem Th11: :: SIN_COS3:11
for z1, z2 being Element of COMPLEX holds sinh_C /. (z1 + z2) = ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))
proofend;

theorem Th12: :: SIN_COS3:12
for z1, z2 being Element of COMPLEX holds sinh_C /. (z1 - z2) = ((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2))
proofend;

theorem Th13: :: SIN_COS3:13
for z1, z2 being Element of COMPLEX holds cosh_C /. (z1 - z2) = ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))
proofend;

theorem Th14: :: SIN_COS3:14
for z1, z2 being Element of COMPLEX holds cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))
proofend;

theorem Th15: :: SIN_COS3:15
for z being complex number holds sin_C /. (<i> * z) = <i> * (sinh_C /. z)
proofend;

theorem Th16: :: SIN_COS3:16
for z being complex number holds cos_C /. (<i> * z) = cosh_C /. z
proofend;

theorem Th17: :: SIN_COS3:17
for z being complex number holds sinh_C /. (<i> * z) = <i> * (sin_C /. z)
proofend;

theorem Th18: :: SIN_COS3:18
for z being complex number holds cosh_C /. (<i> * z) = cos_C /. z
proofend;

Lm4:  for x, y being Element of REAL holds exp (x + (y * <i>)) = (exp_R x) * ((cos y) + ((sin y) * <i>))
proofend;

theorem Th19: :: SIN_COS3:19
for x, y being Element of REAL holds exp (x + (y * <i>)) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * <i>)
proofend;

theorem :: SIN_COS3:20
exp 0c = 1 by SIN_COS:49, SIN_COS:51;

theorem Th21: :: SIN_COS3:21
sin_C /. 0c = 0
proofend;

theorem :: SIN_COS3:22
sinh_C /. 0c = 0
proofend;

theorem Th23: :: SIN_COS3:23
cos_C /. 0c = 1
proofend;

theorem :: SIN_COS3:24
cosh_C /. 0c = 1
proofend;

theorem :: SIN_COS3:25
for z being Element of COMPLEX holds exp z = (cosh_C /. z) + (sinh_C /. z)
proofend;

theorem :: SIN_COS3:26
for z being Element of COMPLEX holds exp (- z) = (cosh_C /. z) - (sinh_C /. z)
proofend;

theorem :: SIN_COS3:27
for z being Element of COMPLEX holds exp (z + ((2 * PI) * <i>)) = exp z
proofend;

theorem Th28: :: SIN_COS3:28
for n being Element of NAT holds exp (((2 * PI) * n) * <i>) = 1
proofend;

theorem Th29: :: SIN_COS3:29
for n being Element of NAT holds exp ((- ((2 * PI) * n)) * <i>) = 1
proofend;

theorem :: SIN_COS3:30
for n being Element of NAT holds exp ((((2 * n) + 1) * PI) * <i>) = - 1
proofend;

theorem :: SIN_COS3:31
for n being Element of NAT holds exp ((- (((2 * n) + 1) * PI)) * <i>) = - 1
proofend;

theorem :: SIN_COS3:32
for n being Element of NAT holds exp ((((2 * n) + (1 / 2)) * PI) * <i>) = <i>
proofend;

theorem :: SIN_COS3:33
for n being Element of NAT holds exp ((- (((2 * n) + (1 / 2)) * PI)) * <i>) = - (1 * <i>)
proofend;

theorem :: SIN_COS3:34
for z being Element of COMPLEX
for n being Element of NAT holds sin_C /. (z + ((2 * n) * PI)) = sin_C /. z
proofend;

theorem :: SIN_COS3:35
for z being Element of COMPLEX
for n being Element of NAT holds cos_C /. (z + ((2 * n) * PI)) = cos_C /. z
proofend;

theorem Th36: :: SIN_COS3:36
for z being complex number holds exp (<i> * z) = (cos_C /. z) + (<i> * (sin_C /. z))
proofend;

theorem Th37: :: SIN_COS3:37
for z being complex number holds exp (- (<i> * z)) = (cos_C /. z) - (<i> * (sin_C /. z))
proofend;

theorem Th38: :: SIN_COS3:38
for x being Element of REAL holds sin_C /. x = sin . x
proofend;

theorem Th39: :: SIN_COS3:39
for x being Element of REAL holds cos_C /. x = cos . x
proofend;

theorem Th40: :: SIN_COS3:40
for x being Element of REAL holds sinh_C /. x = sinh . x
proofend;

theorem Th41: :: SIN_COS3:41
for x being Element of REAL holds cosh_C /. x = cosh . x
proofend;

theorem Th42: :: SIN_COS3:42
for x, y being Element of REAL holds sin_C /. (x + (y * <i>)) = ((sin . x) * (cosh . y)) + (((cos . x) * (sinh . y)) * <i>)
proofend;

theorem Th43: :: SIN_COS3:43
for x, y being Element of REAL holds sin_C /. (x + ((- y) * <i>)) = ((sin . x) * (cosh . y)) + ((- ((cos . x) * (sinh . y))) * <i>)
proofend;

theorem Th44: :: SIN_COS3:44
for x, y being Element of REAL holds cos_C /. (x + (y * <i>)) = ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * <i>)
proofend;

theorem Th45: :: SIN_COS3:45
for x, y being Element of REAL holds cos_C /. (x + ((- y) * <i>)) = ((cos . x) * (cosh . y)) + (((sin . x) * (sinh . y)) * <i>)
proofend;

theorem Th46: :: SIN_COS3:46
for x, y being Element of REAL holds sinh_C /. (x + (y * <i>)) = ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * <i>)
proofend;

theorem Th47: :: SIN_COS3:47
for x, y being Element of REAL holds sinh_C /. (x + ((- y) * <i>)) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * <i>)
proofend;

theorem Th48: :: SIN_COS3:48
for x, y being Element of REAL holds cosh_C /. (x + (y * <i>)) = ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * <i>)
proofend;

theorem Th49: :: SIN_COS3:49
for x, y being Element of REAL holds cosh_C /. (x + ((- y) * <i>)) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * <i>)
proofend;

:: [WP: ] De_Moivre's_Theorem
theorem Th50: :: SIN_COS3:50
for n being Element of NAT
for z being Element of COMPLEX holds ((cos_C /. z) + (<i> * (sin_C /. z))) #N n = (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z)))
proofend;

theorem Th51: :: SIN_COS3:51
for n being Element of NAT
for z being Element of COMPLEX holds ((cos_C /. z) - (<i> * (sin_C /. z))) #N n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z)))
proofend;

theorem :: SIN_COS3:52
for n being Element of NAT
for z being Element of COMPLEX holds exp ((<i> * n) * z) = ((cos_C /. z) + (<i> * (sin_C /. z))) #N n
proofend;

theorem :: SIN_COS3:53
for n being Element of NAT
for z being Element of COMPLEX holds exp (- ((<i> * n) * z)) = ((cos_C /. z) - (<i> * (sin_C /. z))) #N n
proofend;

theorem :: SIN_COS3:54
for x, y being Element of REAL holds (((1 + ((- 1) * <i>)) / 2) * (sinh_C /. (x + (y * <i>)))) + (((1 + <i>) / 2) * (sinh_C /. (x + ((- y) * <i>)))) = ((sinh . x) * (cos . y)) + ((cosh . x) * (sin . y))
proofend;

theorem :: SIN_COS3:55
for x, y being Element of REAL holds (((1 + ((- 1) * <i>)) / 2) * (cosh_C /. (x + (y * <i>)))) + (((1 + <i>) / 2) * (cosh_C /. (x + ((- y) * <i>)))) = ((sinh . x) * (sin . y)) + ((cosh . x) * (cos . y))
proofend;

theorem :: SIN_COS3:56
for z being Element of COMPLEX holds (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2
proofend;

theorem Th57: :: SIN_COS3:57
for z being Element of COMPLEX holds (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2
proofend;

theorem Th58: :: SIN_COS3:58
for z being Element of COMPLEX holds
( sinh_C /. (2 * z) = (2 * (sinh_C /. z)) * (cosh_C /. z) &amp; cosh_C /. (2 * z) = ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 )
proofend;

theorem Th59: :: SIN_COS3:59
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)) &amp; ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) &amp; ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) )
proofend;

theorem Th60: :: SIN_COS3:60
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)) &amp; (cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) &amp; ((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) + ((sinh_C /. z2) * (sinh_C /. z2)) )
proofend;

theorem :: SIN_COS3:61
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)) &amp; (sinh_C /. (2 * z1)) - (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) )
proofend;

Lm5:  for z1 being Element of COMPLEX holds (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1
proofend;

theorem :: SIN_COS3:62
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)) &amp; (cosh_C /. (2 * z1)) - (cosh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) )
proofend;