:: Trigonometric Functions on Complex Space :: by Takashi Mitsuishi , Noboru Endou and Keiji Ohkubo :: :: Received October 10, 2002 :: Copyright (c) 2002-2021 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, 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);