Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

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

Back to top