The abstract of the Mizar article:

Trigonometric Functions on Complex Space

by

Takashi Mitsuishi,

Noboru Endou, and

Keiji Ohkubo

Received October 10, 2002

MML identifier: SIN_COS3

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, FINSEQ_4, ORDINAL2, COMPLEX1, SIN_COS, PREPOWER, SIN_COS2,
      SIN_COS3, FUNCT_1, ARYTM_1, ARYTM_3, XCMPLX_0;
 notation SUBSET_1, NUMBERS, REAL_1, RELAT_1, NAT_1, FINSEQ_4, ARYTM_0,
      COMPLEX1, FUNCT_2, SEQ_1, COMSEQ_3, SIN_COS, SIN_COS2;
 constructors NAT_1, COMSEQ_1, COMSEQ_3, REAL_1, SEQ_1, FINSEQ_4, SIN_COS,
      SIN_COS2, COMPLEX1, MEMBERED, INT_1, ARYTM_0, ARYTM_3, FUNCT_4;
 clusters RELSET_1, COMPLEX1, MEMBERED, ORDINAL2, NUMBERS;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin  :: Definitions of trigonometric functions

 reserve x,y for Element of REAL;
 reserve z,z1,z2 for Element of COMPLEX;
 reserve n for Nat;
  func sin_C -> Function of COMPLEX, COMPLEX means
:: SIN_COS3:def 1
  it.z = (exp(<i>*z)-(exp(-<i> * z)))/([*2,0*] * <i>);
end;
  func cos_C -> Function of COMPLEX,COMPLEX means
:: SIN_COS3:def 2
  it.z = (exp(<i>*z) + exp(-<i>*z))/[*2,0*];
end;
  func sinh_C -> Function of COMPLEX,COMPLEX means
:: SIN_COS3:def 3
  it.z = (exp(z) - exp(-z))/[*2,0*];
end;
  func cosh_C -> Function of COMPLEX,COMPLEX means
:: SIN_COS3:def 4
  it.z = (exp(z) + exp(-z))/[*2,0*];
end;

begin  :: Properties of trigonometric functions on complex space

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

theorem :: SIN_COS3:2
-sin_C/.z = sin_C/.(-z);

theorem :: SIN_COS3:3
cos_C/.z = cos_C/.(-z);

theorem :: SIN_COS3:4
sin_C/.(z1+z2) = (sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2);

theorem :: SIN_COS3:5
  sin_C/.(z1-z2) = (sin_C/.z1)*(cos_C/.z2) - (cos_C/.z1)*(sin_C/.z2);

theorem :: SIN_COS3:6
cos_C/.(z1+z2) = (cos_C/.z1)*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2);

theorem :: SIN_COS3:7
  cos_C/.(z1-z2) = (cos_C/.z1)*(cos_C/.z2) + (sin_C/.z1)*(sin_C/.z2);

theorem :: SIN_COS3:8
(cosh_C/.z)*(cosh_C/.z) - (sinh_C/.z)*(sinh_C/.z) = 1r;

theorem :: SIN_COS3:9
-sinh_C/.z = sinh_C/.(-z);

theorem :: SIN_COS3:10
cosh_C/.z = cosh_C/.(-z);

theorem :: SIN_COS3:11
sinh_C/.(z1+z2) = (sinh_C/.z1)*(cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2);

theorem :: SIN_COS3:12
sinh_C/.(z1-z2) = (sinh_C/.z1)*(cosh_C/.z2) - (cosh_C/.z1)*(sinh_C/.z2);

theorem :: SIN_COS3:13
cosh_C/.(z1-z2) = (cosh_C/.z1)*(cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2);

theorem :: SIN_COS3:14
cosh_C/.(z1+z2) = (cosh_C/.z1)*(cosh_C/.z2) + (sinh_C/.z1)*(sinh_C/.z2);

theorem :: SIN_COS3:15
sin_C/.(<i>*z) = <i>*sinh_C/.z;

theorem :: SIN_COS3:16
cos_C/.(<i>*z) = cosh_C/.z;

theorem :: SIN_COS3:17
sinh_C/.(<i>*z) = <i>*sin_C/.z;

theorem :: SIN_COS3:18
cosh_C/.(<i>*z) = cos_C/.z;

theorem :: SIN_COS3:19
for x,y being Element of REAL holds
exp([*x,y*]) = [*(exp.x)*(cos.y),(exp.x)*(sin.y)*];

theorem :: SIN_COS3:20
exp(0c) = [*1,0*];

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

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

theorem :: SIN_COS3:23
cos_C/.0c = [*1,0*];

theorem :: SIN_COS3:24
  cosh_C/.0c = [*1,0*];

theorem :: SIN_COS3:25
  exp(z) = cosh_C/.z + sinh_C/.z;

theorem :: SIN_COS3:26
  exp(-z) = cosh_C/.z - sinh_C/.z;

theorem :: SIN_COS3:27
  exp(z+[*2*PI,0*]*<i>) = exp(z) &
exp(z+[*0,2*PI*]) = exp(z);

theorem :: SIN_COS3:28
exp([*0,2*PI*n*]) = [*1,0*] & exp([*2*PI*n,0*]*<i>) = [*1,0*];

theorem :: SIN_COS3:29
exp([*0,-2*PI*n*]) = [*1,0*] & exp([*-2*PI*n,0*]*<i>) = [*1,0*];

theorem :: SIN_COS3:30
  exp([*0,(2*n+1)*PI*]) = [*-1,0*] & exp([*(2*n+1)*PI,0*]*<i>) = [*-1,0*];

