:: by Takashi Mitsuishi , Noboru Endou and Keiji Ohkubo

::

:: Received October 10, 2002

:: Copyright (c) 2002-2017 Association of Mizar Users

definition

ex b_{1} being Function of COMPLEX,COMPLEX st

for z being Complex holds b_{1} . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>)

for b_{1}, b_{2} being Function of COMPLEX,COMPLEX st ( for z being Complex holds b_{1} . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>) ) & ( for z being Complex holds b_{2} . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>) ) holds

b_{1} = b_{2}
end;

func sin_C -> Function of COMPLEX,COMPLEX means :Def1: :: SIN_COS3:def 1

for z being Complex holds it . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>);

existence for z being Complex holds it . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>);

ex b

for z being Complex holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines sin_C SIN_COS3:def 1 :

for b_{1} being Function of COMPLEX,COMPLEX holds

( b_{1} = sin_C iff for z being Complex holds b_{1} . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>) );

for b

( b

definition

ex b_{1} being Function of COMPLEX,COMPLEX st

for z being Complex holds b_{1} . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2

for b_{1}, b_{2} being Function of COMPLEX,COMPLEX st ( for z being Complex holds b_{1} . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ) & ( for z being Complex holds b_{2} . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 ) holds

b_{1} = b_{2}
end;

func cos_C -> Function of COMPLEX,COMPLEX means :Def2: :: SIN_COS3:def 2

for z being Complex holds it . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2;

existence for z being Complex holds it . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2;

ex b

for z being Complex holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines cos_C SIN_COS3:def 2 :

for b_{1} being Function of COMPLEX,COMPLEX holds

( b_{1} = cos_C iff for z being Complex holds b_{1} . z = ((exp (<i> * z)) + (exp (- (<i> * z)))) / 2 );

for b

( b

definition

ex b_{1} being Function of COMPLEX,COMPLEX st

for z being Complex holds b_{1} . z = ((exp z) - (exp (- z))) / 2

for b_{1}, b_{2} being Function of COMPLEX,COMPLEX st ( for z being Complex holds b_{1} . z = ((exp z) - (exp (- z))) / 2 ) & ( for z being Complex holds b_{2} . z = ((exp z) - (exp (- z))) / 2 ) holds

b_{1} = b_{2}
end;

func sinh_C -> Function of COMPLEX,COMPLEX means :Def3: :: SIN_COS3:def 3

for z being Complex holds it . z = ((exp z) - (exp (- z))) / 2;

existence for z being Complex holds it . z = ((exp z) - (exp (- z))) / 2;

ex b

for z being Complex holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines sinh_C SIN_COS3:def 3 :

for b_{1} being Function of COMPLEX,COMPLEX holds

( b_{1} = sinh_C iff for z being Complex holds b_{1} . z = ((exp z) - (exp (- z))) / 2 );

for b

( b

definition

ex b_{1} being Function of COMPLEX,COMPLEX st

for z being Complex holds b_{1} . z = ((exp z) + (exp (- z))) / 2

for b_{1}, b_{2} being Function of COMPLEX,COMPLEX st ( for z being Complex holds b_{1} . z = ((exp z) + (exp (- z))) / 2 ) & ( for z being Complex holds b_{2} . z = ((exp z) + (exp (- z))) / 2 ) holds

b_{1} = b_{2}
end;

func cosh_C -> Function of COMPLEX,COMPLEX means :Def4: :: SIN_COS3:def 4

for z being Complex holds it . z = ((exp z) + (exp (- z))) / 2;

existence for z being Complex holds it . z = ((exp z) + (exp (- z))) / 2;

ex b

for z being Complex holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines cosh_C SIN_COS3:def 4 :

for b_{1} being Function of COMPLEX,COMPLEX holds

( b_{1} = cosh_C iff for z being Complex holds b_{1} . z = ((exp z) + (exp (- z))) / 2 );

for b

( b

Lm1: for z being Complex holds sinh_C /. z = ((exp z) - (exp (- z))) / 2

by Def3;

Lm2: for z being Complex holds cosh_C /. z = ((exp z) + (exp (- z))) / 2

by Def4;

Lm3: for z being Complex holds (exp z) * (exp (- z)) = 1

proof end;

theorem :: SIN_COS3:1

for z being Element of COMPLEX holds ((sin_C /. z) * (sin_C /. z)) + ((cos_C /. z) * (cos_C /. z)) = 1

proof end;

theorem Th4: :: SIN_COS3:4

for z1, z2 being Complex holds sin_C /. (z1 + z2) = ((sin_C /. z1) * (cos_C /. z2)) + ((cos_C /. z1) * (sin_C /. z2))

proof end;

theorem :: SIN_COS3:5

for z1, z2 being 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

for z1, z2 being Complex holds cos_C /. (z1 + z2) = ((cos_C /. z1) * (cos_C /. z2)) - ((sin_C /. z1) * (sin_C /. z2))

proof end;

theorem :: SIN_COS3:7

for z1, z2 being Complex holds cos_C /. (z1 - z2) = ((cos_C /. z1) * (cos_C /. z2)) + ((sin_C /. z1) * (sin_C /. z2))

proof end;

registration
end;

theorem Th11: :: SIN_COS3:11

for z1, z2 being 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

for z1, z2 being 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

for z1, z2 being 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

for z1, z2 being Complex holds cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))

proof end;

Lm4: for x, y being Real holds exp (x + (y * <i>)) = (exp_R x) * ((cos y) + ((sin y) * <i>))

proof end;

theorem Th19: :: SIN_COS3:19

for x, y being Real holds exp (x + (y * <i>)) = ((exp_R . x) * (cos . y)) + (((exp_R . x) * (sin . y)) * <i>)

proof end;

theorem Th42: :: SIN_COS3:42

for x, y being Real holds sin_C /. (x + (y * <i>)) = ((sin . x) * (cosh . y)) + (((cos . x) * (sinh . y)) * <i>)

proof end;

theorem Th43: :: SIN_COS3:43

for x, y being Real holds sin_C /. (x + ((- y) * <i>)) = ((sin . x) * (cosh . y)) + ((- ((cos . x) * (sinh . y))) * <i>)

proof end;

theorem Th44: :: SIN_COS3:44

for x, y being Real holds cos_C /. (x + (y * <i>)) = ((cos . x) * (cosh . y)) + ((- ((sin . x) * (sinh . y))) * <i>)

proof end;

theorem Th45: :: SIN_COS3:45

for x, y being Real holds cos_C /. (x + ((- y) * <i>)) = ((cos . x) * (cosh . y)) + (((sin . x) * (sinh . y)) * <i>)

proof end;

theorem Th46: :: SIN_COS3:46

for x, y being Real holds sinh_C /. (x + (y * <i>)) = ((sinh . x) * (cos . y)) + (((cosh . x) * (sin . y)) * <i>)

proof end;

theorem Th47: :: SIN_COS3:47

for x, y being Real holds sinh_C /. (x + ((- y) * <i>)) = ((sinh . x) * (cos . y)) + ((- ((cosh . x) * (sin . y))) * <i>)

proof end;

theorem Th48: :: SIN_COS3:48

for x, y being Real holds cosh_C /. (x + (y * <i>)) = ((cosh . x) * (cos . y)) + (((sinh . x) * (sin . y)) * <i>)

proof end;

theorem Th49: :: SIN_COS3:49

for x, y being Real holds cosh_C /. (x + ((- y) * <i>)) = ((cosh . x) * (cos . y)) + ((- ((sinh . x) * (sin . y))) * <i>)

proof end;

:: De Moivre's Theorem

theorem Th50: :: SIN_COS3:50

for n being Element of NAT

for z being Complex holds ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z)))

for z being Complex holds ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z)))

proof end;

theorem Th51: :: SIN_COS3:51

for n being Element of NAT

for z being Complex holds ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z)))

for z being Complex holds ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) - (<i> * (sin_C /. (n * z)))

proof end;

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

for z being Element of COMPLEX holds exp ((<i> * n) * z) = ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n

proof end;

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

for z being Element of COMPLEX holds exp (- ((<i> * n) * z)) = ((cos_C /. z) - (<i> * (sin_C /. z))) |^ n

proof end;

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))

proof end;

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))

proof end;

theorem Th58: :: SIN_COS3:58

for z being 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 )

( 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 Th59: :: SIN_COS3:59

for z1, z2 being 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)) )

( ((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 Th60: :: SIN_COS3:60

for z1, z2 being 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)) )

( (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:61

for z1, z2 being 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)) )

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

Lm5: for z1 being Complex holds (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1

proof end;

theorem :: SIN_COS3:62

for z1, z2 being 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)) )

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