:: Trigonometric Functions on Complex Space
:: by Takashi Mitsuishi , Noboru Endou and Keiji Ohkubo
::
:: Received October 10, 2002
:: Copyright (c) 2002-2016 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;
definitions FUNCT_2;
theorems COMPLEX1, SIN_COS, SIN_COS2, COMSEQ_3, XCMPLX_0, NUMBERS, XREAL_0;
schemes NAT_1, FUNCT_2;
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
:Def1:
it.z = (exp(**z)-( exp(-** * z)))/(2 * **);
existence
proof
deffunc U(Complex) = In((exp(***$1)-(exp(-** * $1)))/(2 * **),COMPLEX);
consider f being Function of COMPLEX, COMPLEX such that
A1: for z being Element of COMPLEX holds f.z = U(z) from FUNCT_2:sch 4;
take f;
let z be Complex;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
f.z = U(z) by A1;
hence thesis;
end;
uniqueness
proof let f1,f2 be Function of COMPLEX, COMPLEX such that
A2: f1.z = (exp(***z)-( exp(-** * z)))/(2 * **) and
A3: f2.z = (exp(***z)-( exp(-** * z)))/(2 * **);
let z be Element of COMPLEX;
thus f1.z = (exp(***z)-( exp(-** * z)))/(2 * **) by A2
.= f2.z by A3;
end;
end;
definition
func cos_C -> Function of COMPLEX,COMPLEX means
:Def2:
it.z = (exp(***z) + exp(-***z))/2;
existence
proof
deffunc U(Complex) = In((exp(***$1) + exp(-***$1))/2,COMPLEX);
consider f being Function of COMPLEX, COMPLEX such that
A1: for z being Element of COMPLEX holds f.z = U(z) from FUNCT_2:sch 4;
take f;
let z;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
f.z = U(z) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of COMPLEX,COMPLEX such that
A2: f1.z = (exp(***z) + exp(-***z))/2 and
A3: f2.z = (exp(***z) + exp(-***z))/2;
let z be Element of COMPLEX;
thus f1.z = (exp(***z) + exp(-***z))/2 by A2 .= f2.z by A3;
end;
end;
definition
func sinh_C -> Function of COMPLEX,COMPLEX means
:Def3:
it.z = (exp(z) - exp (-z))/2;
existence
proof
deffunc U(Complex) = In((exp $1 - exp (-$1))/2,COMPLEX);
consider f being Function of COMPLEX, COMPLEX such that
A1: for z being Element of COMPLEX holds f.z = U(z) from FUNCT_2:sch 4;
take f;
let z;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
f.z = U(z) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of COMPLEX,COMPLEX such that
A2: f1.z = (exp(z) - exp (-z))/2 and
A3: f2.z = (exp(z) - exp (-z))/2;
let z be Element of COMPLEX;
thus f1.z = (exp(z) - exp (-z))/2 by A2 .= f2.z by A3;
end;
end;
definition
func cosh_C -> Function of COMPLEX,COMPLEX means
:Def4:
it.z = (exp(z) + exp (-z))/2;
existence
proof
deffunc U(Complex) = In((exp $1 + exp (-$1))/2,COMPLEX);
consider f being Function of COMPLEX, COMPLEX such that
A1: for z being Element of COMPLEX holds f.z = U(z) from FUNCT_2:sch 4;
take f;
let z;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
f.z = U(z) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of COMPLEX,COMPLEX such that
A2: f1.z = (exp(z) + exp (-z))/2 and
A3: f2.z = (exp(z) + exp (-z))/2;
let z be Element of COMPLEX;
thus f1.z = (exp(z) + exp (-z))/2 by A2 .= f2.z by A3;
end;
end;
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 be Complex holds exp(z)*exp(-z) = 1
proof
let z be Complex;
thus exp(z)*exp(-z) = exp(z + -z) by SIN_COS:23
.= 1 by SIN_COS:49,51;
end;
begin :: Properties of trigonometric functions on complex space
theorem
for z being Element of COMPLEX holds (sin_C/.z)*(sin_C/.z) + (cos_C/.z
)*(cos_C/.z) = 1
proof
let z be Element of COMPLEX;
set z1 = exp(***z), z2 = exp(-***z);
(sin_C/.z)*(sin_C/.z) + (cos_C/.z)*(cos_C/.z) =(sin_C/.z)*(sin_C/.z) + (
cos_C/.z)*((exp(***z) + exp(-***z))/2) by Def2
.=(sin_C/.z)*(sin_C/.z) + ((z1 + z2)/2)*((z1 + z2)/2) by Def2
.=(z1 - z2)/(2***)*(sin_C/.z) + ((z1 + z2)/2)*((z1 + z2)/2) by Def1
.=((z1 - z2)/(2***))*((z1 - z2)/(2***)) + ((z1 + z2)/2)*((z1 + z2)/2)
by Def1
.=((z1*z2 + z1*z2) + (z1*z2 + z1*z2))/4
.=((1 + z1*exp(-(***z))) + (z1*exp(-(***z)) + z1*exp(-(***z)))) /4 by
Lm3
.=((1 + 1) + (z1*exp(-(***z)) + z1*exp(-(***z)))) /4 by Lm3
.=((1 + 1) + (z1*exp(-(***z)) + 1))/4 by Lm3
.=(2 + 2)/4 by Lm3;
hence thesis;
end;
theorem Th2:
for z being Complex holds -sin_C/.z = sin_C/.(-z)
proof
let z be Complex;
sin_C/.(-z) = (exp(***(-z)) - exp(-***(-z)))/(2***) by Def1
.= -((exp(***z) - exp(-***z))/(2***));
then -sin_C/.z = sin_C/.(-z) by Def1;
hence thesis;
end;
theorem Th3:
for z being Complex holds cos_C/.z = cos_C/.(-z)
proof
let z be Complex;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
cos_C/.(-z) = (exp(***(-z)) + exp(-***(-z)))/2 by Def2
.=(exp(-***z) + exp(***z))/2;
then cos_C/.z = cos_C/.(-z) by Def2;
hence thesis;
end;
theorem Th4:
for z1,z2 being Complex holds sin_C/.(z1+z2) = (sin_C/.z1)
*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2)
proof
let z1,z2 be Complex;
reconsider z1,z2 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider e1 = exp(***z1), e2 = exp(-***z1),
e3 = exp(***z2), e4 = exp(-***z2) as Element of COMPLEX;
(sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2) =((exp(***z1) - exp(-
***z1))/(2***))*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2) by Def1
.=((exp(***z1) - exp(-***z1))/(2***))*(cos_C/.z2) + (cos_C/.z1)*((exp
(***z2) - exp(-***z2))/(2***)) by Def1
.=((exp(***z1) - exp(-***z1))/(2***))* ((exp(-***z2) + exp(***z2))/
2) + (cos_C/.z1)*((exp(***z2) - exp(-***z2))/(2***)) by Def2
.=((exp(***z1) - exp(-***z1))*(exp(-***z2) + exp(***z2))) /(2****2)
+ ((exp(-***z1) + exp(***z1))/2)* ((exp(***z2) - exp(-***z2))/(2***))
by Def2
.=( e1*e3+e1*e3-(e1*e4+e2*e4 - (e1*e4-e2*e4)) ) /(2****2)
.=(Re(e1*e3)+Re(e1*e3)+(Im(e1*e3)+Im(e1*e3))***-(e2*e4 + e2*e4)) /(2*
***2) by COMPLEX1:81
.=((2*Re(e1*e3)+2*Im(e1*e3)***)-(e2*e4 + e2*e4)) /(2****2)
.=((Re(2*(e1*e3))+2*Im(e1*e3)***)-(e2*e4 + e2*e4)) /(2****2) by
COMSEQ_3:17
.=((Re(2*(e1*e3))+Im(2*(e1*e3))***)-(e2*e4 + e2*e4)) /(2****2) by
COMSEQ_3:17
.=(2*(e1*e3)-(e2*e4 + e2*e4)) /(2****2) by COMPLEX1:13
.=(2*(e1*e3)-(Re(e2*e4)+Re(e2*e4)+(Im(e2*e4)+Im(e2*e4))***)) /(2****2)
by COMPLEX1:81
.=(2*(e1*e3)-(2*Re(e2*e4)+2*Im(e2*e4)***)) /(2****2)
.=(2*(e1*e3)-(Re(2*(e2*e4))+2*Im(e2*e4)***)) /(2****2) by COMSEQ_3:17
.=(2*(e1*e3)-(Re(2*(e2*e4))+Im(2*(e2*e4))***)) /(2****2) by COMSEQ_3:17
.=(2*(e1*e3)-2*(e2*e4)) /(2****2) by COMPLEX1:13
.=(e1*e3)/(2***) -(2*(e2*e4))/(2****2)
.=exp(***z1+***z2)/(2***)-(e2*e4)/(2***) by SIN_COS:23
.=exp(***(z1+z2))/(2***)-exp(-***z1+-***z2)/(2***) by SIN_COS:23
.=( exp(***(z1+z2))-exp(-***(z1+z2)) )/(2***);
then
sin_C/.(z1+z2) = (sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2) by Def1;
hence thesis;
end;
theorem
sin_C/.(z1-z2) = (sin_C/.z1)*(cos_C/.z2) - (cos_C/.z1)*(sin_C/.z2)
proof
sin_C/.(z1-z2) = sin_C/.(z1 + -z2)
.=(sin_C/.z1)*(cos_C/.(-z2)) + (cos_C/.z1)*(sin_C/.(-z2)) by Th4
.=(sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.(-z2)) by Th3
.=(sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(-sin_C/.z2) by Th2
.=(sin_C/.z1)*(cos_C/.z2) + -(cos_C/.z1)*(sin_C/.z2);
hence thesis;
end;
theorem Th6:
for z1,z2 being Complex holds cos_C/.(z1+z2) = (cos_C/.z1)
*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2)
proof
let z1,z2 be Complex;
reconsider z1,z2 as Element of COMPLEX by XCMPLX_0:def 2;
set e1 = exp(***z1), e2 = exp(-***z1), e3 = exp(***z2), e4 = exp(-***z2);
(cos_C/.z1)*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2) =(cos_C/.z1)*(cos_C/.
z2) - ((exp(***z1) - exp(-***z1))/(2***))*(sin_C/.z2) by Def1
.=(cos_C/.z1)*(cos_C/.z2) - ((exp(***z1) - exp(-***z1))/(2***)) *((
exp(***z2) - exp(-***z2))/(2***)) by Def1
.=(cos_C/.z1)*((exp(***z2) + exp(-***z2))/2) - ((exp(***z1) - exp(-
***z1))/(2***)) *((exp(***z2) - exp(-***z2))/(2***)) by Def2
.=((e1 + e2)/2)*((e3 + e4)/2) - ((e1 - e2)/(2***))*((e3 - e4)/(2***))
by Def2
.=( e1*e3+e1*e3 + (e2*e4+e2*e4) )/(2*2)
.=(Re(e1*e3)+Re(e1*e3)+(Im(e1*e3)+Im(e1*e3))***+(e2*e4 + e2*e4)) /(2*2)
by COMPLEX1:81
.=((2*Re(e1*e3)+2*Im(e1*e3)***)+(e2*e4 + e2*e4)) /(2*2)
.=((Re(2*(e1*e3))+2*Im(e1*e3)***)+(e2*e4 + e2*e4)) /(2*2) by COMSEQ_3:17
.=((Re(2*(e1*e3))+Im(2*(e1*e3))***)+(e2*e4 + e2*e4)) /(2*2) by COMSEQ_3:17
.=(2*(e1*e3)+(e2*e4 + e2*e4))/(2*2) by COMPLEX1:13
.=(2*(e1*e3)+(Re(e2*e4)+Re(e2*e4)+(Im(e2*e4)+Im(e2*e4))***)) /(2*2) by
COMPLEX1:81
.=(2*(e1*e3)+(2*Re(e2*e4)+2*Im(e2*e4)***)) /(2*2)
.=(2*(e1*e3)+(Re(2*(e2*e4))+2*Im(e2*e4)***)) /(2*2) by COMSEQ_3:17
.=(2*(e1*e3)+(Re(2*(e2*e4))+Im(2*(e2*e4))***)) /(2*2) by COMSEQ_3:17
.=(2*(e1*e3)+2*(e2*e4))/(2*2) by COMPLEX1:13
.=(e1*e3)/(2)+(2*(e2*e4))/(2*2)
.=exp(***z1+***z2)/(2)+(e2*e4)/(2) by SIN_COS:23
.=exp(***(z1+z2))/(2)+exp(-***z1+-***z2)/(2) by SIN_COS:23
.=( exp(***(z1+z2))+exp(-***(z1+z2)) )/(2);
then
cos_C/.(z1+z2) = (cos_C/.z1)*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2) by Def2;
hence thesis;
end;
theorem
cos_C/.(z1-z2) = (cos_C/.z1)*(cos_C/.z2) + (sin_C/.z1)*(sin_C/.z2)
proof
cos_C/.(z1-z2) = cos_C/.(z1+-z2)
.=cos_C/.z1*cos_C/.(-z2) - sin_C/.z1*sin_C/.(-z2) by Th6
.=cos_C/.z1*cos_C/.z2 - sin_C/.z1*sin_C/.(-z2) by Th3
.=cos_C/.z1*cos_C/.z2 - sin_C/.z1*(-sin_C/.z2) by Th2
.=cos_C/.z1*cos_C/.z2 - -sin_C/.z1*sin_C/.z2;
hence thesis;
end;
registration
let p be Function of COMPLEX,COMPLEX, i be Complex;
identify p/.i with p.i;
correctness;
end;
theorem Th8:
(cosh_C/.z)*(cosh_C/.z) - (sinh_C/.z)*(sinh_C/.z) = 1
proof
set e1 = exp(z), e2 = exp(-z);
(cosh_C/.z)*(cosh_C/.z) - (sinh_C/.z)*(sinh_C/.z)
=(cosh_C/.z)*(cosh_C/.z) - ((e1-e2)/2)*(sinh_C/.z) by Def3
.=(cosh_C/.z)*(cosh_C/.z) - ((e1-e2)/2)*((e1-e2)/2) by Def3
.=((e1+e2)/2)*(cosh_C/.z) - (((e1-e2)*(e1-e2))/(2*2)) by Def4
.=((e1+e2)/2)*((e1+e2)/2) - (((e1-e2)*(e1-e2))/(2*2)) by Def4
.=(e1*e2 + e1*e2 + (e1*e2 + e1*e2))/(2*2)
.=(1 + e1*e2 + (e1*e2 + e1*e2))/(2*2) by Lm3
.=(1 + 1 + (e1*e2 + e1*e2))/(2*2) by Lm3
.=(1 + 1 + (1 + e1*e2))/(2*2) by Lm3
.=(2+2)/(2*2) by Lm3
.= 1;
hence thesis;
end;
theorem Th9:
-sinh_C/.z = sinh_C/.(-z)
proof
sinh_C/.(-z) = (exp(-z) - exp(-(-z)))/2 by Def3
.= -(exp(z) - exp(-z))/2;
hence thesis by Def3;
end;
theorem Th10:
cosh_C/.z = cosh_C/.(-z)
proof
cosh_C/.(-z) = (exp(-z) + exp(-(-z)))/2 by Def4
.= (exp(-z) + exp(z))/2;
hence thesis by Def4;
end;
theorem Th11:
sinh_C/.(z1+z2) = (sinh_C/.z1)*(cosh_C/.z2) + (cosh_C/.z1)*( sinh_C/.z2)
proof
set e1=exp(z1), e2=exp(-z1), e3=exp(z2), e4=exp(-z2);
(sinh_C/.z1)*(cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2) =((e1-e2)/2)*(
cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2) by Def3
.=((e1-e2)/2)*(cosh_C/.z2) + (cosh_C/.z1)*((e3-e4)/2) by Def3
.=((e1-e2)/2)*(cosh_C/.z2) + ((e1+e2)/2)*((e3-e4)/2) by Def4
.=((e1-e2)/2)*((e3+e4)/2) + ((e1+e2)/2)*((e3-e4)/2) by Def4
.=(e1*e3+e1*e3-(e2*e4+e2*e4))/4
.=(Re(e1*e3)+Re(e1*e3)+(Im(e1*e3)+Im(e1*e3))***-(e2*e4 + e2*e4)) /4 by
COMPLEX1:81
.=((2*Re(e1*e3)+2*Im(e1*e3)***)-(e2*e4 + e2*e4)) /4
.=((Re(2*(e1*e3))+2*Im(e1*e3)***)-(e2*e4 + e2*e4)) /4 by COMSEQ_3:17
.=((Re(2*(e1*e3))+Im(2*(e1*e3))***)-(e2*e4 + e2*e4)) /4 by COMSEQ_3:17
.=(2*(e1*e3)-(e2*e4 + e2*e4))/4 by COMPLEX1:13
.=(2*(e1*e3)-(Re(e2*e4)+Re(e2*e4)+(Im(e2*e4)+Im(e2*e4))***)) /4 by
COMPLEX1:81
.=(2*(e1*e3)-(2*Re(e2*e4)+2*Im(e2*e4)***)) /4
.=(2*(e1*e3)-(Re(2*(e2*e4))+2*Im(e2*e4)***)) /4 by COMSEQ_3:17
.=(2*(e1*e3)-(Re(2*(e2*e4))+Im(2*(e2*e4))***)) /4 by COMSEQ_3:17
.=(2*(e1*e3)-2*(e2*e4))/4 by COMPLEX1:13
.=(e1*e3)/(2)-(2*(e2*e4))/(2*2)
.=exp(z1+z2)/2-(e2*e4)/(2) by SIN_COS:23
.=exp(z1+z2)/2-exp(-z1+-z2)/2 by SIN_COS:23
.=(exp(z1+z2)-exp(-(z1+z2)))/2;
hence thesis by Def3;
end;
theorem Th12:
sinh_C/.(z1-z2) = (sinh_C/.z1)*(cosh_C/.z2) - (cosh_C/.z1)*( sinh_C/.z2)
proof
sinh_C/.(z1-z2) = sinh_C/.(z1+ -z2)
.= (sinh_C/.z1)*cosh_C/.(-z2) + (cosh_C/.z1)*sinh_C/.(-z2) by Th11
.= (sinh_C/.z1)*cosh_C/.z2 + (cosh_C/.z1)*sinh_C/.(-z2) by Th10
.= (sinh_C/.z1)*cosh_C/.z2 + (cosh_C/.z1)*(-sinh_C/.z2) by Th9
.= (sinh_C/.z1)*cosh_C/.z2 + -(cosh_C/.z1)*(sinh_C/.z2);
hence thesis;
end;
theorem Th13:
cosh_C/.(z1-z2) = (cosh_C/.z1)*(cosh_C/.z2) - (sinh_C/.z1)*( sinh_C/.z2)
proof
set e1=exp(z1), e2=exp(-z1), e3=exp(z2), e4=exp(-z2);
(cosh_C/.z1)*(cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2) =((e1+e2)/2)*(
cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2) by Def4
.=((e1+e2)/2)*((e3+e4)/2) - (sinh_C/.z1)*(sinh_C/.z2) by Def4
.=((e1+e2)*(e3+e4))/(2*2) - ((e1-e2)/2)*(sinh_C/.z2) by Def3
.=((e1+e2)*(e3+e4))/(2*2)-((e1-e2)/2)*((e3-e4)/2) by Def3
.=(e2*e3+e2*e3+(e1*e4+e2*e4+(e1*e4-e2*e4)))/(2*2)
.=(Re(e2*e3)+Re(e2*e3)+(Im(e2*e3)+Im(e2*e3))***+(e1*e4+e1*e4)) /(2*2)
by COMPLEX1:81
.=((2*Re(e2*e3)+2*Im(e2*e3)***)+(e1*e4+e1*e4))/(2*2)
.=((Re(2*(e2*e3))+2*Im(e2*e3)***)+(e1*e4+e1*e4)) /(2*2) by COMSEQ_3:17
.=((Re(2*(e2*e3))+Im(2*(e2*e3))***)+(e1*e4+e1*e4)) /(2*2) by COMSEQ_3:17
.=(2*(e2*e3)+(e1*e4+e1*e4))/(2*2) by COMPLEX1:13
.=(2*(e2*e3)+(Re(e1*e4)+Re(e1*e4)+(Im(e1*e4)+Im(e1*e4))***)) /(2*2) by
COMPLEX1:81
.=(2*(e2*e3)+(2*Re(e1*e4)+2*Im(e1*e4)***)) /(2*2)
.=(2*(e2*e3)+(Re(2*(e1*e4))+2*Im(e1*e4)***)) /(2*2) by COMSEQ_3:17
.=(2*(e2*e3)+(Re(2*(e1*e4))+Im(2*(e1*e4))***)) /(2*2) by COMSEQ_3:17
.=(2*(e2*e3)+2*(e1*e4))/(2*2) by COMPLEX1:13
.=(e1*e4)/(2)+(2*(e2*e3))/(2*2)
.=exp(z1+-z2)/2+(e2*e3)/2 by SIN_COS:23
.=exp(z1-z2)/2+exp(-z1+z2)/2 by SIN_COS:23
.=(exp(z1-z2)+exp(-(z1-z2)))/2;
hence thesis by Def4;
end;
theorem Th14:
cosh_C/.(z1+z2) = (cosh_C/.z1)*(cosh_C/.z2) + (sinh_C/.z1)*( sinh_C/.z2)
proof
cosh_C/.(z1+z2) = cosh_C/.(z1- -z2)
.=(cosh_C/.z1)*cosh_C/.(-z2) - (sinh_C/.z1)*sinh_C/.(-z2) by Th13
.=(cosh_C/.z1)*cosh_C/.(z2) - (sinh_C/.z1)*sinh_C/.(-z2) by Th10
.=(cosh_C/.z1)*cosh_C/.(z2) - (sinh_C/.z1)*(-sinh_C/.z2) by Th9
.=(cosh_C/.z1)*cosh_C/.(z2) - -(sinh_C/.z1)*(sinh_C/.z2);
hence thesis;
end;
theorem Th15:
for z being Complex holds sin_C/.(***z) = ***sinh_C/.z
proof
let z be Complex;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
sin_C/.(***z) = (exp(******z) - exp(-***(***z)))/(***2) by Def1
.= ***((exp(z) - exp(-z))/2);
then sin_C/.(***z) = ***sinh_C/.z by Def3;
hence thesis;
end;
theorem Th16:
for z being Complex holds cos_C/.(***z) = cosh_C/.z
proof
let z be Complex;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
cos_C/.(***z) = (exp(******z)+exp(-***(***z)))/2 by Def2
.= (exp(-z)+exp(z))/2;
then cos_C/.(***z) = cosh_C/.z by Def4;
hence thesis;
end;
theorem Th17:
for z being Complex holds sinh_C/.(***z) = ***sin_C/.z
proof
let z be Complex;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
sinh_C/.(***z) = (exp(***z)-exp(-***z))/2 by Def3
.= ***((exp(***z)-exp(-***z))/(***2));
then sinh_C/.(***z) = ***sin_C/.z by Def1;
hence thesis;
end;
theorem Th18:
for z being Complex holds cosh_C/.(***z) = cos_C/.z
proof
let z be Complex;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
cosh_C/.(***z) = (exp(***z) + exp(-***z))/2 by Def4;
then cosh_C/.(***z) = cos_C/.z by Def2;
hence thesis;
end;
Lm4: exp(x+y***)=exp_R(x)*(cos(y)+sin(y)***)
proof
exp(x+y***) =exp(x)*exp(y***) by SIN_COS:23
.= exp_R(x)*exp(y***) by SIN_COS:49
.= exp_R(x)*(cos y+(sin y)***) by SIN_COS:25;
hence thesis;
end;
theorem Th19:
for x,y holds exp(x+y***) = (exp_R.x)*(
cos.y)+(exp_R.x)*(sin.y)***
proof
let x,y;
exp(x+y***)=exp_R(x)*(cos(y)+sin(y)***) by Lm4
.= exp_R(x)*cos(y)-0*sin(y) + (exp_R(x)*sin(y)+cos(y)*0)***
.=exp_R(x)*cos.y+exp_R(x)*sin(y)*** by SIN_COS:def 19
.=exp_R.x*cos.y+exp_R(x)*sin(y)*** by SIN_COS:def 23
.=exp_R.x*cos.y+exp_R.x*sin(y)*** by SIN_COS:def 23;
hence thesis by SIN_COS:def 17;
end;
theorem
exp(0c) = 1 by SIN_COS:49,51;
theorem Th21:
sin_C/.0c = 0
proof
sin_C/.0c = (exp(0c)-exp(-***0c))/(***2) by Def1
.=0c/(***2);
hence thesis;
end;
theorem
sinh_C/.0c = 0
proof
sinh_C/.0c = (exp(0c)-exp(-0c))/2 by Def3
.=0c/2;
hence thesis;
end;
theorem Th23:
cos_C/.0c = 1
proof
cos_C/.0c = (exp(0c)+exp(-***0c))/2 by Def2
.= 1 by SIN_COS:49,51;
hence thesis;
end;
theorem
cosh_C/.0c = 1
proof
cosh_C/.0c = (exp 0c + exp(-0c))/2 by Def4
.=1 by SIN_COS:49,51;
hence thesis;
end;
theorem
exp(z) = cosh_C/.z + sinh_C/.z
proof
cosh_C/.z + sinh_C/.z = (exp(z)+exp(-z))/2 + sinh_C/.z by Def4
.= (exp(z)+exp(-z))/2 + (exp(z)-exp(-z))/2 by Def3
.= (exp(z)+(exp(-z) + exp(z)-exp(-z)))/2
.=(Re(exp(z))+Re(exp(z))+(Im(exp(z))+Im(exp(z)))***)/2 by COMPLEX1:81
.=((2*Re(exp(z))+2*Im(exp(z))***))/2
.=((Re(2*exp(z))+2*Im(exp(z))***))/2 by COMSEQ_3:17
.=((Re(2*exp(z))+Im(2*exp(z))***))/2 by COMSEQ_3:17
.=(2*exp(z))/2 by COMPLEX1:13
.=exp(z)*1;
hence thesis;
end;
theorem
exp(-z) = cosh_C/.z - sinh_C/.z
proof
cosh_C/.z - sinh_C/.z = (exp(z)+exp(-z))/2 - sinh_C/.z by Def4
.= (exp(z)+exp(-z))/2 - (exp(z)-exp(-z))/2 by Def3
.= (exp(-z)+exp(-z))/2
.= (Re(exp(-z))+Re(exp(-z))+(Im(exp(-z))+Im(exp(-z)))***)/2 by
COMPLEX1:81
.=((2*Re(exp(-z))+2*Im(exp(-z))***))/2
.=((Re(2*exp(-z))+2*Im(exp(-z))***))/2 by COMSEQ_3:17
.=((Re(2*exp(-z))+Im(2*exp(-z))***))/2 by COMSEQ_3:17
.=(2*exp(-z))/2 by COMPLEX1:13
.=exp(-z)*1;
hence thesis;
end;
theorem
exp(z+2*PI***) = exp(z)
proof
z+2*PI*** = (Re z+(Im z)***)+(2*PI+0***)*** by COMPLEX1:13
.= Re z + 0 + (Im z + 2*PI)***;
then
exp(z+2*PI***) =exp_R.(Re z)*cos.(Im z + 2*PI*1)+exp_R.(Re z)*sin.(Im z
+ 2*PI)*** by Th19
.=exp_R.(Re z)*cos.(Im z)+exp_R.(Re z)*sin.(Im z + 2*PI*1)*** by
SIN_COS2:11
.=exp_R.(Re z)*cos.(Im z)+exp_R.(Re z)*sin.(Im z)*** by SIN_COS2:10
.=exp(Re z+Im z***) by Th19;
hence thesis by COMPLEX1:13;
end;
theorem Th28:
exp(2*PI*n***) = 1
proof
thus exp(2*PI*n***) = cos(0+2*PI*n)+sin(0+2*PI*n)*** by SIN_COS:25
.=cos.(0+2*PI*n)+sin(0+2*PI*n)*** by SIN_COS:def 19
.=cos.(0+2*PI*n)+sin.(0+2*PI*n)*** by SIN_COS:def 17
.=cos.(0+2*PI*n)+sin.(0)*** by SIN_COS2:10
.= 1 by SIN_COS:30,SIN_COS2:11;
end;
theorem Th29:
exp((-2*PI*n)***) = 1
proof
thus exp((-2*PI*n)***) = cos(-2*PI*n)+sin(-2*PI*n)*** by SIN_COS:25
.=cos(2*PI*n)+sin(-(2*PI*n))*** by SIN_COS:31
.=cos(0+2*PI*n)+(-sin(2*PI*n))*** by SIN_COS:31
.=cos.(0+2*PI*n)+-sin(0+2*PI*n)*** by SIN_COS:def 19
.=cos.(0+2*PI*n)+-sin.(0+2*PI*n)*** by SIN_COS:def 17
.=cos.(0+2*PI*n)+-sin.(0)*** by SIN_COS2:10
.= 1 by SIN_COS:30,SIN_COS2:11;
end;
theorem
exp((2*n+1)*PI***) = -1
proof
exp((2*n+1)*PI***) = cos(PI*2*n+PI)+sin(PI*(2*n)+1*PI)*** by SIN_COS:25
.= cos.(PI*2*n+PI)+sin(PI*2*n+PI)*** by SIN_COS:def 19
.= cos.(PI*2*n+PI)+sin.(PI*2*n+PI)**