:: Trigonometric Functions on Complex Space
:: by Takashi Mitsuishi , Noboru Endou and Keiji Ohkubo
::
:: Received October 10, 2002
:: Copyright (c) 2002-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, NUMBERS, FUNCT_1, ORDINAL2, XCMPLX_0, RELAT_1, ARYTM_1,
ARYTM_3, PARTFUN1, COMPLEX1, SIN_COS, CARD_1, SIN_COS2, PREPOWER,
SIN_COS3, FUNCT_7, REAL_1, NEWTON, NAT_1;
notations SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, XREAL_0,
REAL_1, NAT_1, PARTFUN1, FUNCT_2, COMSEQ_3, SIN_COS, SIN_COS2;
constructors FUNCT_4, ARYTM_0, REAL_1, NAT_1, BINOP_2, PARTFUN1, COMSEQ_3,
SIN_COS, SIN_COS2, RVSUM_1, XXREAL_0, FCONT_1;
registrations NUMBERS, XCMPLX_0, MEMBERED, RELSET_1, XREAL_0, SIN_COS,
VALUED_0, CFUNCT_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Definitions of trigonometric functions
reserve x,y for Real;
reserve z,z1,z2 for Complex;
reserve n for Element of NAT;
definition
func sin_C -> Function of COMPLEX, COMPLEX means
:: SIN_COS3:def 1
it.z = (exp(**z)-( exp(-** * z)))/(2 * **);
end;
definition
func cos_C -> Function of COMPLEX,COMPLEX means
:: SIN_COS3:def 2
it.z = (exp(***z) + exp(-***z))/2;
end;
definition
func sinh_C -> Function of COMPLEX,COMPLEX means
:: SIN_COS3:def 3
it.z = (exp(z) - exp (-z))/2;
end;
definition
func cosh_C -> Function of COMPLEX,COMPLEX means
:: SIN_COS3:def 4
it.z = (exp(z) + exp (-z))/2;
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) = 1;
theorem :: SIN_COS3:2
for z being Complex holds -sin_C/.z = sin_C/.(-z);
theorem :: SIN_COS3:3
for z being Complex holds cos_C/.z = cos_C/.(-z);
theorem :: 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);
theorem :: SIN_COS3:5
sin_C/.(z1-z2) = (sin_C/.z1)*(cos_C/.z2) - (cos_C/.z1)*(sin_C/.z2);
theorem :: 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);
theorem :: SIN_COS3:7
cos_C/.(z1-z2) = (cos_C/.z1)*(cos_C/.z2) + (sin_C/.z1)*(sin_C/.z2);
registration
let p be Function of COMPLEX,COMPLEX, i be Complex;
identify p/.i with p.i;
end;
theorem :: SIN_COS3:8
(cosh_C/.z)*(cosh_C/.z) - (sinh_C/.z)*(sinh_C/.z) = 1;
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
for z being Complex holds sin_C/.(***z) = ***sinh_C/.z;
theorem :: SIN_COS3:16
for z being Complex holds cos_C/.(***z) = cosh_C/.z;
theorem :: SIN_COS3:17
for z being Complex holds sinh_C/.(***z) = ***sin_C/.z;
theorem :: SIN_COS3:18
for z being Complex holds cosh_C/.(***z) = cos_C/.z;
theorem :: SIN_COS3:19
for x,y holds exp(x+y***) = (exp_R.x)*(
cos.y)+(exp_R.x)*(sin.y)***;
theorem :: SIN_COS3:20
exp(0c) = 1;
theorem :: SIN_COS3:21
sin_C/.0c = 0;
theorem :: SIN_COS3:22
sinh_C/.0c = 0;
theorem :: SIN_COS3:23
cos_C/.0c = 1;
theorem :: SIN_COS3:24
cosh_C/.0c = 1;
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***) = exp(z);
theorem :: SIN_COS3:28
exp(2*PI*n***) = 1;
theorem :: SIN_COS3:29
exp((-2*PI*n)***) = 1;
theorem :: SIN_COS3:30
exp((2*n+1)*PI***) = -1;
theorem :: SIN_COS3:31
exp((-(2*n+1)*PI)***) = -1;
theorem :: SIN_COS3:32
exp((2*n + 1/2)*PI***) = **;
theorem :: SIN_COS3:33
exp((-(2*n + 1/2)*PI)***) = -1***;
theorem :: SIN_COS3:34
sin_C/.(z + 2*n*PI) = sin_C/.z;
theorem :: SIN_COS3:35
cos_C/.(z + 2*n*PI) = cos_C/.z;
theorem :: SIN_COS3:36
for z being Complex holds exp(***z) = cos_C/.z + *** sin_C/.z;
theorem :: SIN_COS3:37
for z being Complex holds exp(-***z) = cos_C/.z - *** sin_C/.z;
theorem :: SIN_COS3:38
for x holds sin_C/.x = sin.x;
theorem :: SIN_COS3:39
for x holds cos_C/.x = cos.x;
theorem :: SIN_COS3:40
for x holds sinh_C/.x = sinh.x;
theorem :: SIN_COS3:41
for x holds cosh_C/.x = cosh.x;
theorem :: SIN_COS3:42
sin_C/.(x+y***) = sin.x*(cosh.y qua Real)+cos.x*sinh.y***;
theorem :: SIN_COS3:43
sin_C/.(x+(-y)***) = sin.x*cosh.y+(-cos.x*sinh.y)***;
theorem :: SIN_COS3:44
cos_C/.(x+y***) = cos.x*cosh.y+(-sin.x*sinh.y)***;
theorem :: SIN_COS3:45
cos_C/.(x+(-y)***) = cos.x*cosh.y+sin.x*sinh.y***;
theorem :: SIN_COS3:46
sinh_C/.(x+y***) = sinh.x*cos.y+cosh.x*sin.y***;
theorem :: SIN_COS3:47
sinh_C/.(x+(-y)***) = sinh.x*cos.y+(-cosh.x*sin.y)***;
theorem :: SIN_COS3:48
cosh_C/.(x+y***) = cosh.x*cos.y+sinh.x*sin.y***;
theorem :: SIN_COS3:49
cosh_C/.(x+(-y)***) = cosh.x*cos.y+(-sinh.x*sin.y)***;
::$N De Moivre's Theorem
theorem :: SIN_COS3:50
for n being Element of NAT, z being Complex holds (
cos_C/.z + ***sin_C/.z) |^ n = cos_C/.(n*z) + ***sin_C/.(n*z);
theorem :: SIN_COS3:51
for n being Element of NAT, z being Complex holds (
cos_C/.z - ***sin_C/.z) |^ n = cos_C/.(n*z) - ***sin_C/.(n*z);
theorem :: SIN_COS3:52
for n being Element of NAT, z being Element of COMPLEX holds exp(***n
*z) = (cos_C/.z + ***sin_C/.z) |^ n;
theorem :: SIN_COS3:53
for n being Element of NAT, z being Element of COMPLEX holds exp(-***
n*z) = (cos_C/.z - ***sin_C/.z) |^ n;
theorem :: SIN_COS3:54
for x,y being Element of REAL holds (1+(-1)***)/2*sinh_C/.(x+y***) +
(1+**)/2*sinh_C/.(x+(-y)***) = sinh.x*cos.y + cosh.x*sin.y;
theorem :: SIN_COS3:55
for x,y being Element of REAL holds (1+(-1)***)/2*cosh_C/.(x+y***) +
(1+**)/2*cosh_C/.(x+(-y)***) = sinh.x*sin.y + cosh.x*cos.y;
theorem :: SIN_COS3:56
sinh_C/.z*sinh_C/.z = (cosh_C/.(2*z) - 1)/2;
theorem :: SIN_COS3:57
cosh_C/.z*cosh_C/.z = (cosh_C/.(2*z) + 1)/2;
theorem :: SIN_COS3:58
sinh_C/.(2*z) = 2*(sinh_C/.z)*(cosh_C/.z) & cosh_C/.(2*z) = 2*(
cosh_C/.z)*(cosh_C/.z) - 1;
theorem :: SIN_COS3:59
(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:60
(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:61
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);
theorem :: SIN_COS3:62
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);
*