theorem :: SIN_COS3:31
  exp([*0,-(2*n+1)*PI*]) = [*-1,0*] & exp([*-(2*n+1)*PI,0*]*<i>) = [*-1,0*];

theorem :: SIN_COS3:32
  exp([*0,(2*n + 1/2)*PI*]) = [*0,1*] & exp([*(2*n + 1/2)*PI,0*]*<i>) = [*0,1*]
;

theorem :: SIN_COS3:33
  exp([*0,-(2*n + 1/2)*PI*]) = [*0,-1*] &
exp([*-(2*n + 1/2)*PI,0*]*<i>) = [*0,-1*];

theorem :: SIN_COS3:34
  sin_C/.(z + [*2*n*PI,0*]) = sin_C/.z;

theorem :: SIN_COS3:35
  cos_C/.(z + [*2*n*PI,0*]) = cos_C/.z;

theorem :: SIN_COS3:36
exp(<i>*z) = cos_C/.z + <i>*sin_C/.z;

theorem :: SIN_COS3:37
exp(-<i>*z) = cos_C/.z - <i>*sin_C/.z;

theorem :: SIN_COS3:38
for x being Element of REAL holds
sin_C/.[*x,0*] = [*sin.x,0*];

theorem :: SIN_COS3:39
for x being Element of REAL holds
cos_C/.[*x,0*] = [*cos.x,0*];

theorem :: SIN_COS3:40
for x being Element of REAL holds
sinh_C/.[*x,0*] = [*sinh.x,0*];

theorem :: SIN_COS3:41
for x being Element of REAL holds
cosh_C/.[*x,0*] = [*cosh.x,0*];

theorem :: SIN_COS3:42
  for x,y being Element of REAL holds
[*x,y*] = [*x,0*] + <i>*[*y,0*];

theorem :: SIN_COS3:43
sin_C/.[*x,y*] = [*sin.x*cosh.y,cos.x*sinh.y*];

theorem :: SIN_COS3:44
sin_C/.[*x,-y*] = [*sin.x*cosh.y,-cos.x*sinh.y*];

theorem :: SIN_COS3:45
cos_C/.[*x,y*] = [*cos.x*cosh.y,-sin.x*sinh.y*];

theorem :: SIN_COS3:46
cos_C/.[*x,-y*] = [*cos.x*cosh.y,sin.x*sinh.y*];

theorem :: SIN_COS3:47
sinh_C/.[*x,y*] = [*sinh.x*cos.y,cosh.x*sin.y*];

theorem :: SIN_COS3:48
sinh_C/.[*x,-y*] = [*sinh.x*cos.y,-cosh.x*sin.y*];

theorem :: SIN_COS3:49
cosh_C/.[*x,y*] = [*cosh.x*cos.y,sinh.x*sin.y*];

theorem :: SIN_COS3:50
cosh_C/.[*x,-y*] = [*cosh.x*cos.y,-sinh.x*sin.y*];

theorem :: SIN_COS3:51
for n being Nat, 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);

theorem :: SIN_COS3:52
for n being Nat, 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);

theorem :: SIN_COS3:53
  for n being Nat, z being Element of COMPLEX holds
exp(<i>*[*n,0*]*z) = (cos_C/.z + <i>*sin_C/.z) #N n;

theorem :: SIN_COS3:54
  for n being Nat, z being Element of COMPLEX holds
exp(-<i>*[*n,0*]*z) = (cos_C/.z - <i>*sin_C/.z) #N n;

theorem :: SIN_COS3:55
  for x,y being Element of REAL holds
[*1,-1*]/[*2,0*]*sinh_C/.[*x,y*] + [*1,1*]/[*2,0*]*sinh_C/.[*x,-y*]
= [*sinh.x*cos.y + cosh.x*sin.y,0*];

theorem :: SIN_COS3:56
  for x,y being Element of REAL holds
[*1,-1*]/[*2,0*]*cosh_C/.[*x,y*] + [*1,1*]/[*2,0*]*cosh_C/.[*x,-y*]
= [*sinh.x*sin.y + cosh.x*cos.y,0*];

theorem :: SIN_COS3:57
  sinh_C/.z*sinh_C/.z = (cosh_C/.([*2,0*]*z) - [*1,0*])/[*2,0*];

theorem :: SIN_COS3:58
cosh_C/.z*cosh_C/.z = (cosh_C/.([*2,0*]*z) + [*1,0*])/[*2,0*];

theorem :: SIN_COS3:59
sinh_C/.([*2,0*]*z) = [*2,0*]*(sinh_C/.z)*(cosh_C/.z) &
cosh_C/.([*2,0*]*z) = [*2,0*]*(cosh_C/.z)*(cosh_C/.z) - [*1,0*];

theorem :: SIN_COS3:60
 (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);

theorem :: SIN_COS3:61
 (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);

theorem :: SIN_COS3:62
    sinh_C/.([*2,0*]*z1) + sinh_C/.([*2,0*]*z2)
= [*2,0*]*sinh_C/.(z1+z2)*cosh_C/.(z1-z2)
&
  sinh_C/.([*2,0*]*z1) - sinh_C/.([*2,0*]*z2)
= [*2,0*]*sinh_C/.(z1-z2)*cosh_C/.(z1+z2);

theorem :: SIN_COS3:63
   cosh_C/.([*2,0*]*z1) + cosh_C/.([*2,0*]*z2)
=[*2,0*]*cosh_C/.(z1+z2)*cosh_C/.(z1-z2)
 &
 cosh_C/.([*2,0*]*z1) - cosh_C/.([*2,0*]*z2)
=[*2,0*]*sinh_C/.(z1+z2)*sinh_C/.(z1-z2);