Copyright (c) 2002 Association of Mizar Users
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;
theorems COMPLEX1, REAL_1, SIN_COS, SIN_COS2, COMSEQ_3, FINSEQ_4, FUNCT_2,
COMPLFLD, HAHNBAN1, XCMPLX_0, XCMPLX_1, ARYTM_0;
schemes NAT_1, COMPLSP1, FUNCT_2;
begin :: Definitions of trigonometric functions
reserve x,y for Element of REAL;
reserve z,z1,z2 for Element of COMPLEX;
reserve n for Nat;
definition
deffunc
U(Element of COMPLEX) = (exp(<i>*$1)-(exp(-<i> * $1)))/([*2,0*] * <i>);
func sin_C -> Function of COMPLEX, COMPLEX means :Def1:
it.z = (exp(<i>*z)-(exp(-<i> * z)))/([*2,0*] * <i>);
existence
proof
thus ex f being Function of COMPLEX, COMPLEX st
for z holds f.z = U(z) from LambdaD;
end;
uniqueness
proof
thus for f1,f2 being Function of COMPLEX, COMPLEX st
(for z holds f1.z = U(z)) &
(for z holds f2.z = U(z))
holds f1 = f2 from FuncDefUniq;
end;
end;
definition
deffunc U(Element of COMPLEX) = (exp(<i>*$1) + exp(-<i>*$1))/[*2,0*];
func cos_C -> Function of COMPLEX,COMPLEX means :Def2:
it.z = (exp(<i>*z) + exp(-<i>*z))/[*2,0*];
existence
proof
thus ex f being Function of COMPLEX, COMPLEX st
for z holds f.z = U(z) from LambdaD;
end;
uniqueness
proof
thus for f1,f2 being Function of COMPLEX, COMPLEX st
(for z holds f1.z = U(z)) &
(for z holds f2.z = U(z))
holds f1 = f2 from FuncDefUniq;
end;
end;
definition
deffunc U(Element of COMPLEX) = (exp($1) - exp(-$1))/[*2,0*];
func sinh_C -> Function of COMPLEX,COMPLEX means :Def3:
it.z = (exp(z) - exp(-z))/[*2,0*];
existence
proof
thus ex f being Function of COMPLEX, COMPLEX st
for z holds f.z = U(z) from LambdaD;
end;
uniqueness
proof
thus for f1,f2 being Function of COMPLEX, COMPLEX st
(for z holds f1.z = U(z)) &
(for z holds f2.z = U(z))
holds f1 = f2 from FuncDefUniq;
end;
end;
definition
deffunc U(Element of COMPLEX) = (exp($1) + exp(-$1))/[*2,0*];
func cosh_C -> Function of COMPLEX,COMPLEX means :Def4:
it.z = (exp(z) + exp(-z))/[*2,0*];
existence
proof
thus ex f being Function of COMPLEX, COMPLEX st
for z holds f.z = U(z) from LambdaD;
end;
uniqueness
proof
thus for f1,f2 being Function of COMPLEX, COMPLEX st
(for z holds f1.z = U(z)) &
(for z holds f2.z = U(z))
holds f1 = f2 from FuncDefUniq;
end;
end;
Lm1: sin_C/.z = (exp(<i>*z)-(exp(-<i> * z)))/([*2,0*] * <i>)
proof
dom sin_C = COMPLEX by FUNCT_2:def 1;
then sin_C/.z = sin_C.z by FINSEQ_4:def 4
.= (exp(<i>*z)-(exp(-<i> * z)))/([*2,0*] * <i>) by Def1;
hence thesis;
end;
Lm2: cos_C/.z = (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
proof
dom cos_C = COMPLEX by FUNCT_2:def 1;
then cos_C/.z = cos_C.z by FINSEQ_4:def 4
.= (exp(<i>*z) + exp(-<i>*z))/[*2,0*] by Def2;
hence thesis;
end;
Lm3: sinh_C/.z = (exp(z) - exp(-z))/[*2,0*]
proof
dom sinh_C = COMPLEX by FUNCT_2:def 1;
then sinh_C/.z = sinh_C.z by FINSEQ_4:def 4
.= (exp(z) - exp(-z))/[*2,0*] by Def3;
hence thesis;
end;
Lm4: cosh_C/.z = (exp(z) + exp(-z))/[*2,0*]
proof
dom cosh_C = COMPLEX by FUNCT_2:def 1;
then cosh_C/.z = cosh_C.z by FINSEQ_4:def 4
.= (exp(z) + exp(-z))/[*2,0*] by Def4;
hence thesis;
end;
Lm5:
(z1 + z2)*(z1 + z2) = z1*z1 + z2*z2 + z1*z2 + z1*z2
proof
(z1 + z2)*(z1 + z2) = (z1 + z2)*z1 + (z1 + z2)*z2 by XCMPLX_1:8
.= z1*z1 + z1*z2 + z2*(z1 + z2) by XCMPLX_1:8
.= z1*z1 + z1*z2 + (z2*z1 + z2*z2) by XCMPLX_1:8
.= ((z2*z1 + z2*z2) + z1*z1) + z1*z2 by XCMPLX_1:1
.= z2*z1 + (z2*z2 + z1*z1) + z1*z2 by XCMPLX_1:1;
hence thesis;
end;
Lm6:
(z1 - z2)*(z1 - z2) = z1*z1 + z2*z2 - (z1*z2 + z1*z2)
proof
(z1 -z2)*(z1 - z2) = (z1 + -z2)*(z1 -z2) by XCMPLX_0:def 8
.= (z1 + -z2)*(z1 + -z2) by XCMPLX_0:def 8
.= z1*z1 + (-z2)*(-z2) +z1*(-z2) + z1*(-z2) by Lm5
.= z1*z1 + z2*z2 +z1*(-z2) + z1*(-z2) by XCMPLX_1:177
.= z1*z1 + z2*z2 + -(z1*z2) + z1*(-z2) by XCMPLX_1:175
.= z1*z1 + z2*z2 + -(z1*z2) + -(z1*z2) by XCMPLX_1:175
.= z1*z1 + z2*z2 + (-(z1*z2) + -(z1*z2)) by XCMPLX_1:1
.= z1*z1 + z2*z2 + -(z1*z2 + z1*z2) by XCMPLX_1:140;
hence thesis by XCMPLX_0:def 8;
end;
L0: 0c = [*0,0*] by ARYTM_0:def 7;
L1: 1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7;
Lm7:
[*2,0*]*<i><>0c
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
<i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
hence thesis by A1,XCMPLX_1:6;
end;
Lm8:
for z be Element of COMPLEX holds
exp(z)*exp(-z) = [*1,0*]
proof
let z be Element of COMPLEX;
exp(z)*exp(-z) = exp(z + -z) by SIN_COS:24
.= exp([*0,0*]) by L0,XCMPLX_0:def 6
.= [*exp(0),0*] by SIN_COS:54;
hence thesis by SIN_COS:56;
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) = 1r
proof
let z be Element of COMPLEX;
A1:[*4,0*] <> 0c by ARYTM_0:12,L0;
set z1 = exp(<i>*z), z2 = exp(-<i>*z);
(sin_C/.z)*(sin_C/.z) + (cos_C/.z)*(cos_C/.z)
=(sin_C/.z)*(sin_C/.z) +
(cos_C/.z)*((exp(<i>*z) + exp(-<i>*z))/[*2,0*]) by Lm2
.=(sin_C/.z)*(sin_C/.z) + ((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by Lm2
.=(z1 - z2)/([*2,0*]*<i>)*(sin_C/.z) +
((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by Lm1
.=((z1 - z2)/([*2,0*]*<i>))*((z1 - z2)/([*2,0*]*<i>)) +
((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by Lm1
.=((z1 - z2)*(z1 - z2))/(([*2,0*]*<i>)*([*2,0*]*<i>)) +
((z1 + z2)/[*2,0*])*((z1 + z2)/[*2,0*]) by XCMPLX_1:77
.=((z1 - z2)*(z1 - z2))/([*2,0*]*<i>*([*2,0*]*<i>)) +
((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by XCMPLX_1:77
.=((z1 - z2)*(z1 - z2))/(([*2,0*]*<i>)*<i>*[*2,0*]) +
((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by XCMPLX_1:4
.=((z1 - z2)*(z1 - z2))/([*2,0*]*(-1r)*[*2,0*]) +
((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
.=((z1 - z2)*(z1 - z2))/((-1r)*([*2,0*]*[*2,0*])) +
((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by XCMPLX_1:4
.=((z1 - z2)*(z1 - z2))/(-([*2,0*]*[*2,0*])) +
((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by COMPLEX1:46
.=((z1 - z2)*(z1 - z2))/(-([*2*2-0*0,2*0+2*0*])) +
((z1 + z2)*(z1 + z2))/([*2,0*]*[*2,0*]) by HAHNBAN1:2
.=((z1 - z2)*(z1 - z2))/(-[*4,0*]) +
((z1 + z2)*(z1 + z2))/([*4,0*]) by HAHNBAN1:2
.=-(((z1 - z2)*(z1 - z2))/[*4,0*]) +
((z1 + z2)*(z1 + z2))/[*4,0*] by XCMPLX_1:189
.=((z1 + z2)*(z1 + z2))/[*4,0*] -
(((z1 - z2)*(z1 - z2))/[*4,0*])by XCMPLX_0:def 8
.=((z1 + z2)*(z1 + z2) - (z1 - z2)*(z1 - z2))/[*4,0*]by XCMPLX_1:121
.=(z1*z1 + z2*z2 + z1*z2 + z1*z2 - (z1 - z2)*(z1 - z2))
/[*4,0*] by Lm5
.=(z1*z1 + z2*z2 + z1*z2 + z1*z2 - (z1*z1 + z2*z2 - (z1*z2 + z1*z2)))
/[*4,0*] by Lm6
.=(z1*z1 + z2*z2 + (z1*z2 + z1*z2) - (z1*z1 + z2*z2 - (z1*z2 + z1*z2)))
/[*4,0*] by XCMPLX_1:1
.=((z1*z2 + z1*z2) + (z1*z1 + z2*z2) - (z1*z1 + z2*z2) + (z1*z2 + z1*z2))
/[*4,0*] by XCMPLX_1:37
.=((z1*z2 + z1*z2) + (z1*z2 + z1*z2))/[*4,0*] by XCMPLX_1:26
.=(([*1,0*] + z1*exp(-(<i>*z))) + (z1*exp(-(<i>*z)) + z1*exp(-(<i>*z))))
/[*4,0*] by Lm8
.=(([*1,0*] + [*1,0*]) + (z1*exp(-(<i>*z)) + z1*exp(-(<i>*z))))
/[*4,0*] by Lm8
.=(([*1,0*] + [*1,0*]) + (z1*exp(-(<i>*z)) + [*1,0*]))/[*4,0*] by Lm8
.=(([*1,0*] + [*1,0*]) + ([*1,0*] + [*1,0*]))/[*4,0*] by Lm8
.=([*1+1,0+0*] + ([*1,0*] + [*1,0*]))/[*4,0*] by COMPLFLD:2
.=([*2,0*] + [*2,0*])/[*4,0*] by COMPLFLD:2
.=[*2+2,0+0*]/[*4,0*] by COMPLFLD:2;
hence thesis by A1,COMPLEX1:86;
end;
theorem Th2:
-sin_C/.z = sin_C/.(-z)
proof
sin_C/.(-z) = (exp(<i>*(-z)) - exp(-<i>*(-z)))/([*2,0*]*<i>) by Lm1
.= (exp(<i>*(-z)) - exp((-<i>)*(-z)))/([*2,0*]*<i>) by XCMPLX_1:175
.= (exp(<i>*(-z)) - exp(<i>*z))/([*2,0*]*<i>) by XCMPLX_1:177
.= (exp(-<i>*z) - exp(<i>*z))/([*2,0*]*<i>) by XCMPLX_1:175
.= (-(exp(<i>*z) - exp(-<i>*z)))/([*2,0*]*<i>) by XCMPLX_1:143
.= -((exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by XCMPLX_1:188;
hence thesis by Lm1;
end;
theorem Th3:
cos_C/.z = cos_C/.(-z)
proof
cos_C/.(-z) = (exp(<i>*(-z)) + exp(-<i>*(-z)))/[*2,0*] by Lm2
.=(exp(<i>*(-z)) + exp((-<i>)*(-z)))/[*2,0*] by XCMPLX_1:175
.=(exp(<i>*(-z)) + exp(<i>*z))/[*2,0*] by XCMPLX_1:177
.=(exp(-<i>*z) + exp(<i>*z))/[*2,0*] by XCMPLX_1:175;
hence thesis by Lm2;
end;
theorem Th4:
sin_C/.(z1+z2) = (sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
set e1 = exp(<i>*z1), e2 = exp(-<i>*z1), e3 = exp(<i>*z2), e4 = exp(-<i>*z2);
(sin_C/.z1)*(cos_C/.z2) + (cos_C/.z1)*(sin_C/.z2)
=((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*(cos_C/.z2) +
(cos_C/.z1)*(sin_C/.z2) by Lm1
.=((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*(cos_C/.z2) +
(cos_C/.z1)*((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm1
.=((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*
((exp(-<i>*z2) + exp(<i>*z2))/[*2,0*]) +
(cos_C/.z1)*((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm2
.=((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*
((exp(-<i>*z2) + exp(<i>*z2))/[*2,0*]) +
((exp(-<i>*z1) + exp(<i>*z1))/[*2,0*])*
((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm2
.=((exp(<i>*z1) - exp(-<i>*z1))*(exp(-<i>*z2) + exp(<i>*z2)))
/([*2,0*]*<i>*[*2,0*]) + ((exp(-<i>*z1) + exp(<i>*z1))/[*2,0*])*
((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by XCMPLX_1:77
.=((exp(<i>*z1) - exp(-<i>*z1))*(exp(-<i>*z2) + exp(<i>*z2)))
/([*2,0*]*<i>*[*2,0*]) +
((exp(-<i>*z1) + exp(<i>*z1))*(exp(<i>*z2) - exp(-<i>*z2)))
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:77
.=( (exp(<i>*z1) - exp(-<i>*z1))*(exp(-<i>*z2) + exp(<i>*z2)) +
(exp(-<i>*z1) + exp(<i>*z1))*(exp(<i>*z2) - exp(-<i>*z2)) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:63
.=( (e1-e2)*e4 + (e1-e2)*e3 + (e1+e2)*(e3-e4) )/([*2,0*]*<i>*[*2,0*])
by XCMPLX_1:8
.=( e1*e4-e2*e4 + (e1-e2)*e3 + (e1+e2)*(e3-e4) )/([*2,0*]*<i>*[*2,0*])
by XCMPLX_1:40
.=( e1*e4-e2*e4 + (e1*e3-e2*e3) + (e1+e2)*(e3-e4) )/([*2,0*]*<i>*[*2,0*])
by XCMPLX_1:40
.=( e1*e4-e2*e4 + (e1*e3-e2*e3) + ((e1+e2)*e3-(e1+e2)*e4) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:40
.=( e1*e4-e2*e4 + (e1*e3-e2*e3) + (e1*e3+e2*e3-(e1+e2)*e4) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:8
.=( e1*e4-e2*e4 + (e1*e3-e2*e3) + (e2*e3+e1*e3-(e1*e4+e2*e4)) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:8
.=( e1*e4-e2*e4 + ((e1*e3-e2*e3) + (e2*e3+e1*e3-(e1*e4+e2*e4))) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:1
.=( e1*e4-e2*e4 + ((e1*e3-e2*e3 + (e2*e3+e1*e3))-(e1*e4+e2*e4)) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:29
.=( e1*e4-e2*e4 + ((e1*e3-e2*e3 + e2*e3)+e1*e3-(e1*e4+e2*e4)) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:1
.=(e1*e4-e2*e4 + (e1*e3+e1*e3-(e1*e4+e2*e4)))/([*2,0*]*<i>*[*2,0*])
by XCMPLX_1:27
.=( e1*e3+e1*e3-(e1*e4+e2*e4 - (e1*e4-e2*e4)) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:37
.=( e1*e3+e1*e3-(e1*e4+(e2*e4 - (e1*e4-e2*e4))) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:29
.=( e1*e3+e1*e3-(e1*e4+(e2*e4 - e1*e4 + e2*e4)) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:37
.=( e1*e3+e1*e3-((e1*e4+(e2*e4 - e1*e4)) + e2*e4) )
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:1
.=(e1*e3+e1*e3-((e1*e4+e2*e4 - e1*e4) + e2*e4))/([*2,0*]*<i>*[*2,0*])
by XCMPLX_1:29
.=(e1*e3+e1*e3-(e2*e4 + e2*e4))/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:26
.=([*Re(e1*e3)+Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*<i>*[*2,0*]) by COMPLEX1:def 9
.=([*2*Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
.=([*2*Re(e1*e3),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
.=([*Re([*2,0*]*(e1*e3)),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
.=([*Re([*2,0*]*(e1*e3)),Im([*2,0*]*(e1*e3))*]-(e2*e4 + e2*e4))
/([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)-(e2*e4 + e2*e4))/([*2,0*]*<i>*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e1*e3)-[*Re(e2*e4)+Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
/([*2,0*]*<i>*[*2,0*]) by COMPLEX1:def 9
.=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),2*Im(e2*e4)*])
/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),2*Im(e2*e4)*])
/([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),Im([*2,0*]*(e2*e4))*])
/([*2,0*]*<i>*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)-[*2,0*]*(e2*e4))/([*2,0*]*<i>*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e1*e3))/([*2,0*]*<i>*[*2,0*])
-([*2,0*]*(e2*e4))/([*2,0*]*<i>*[*2,0*]) by XCMPLX_1:121
.=(e1*e3)/([*2,0*]*<i>)
-([*2,0*]*(e2*e4))/([*2,0*]*<i>*[*2,0*]) by A1,XCMPLX_1:92
.=(e1*e3)/([*2,0*]*<i>)-(e2*e4)/([*2,0*]*<i>) by A1,XCMPLX_1:92
.=exp(<i>*z1+<i>*z2)/([*2,0*]*<i>)-(e2*e4)/([*2,0*]*<i>) by SIN_COS:24
.=exp(<i>*(z1+z2))/([*2,0*]*<i>)-(e2*e4)/([*2,0*]*<i>) by XCMPLX_1:8
.=exp(<i>*(z1+z2))/([*2,0*]*<i>)-exp(-<i>*z1+-<i>*z2)/([*2,0*]*<i>)
by SIN_COS:24
.=( exp(<i>*(z1+z2))-exp(-<i>*z1+ -<i>*z2) )/([*2,0*]*<i>) by XCMPLX_1:121
.=( exp(<i>*(z1+z2))-exp(-(<i>*z1+<i>*z2)) )/([*2,0*]*<i>) by XCMPLX_1:140
.=( exp(<i>*(z1+z2))-exp(-<i>*(z1+z2)) )/([*2,0*]*<i>) by XCMPLX_1:8;
hence thesis by Lm1;
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) by XCMPLX_0:def 8
.=(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) by XCMPLX_1:175;
hence thesis by XCMPLX_0:def 8;
end;
theorem Th6:
cos_C/.(z1+z2) = (cos_C/.z1)*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
set e1 = exp(<i>*z1), e2 = exp(-<i>*z1), e3 = exp(<i>*z2), e4 = exp(-<i>*z2);
(cos_C/.z1)*(cos_C/.z2) - (sin_C/.z1)*(sin_C/.z2)
=(cos_C/.z1)*(cos_C/.z2) -
((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))*(sin_C/.z2) by Lm1
.=(cos_C/.z1)*(cos_C/.z2) - ((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))
*((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm1
.=(cos_C/.z1)*((exp(<i>*z2) + exp(-<i>*z2))/[*2,0*]) -
((exp(<i>*z1) - exp(-<i>*z1))/([*2,0*]*<i>))
*((exp(<i>*z2) - exp(-<i>*z2))/([*2,0*]*<i>)) by Lm2
.=((e1 + e2)/[*2,0*])*((e3 + e4)/[*2,0*]) -
((e1 - e2)/([*2,0*]*<i>))*((e3 - e4)/([*2,0*]*<i>)) by Lm2
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
((e1 - e2)/([*2,0*]*<i>))*((e3 - e4)/([*2,0*]*<i>)) by XCMPLX_1:77
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
((e1 - e2)*(e3 - e4))/([*2,0*]*<i>*([*2,0*]*<i>)) by XCMPLX_1:77
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
((e1 - e2)*(e3 - e4))/(([*2,0*]*<i>*<i>)*[*2,0*]) by XCMPLX_1:4
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
((e1 - e2)*(e3 - e4))/([*2,0*]*(-1r)*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
((e1 - e2)*(e3 - e4))/((-1r)*([*2,0*]*[*2,0*])) by XCMPLX_1:4
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
((e1 - e2)*(e3 - e4))/(-([*2,0*]*[*2,0*])) by COMPLEX1:46
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) -
- ((e1 - e2)*(e3 - e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:189
.=((e1 + e2)*(e3 + e4))/([*2,0*]*[*2,0*]) +
((e1 - e2)*(e3 - e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:151
.=((e1+e2)*(e3+e4) + (e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
.=((e1+e2)*e3+(e1+e2)*e4 + (e1-e2)*(e3-e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=(e1*e3+e2*e3 + (e1+e2)*e4 + (e1-e2)*(e3-e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=(e1*e3+e2*e3 + (e1*e4+e2*e4) + (e1-e2)*(e3-e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=(e1*e3+e2*e3 + (e1*e4+e2*e4) + ((e1-e2)*e3-(e1-e2)*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e3+e2*e3 + (e1*e4+e2*e4) + (e1*e3-e2*e3-(e1-e2)*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e3-e2*e3-(e1*e4-e2*e4) + ((e1*e3+e2*e3) + (e1*e4+e2*e4)) )
/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=( (e1*e3+e2*e3)+( e1*e3-e2*e3-(e1*e4-e2*e4) ) + (e1*e4+e2*e4) )
/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=( (e1*e3-e2*e3 + (e2*e3+e1*e3) )-(e1*e4-e2*e4) + (e1*e4+e2*e4) )
/([*2,0*]*[*2,0*]) by XCMPLX_1:29
.=( (e1*e3-e2*e3 + e2*e3)+e1*e3 -(e1*e4-e2*e4) + (e1*e4+e2*e4) )
/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=(e1*e3+e1*e3-(e1*e4-e2*e4) + (e1*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:27
.=( e1*e3+e1*e3 -(e1*e4-e2*e4 - (e1*e4+e2*e4)) )
/([*2,0*]*[*2,0*]) by XCMPLX_1:37
.=( e1*e3+e1*e3 -(e1*e4-e2*e4 - e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:36
.=( e1*e3+e1*e3 -(-e2*e4+e1*e4- e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:
def 8
.=( e1*e3+e1*e3 -(-e2*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
.=( e1*e3+e1*e3 -(-e2*e4)+e2*e4)/([*2,0*]*[*2,0*]) by XCMPLX_1:37
.=( e1*e3+e1*e3 +e2*e4+e2*e4)/([*2,0*]*[*2,0*]) by XCMPLX_1:151
.=( e1*e3+e1*e3 + (e2*e4+e2*e4) )/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=([*Re(e1*e3)+Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]+(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by COMPLEX1:def 9
.=([*2*Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]+(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2*Re(e1*e3),2*Im(e1*e3)*]+(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*Re([*2,0*]*(e1*e3)),2*Im(e1*e3)*]+(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*Re([*2,0*]*(e1*e3)),Im([*2,0*]*(e1*e3))*]+(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)+(e2*e4 + e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e1*e3)+[*Re(e2*e4)+Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by COMPLEX1:def 9
.=([*2,0*]*(e1*e3)+[*2*Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e1*e3)+[*2*Re(e2*e4),2*Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e1*e3)+[*Re([*2,0*]*(e2*e4)),2*Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)+[*Re([*2,0*]*(e2*e4)),Im([*2,0*]*(e2*e4))*])
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)+[*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e1*e3))/([*2,0*]*[*2,0*])
+([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
.=(e1*e3)/([*2,0*])+([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by A1,XCMPLX_1:92
.=(e1*e3)/([*2,0*])+(e2*e4)/([*2,0*]) by A1,XCMPLX_1:92
.=exp(<i>*z1+<i>*z2)/([*2,0*])+(e2*e4)/([*2,0*]) by SIN_COS:24
.=exp(<i>*(z1+z2))/([*2,0*])+(e2*e4)/([*2,0*]) by XCMPLX_1:8
.=exp(<i>*(z1+z2))/([*2,0*])+exp(-<i>*z1+-<i>*z2)/([*2,0*]) by SIN_COS:24
.=( exp(<i>*(z1+z2))+exp(-<i>*z1+ -<i>*z2) )/([*2,0*]) by XCMPLX_1:63
.=( exp(<i>*(z1+z2))+exp(-(<i>*z1+<i>*z2)) )/([*2,0*]) by XCMPLX_1:140
.=( exp(<i>*(z1+z2))+exp(-<i>*(z1+z2)) )/([*2,0*]) by XCMPLX_1:8;
hence thesis by Lm2;
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) by XCMPLX_0:def 8
.=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 by XCMPLX_1:175;
hence thesis by XCMPLX_1:151;
end;
theorem Th8:
(cosh_C/.z)*(cosh_C/.z) - (sinh_C/.z)*(sinh_C/.z) = 1r
proof
A1:[*4,0*] <> 0c by ARYTM_0:12,L0;
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,0*])*(sinh_C/.z) by Lm3
.=(cosh_C/.z)*(cosh_C/.z) - ((e1-e2)/[*2,0*])*((e1-e2)/[*2,0*]) by Lm3
.=(cosh_C/.z)*(cosh_C/.z) - (((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
by XCMPLX_1:77
.=((e1+e2)/[*2,0*])*(cosh_C/.z) - (((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
by Lm4
.=((e1+e2)/[*2,0*])*((e1+e2)/[*2,0*]) - (((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
by Lm4
.=(((e1+e2)*(e1+e2))/([*2,0*]*[*2,0*]))-(((e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]))
by XCMPLX_1:77
.=((e1+e2)*(e1+e2)-(e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]) by XCMPLX_1:121
.=(e1*e1 + e2*e2 + e1*e2 + e1*e2-(e1-e2)*(e1-e2))/([*2,0*]*[*2,0*]) by Lm5
.=(e1*e1 + e2*e2 + e1*e2 + e1*e2-(e1*e1 + e2*e2 - (e1*e2 + e1*e2)))
/([*2,0*]*[*2,0*]) by Lm6
.=(e1*e1 + e2*e2 + (e1*e2 + e1*e2) - (e1*e1 + e2*e2 - (e1*e2 + e1*e2)))
/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=(e1*e1 + e2*e2 + (e1*e2 + e1*e2) - (e1*e1 + e2*e2) + (e1*e2 + e1*e2))
/([*2,0*]*[*2,0*]) by XCMPLX_1:37
.=(e1*e2 + e1*e2 + (e1*e2 + e1*e2))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
.=([*1,0*] + e1*e2 + (e1*e2 + e1*e2))/([*2,0*]*[*2,0*]) by Lm8
.=([*1,0*] + [*1,0*] + (e1*e2 + e1*e2))/([*2,0*]*[*2,0*]) by Lm8
.=([*1,0*] + [*1,0*] + ([*1,0*] + e1*e2))/([*2,0*]*[*2,0*]) by Lm8
.=([*1,0*] + [*1,0*] + ([*1,0*] + [*1,0*]))/([*2,0*]*[*2,0*]) by Lm8
.=([*1+1,0+0*] + ([*1,0*] + [*1,0*]))/([*2,0*]*[*2,0*]) by COMPLFLD:2
.=([*2,0*] + [*1+1,0+0*])/([*2,0*]*[*2,0*]) by COMPLFLD:2
.=[*2+2,0+0*]/([*2,0*]*[*2,0*]) by COMPLFLD:2
.=[*4,0*]/[*2*2-0*0,2*0+2*0*] by HAHNBAN1:2;
hence thesis by A1,COMPLEX1:86;
end;
theorem Th9:
-sinh_C/.z = sinh_C/.(-z)
proof
sinh_C/.(-z) = (exp(-z) - exp(-(-z)))/[*2,0*] by Lm3
.= (-(exp(z) - exp(-z)))/[*2,0*] by XCMPLX_1:143
.= -(exp(z) - exp(-z))/[*2,0*] by XCMPLX_1:188;
hence thesis by Lm3;
end;
theorem Th10:
cosh_C/.z = cosh_C/.(-z)
proof
cosh_C/.(-z) = (exp(-z) + exp(-(-z)))/[*2,0*] by Lm4
.= (exp(-z) + exp(z))/[*2,0*];
hence thesis by Lm4;
end;
theorem Th11:
sinh_C/.(z1+z2) = (sinh_C/.z1)*(cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
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,0*])*(cosh_C/.z2) + (cosh_C/.z1)*(sinh_C/.z2) by Lm3
.=((e1-e2)/[*2,0*])*(cosh_C/.z2) + (cosh_C/.z1)*((e3-e4)/[*2,0*]) by Lm3
.=((e1-e2)/[*2,0*])*(cosh_C/.z2) + ((e1+e2)/[*2,0*])*((e3-e4)/[*2,0*]) by Lm4
.=((e1-e2)/[*2,0*])*((e3+e4)/[*2,0*]) +
((e1+e2)/[*2,0*])*((e3-e4)/[*2,0*]) by Lm4
.=((e1-e2)*(e3+e4))/([*2,0*]*[*2,0*]) +
((e1+e2)/[*2,0*])*((e3-e4)/[*2,0*]) by XCMPLX_1:77
.=((e1-e2)*(e3+e4))/([*2,0*]*[*2,0*]) +
((e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:77
.=((e1-e2)*(e3+e4)+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
.=((e1-e2)*e3+(e1-e2)*e4+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=(e1*e3-e2*e3+(e1-e2)*e4+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e3-e2*e3+(e1*e4-e2*e4)+(e1+e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e3-e2*e3+(e1*e4-e2*e4)+((e1+e2)*e3-(e1+e2)*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e3-e2*e3+(e1*e4-e2*e4)+(e1*e3+e2*e3-(e1+e2)*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=((e1*e4-e2*e4)+(e1*e3-e2*e3)+(e1*e3+e2*e3-(e1*e4+e2*e4)))
/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=((e1*e4-e2*e4)+(e1*e3-e2*e3)+(e1*e3+e2*e3)-(e1*e4+e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:29
.=(((e1*e3-e2*e3)+(e1*e3+e2*e3))+(e1*e4-e2*e4)-(e1*e4+e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=(e1*e3-e2*e3+e2*e3+e1*e3+(e1*e4-e2*e4)-(e1*e4+e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=(e1*e3+e1*e3+(e1*e4-e2*e4)-(e1*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:27
.=(e1*e3+e1*e3+(e1*e4-e2*e4-(e1*e4+e2*e4)))/([*2,0*]*[*2,0*]) by XCMPLX_1:29
.=(e1*e3+e1*e3+(e1*e4-e2*e4-e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:36
.=(e1*e3+e1*e3+(-e2*e4+e1*e4-e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:def 8
.=(e1*e3+e1*e3+(-e2*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
.=(e1*e3+e1*e3+(-e2*e4+-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:def 8
.=(e1*e3+e1*e3+-(e2*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:140
.=(e1*e3+e1*e3-(e2*e4+e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_0:def 8
.=([*Re(e1*e3)+Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by COMPLEX1:def 9
.=([*2*Re(e1*e3),Im(e1*e3)+Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2*Re(e1*e3),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*Re([*2,0*]*(e1*e3)),2*Im(e1*e3)*]-(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*Re([*2,0*]*(e1*e3)),Im([*2,0*]*(e1*e3))*]-(e2*e4 + e2*e4))
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)-(e2*e4 + e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e1*e3)-[*Re(e2*e4)+Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by COMPLEX1:def 9
.=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),Im(e2*e4)+Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e1*e3)-[*2*Re(e2*e4),2*Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),2*Im(e2*e4)*])
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)-[*Re([*2,0*]*(e2*e4)),Im([*2,0*]*(e2*e4))*])
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e1*e3)-[*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e1*e3))/([*2,0*]*[*2,0*])
-([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:121
.=(e1*e3)/([*2,0*])-([*2,0*]*(e2*e4))/([*2,0*]*[*2,0*]) by A1,XCMPLX_1:92
.=(e1*e3)/([*2,0*])-(e2*e4)/([*2,0*]) by A1,XCMPLX_1:92
.=exp(z1+z2)/[*2,0*]-(e2*e4)/([*2,0*]) by SIN_COS:24
.=exp(z1+z2)/[*2,0*]-exp(-z1+-z2)/[*2,0*] by SIN_COS:24
.=(exp(z1+z2)-exp(-z1+-z2))/[*2,0*] by XCMPLX_1:121
.=(exp(z1+z2)-exp(-(z1+z2)))/[*2,0*] by XCMPLX_1:140;
hence thesis by Lm3;
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) by XCMPLX_0:def 8
.= (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) by XCMPLX_1:175;
hence thesis by XCMPLX_0:def 8;
end;
theorem Th13:
cosh_C/.(z1-z2) = (cosh_C/.z1)*(cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2)
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
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,0*])*(cosh_C/.z2) - (sinh_C/.z1)*(sinh_C/.z2) by Lm4
.=((e1+e2)/[*2,0*])*((e3+e4)/[*2,0*]) - (sinh_C/.z1)*(sinh_C/.z2) by Lm4
.=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*]) - (sinh_C/.z1)*(sinh_C/.z2)
by XCMPLX_1:77
.=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*]) - ((e1-e2)/[*2,0*])*(sinh_C/.z2) by Lm3
.=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*])-((e1-e2)/[*2,0*])*((e3-e4)/[*2,0*])
by Lm3
.=((e1+e2)*(e3+e4))/([*2,0*]*[*2,0*])-((e1-e2)*(e3-e4))/([*2,0*]*[*2,0*])
by XCMPLX_1:77
.=((e1+e2)*(e3+e4)-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:121
.=((e1+e2)*e3+(e1+e2)*e4-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=(e1*e3+e2*e3+(e1+e2)*e4-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=(e1*e3+e2*e3+(e1*e4+e2*e4)-(e1-e2)*(e3-e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:8
.=(e1*e3+e2*e3+(e1*e4+e2*e4)-((e1-e2)*e3-(e1-e2)*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e3+e2*e3+(e1*e4+e2*e4)-(e1*e3-e2*e3-(e1-e2)*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e4+e2*e4+(e2*e3+e1*e3)-(e1*e3-e2*e3-(e1*e4-e2*e4)))
/([*2,0*]*[*2,0*]) by XCMPLX_1:40
.=(e1*e4+e2*e4+(e2*e3+e1*e3)-(e1*e3-e2*e3)+(e1*e4-e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:37
.=(e1*e4+e2*e4+(e2*e3+e1*e3-(e1*e3-e2*e3))+(e1*e4-e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:29
.=(e1*e4+e2*e4+(e2*e3+e1*e3-e1*e3+e2*e3)+(e1*e4-e2*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:37
.=(e2*e3+e2*e3+(e1*e4+e2*e4)+(e1*e4-e2*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
.=(e2*e3+e2*e3+(e1*e4+e2*e4+(e1*e4-e2*e4)))/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=(e2*e3+e2*e3+(e1*e4+(e2*e4+(e1*e4-e2*e4))))/([*2,0*]*[*2,0*]) by XCMPLX_1:1
.=(e2*e3+e2*e3+(e1*e4+(e2*e4+e1*e4-e2*e4)))/([*2,0*]*[*2,0*]) by XCMPLX_1:29
.=(e2*e3+e2*e3+(e1*e4+e1*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:26
.=([*Re(e2*e3)+Re(e2*e3),Im(e2*e3)+Im(e2*e3)*]+(e1*e4+e1*e4))
/([*2,0*]*[*2,0*]) by COMPLEX1:def 9
.=([*2*Re(e2*e3),Im(e2*e3)+Im(e2*e3)*]+(e1*e4+e1*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2*Re(e2*e3),2*Im(e2*e3)*]+(e1*e4+e1*e4))
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*Re([*2,0*]*(e2*e3)),2*Im(e2*e3)*]+(e1*e4+e1*e4))
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*Re([*2,0*]*(e2*e3)),Im([*2,0*]*(e2*e3))*]+(e1*e4+e1*e4))
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e2*e3)+(e1*e4+e1*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e2*e3)+[*Re(e1*e4)+Re(e1*e4),Im(e1*e4)+Im(e1*e4)*])
/([*2,0*]*[*2,0*]) by COMPLEX1:def 9
.=([*2,0*]*(e2*e3)+[*2*Re(e1*e4),Im(e1*e4)+Im(e1*e4)*])
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e2*e3)+[*2*Re(e1*e4),2*Im(e1*e4)*])
/([*2,0*]*[*2,0*]) by XCMPLX_1:11
.=([*2,0*]*(e2*e3)+[*Re([*2,0*]*(e1*e4)),2*Im(e1*e4)*])
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e2*e3)+[*Re([*2,0*]*(e1*e4)),Im([*2,0*]*(e1*e4))*])
/([*2,0*]*[*2,0*]) by COMSEQ_3:17
.=([*2,0*]*(e2*e3)+[*2,0*]*(e1*e4))/([*2,0*]*[*2,0*]) by COMPLEX1:8
.=([*2,0*]*(e2*e3))/([*2,0*]*[*2,0*])
+([*2,0*]*(e1*e4))/([*2,0*]*[*2,0*]) by XCMPLX_1:63
.=(e1*e4)/([*2,0*])+([*2,0*]*(e2*e3))/([*2,0*]*[*2,0*]) by A1,XCMPLX_1:92
.=(e1*e4)/([*2,0*])+(e2*e3)/[*2,0*] by A1,XCMPLX_1:92
.=exp(z1+-z2)/[*2,0*]+(e2*e3)/[*2,0*] by SIN_COS:24
.=exp(z1+-z2)/[*2,0*]+exp(-z1+z2)/[*2,0*] by SIN_COS:24
.=exp(z1-z2)/[*2,0*]+exp(-z1+z2)/[*2,0*] by XCMPLX_0:def 8
.=(exp(z1-z2)+exp(-z1+z2))/[*2,0*] by XCMPLX_1:63
.=(exp(z1-z2)+exp(-(z1-z2)))/[*2,0*] by XCMPLX_1:162;
hence thesis by Lm4;
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) by XCMPLX_1:151
.=(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) by XCMPLX_1:175;
hence thesis by XCMPLX_1:151;
end;
theorem Th15:
sin_C/.(<i>*z) = <i>*sinh_C/.z
proof
A1: <i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
sin_C/.(<i>*z) = (exp(<i>*(<i>*z)) - exp(-<i>*(<i>*z)))/(<i>*[*2,0*]) by Lm1
.= (exp(<i>*<i>*z) - exp(-<i>*(<i>*z)))/(<i>*[*2,0*]) by XCMPLX_1:4
.= (exp((-1r)*z) - exp(-(<i>*<i>*z)))/(<i>*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
.= (exp(-z) - exp(-(-1r)*z))/(<i>*[*2,0*]) by COMPLEX1:37,46
.= (exp(-z) - exp(--z))/(<i>*[*2,0*]) by COMPLEX1:46
.= (<i>*(exp(-z) - exp(z)))/(<i>*(<i>*[*2,0*])) by A1,XCMPLX_1:92
.= (<i>*(exp(-z) - exp(z)))/((-1r)*[*2,0*]) by COMPLEX1:37,XCMPLX_1:4
.= (<i>*(exp(-z) - exp(z)))/(-[*2,0*]) by COMPLEX1:46
.= <i>*((exp(-z) - exp(z))/(-[*2,0*])) by XCMPLX_1:75
.= <i>*(-(exp(-z) - exp(z))/[*2,0*]) by XCMPLX_1:189
.= <i>*((-(exp(-z) - exp(z)))/[*2,0*]) by XCMPLX_1:188
.= <i>*((exp(z) - exp(-z))/[*2,0*]) by XCMPLX_1:143;
hence thesis by Lm3;
end;
theorem Th16:
cos_C/.(<i>*z) = cosh_C/.z
proof
cos_C/.(<i>*z) = (exp(<i>*(<i>*z))+exp(-<i>*(<i>*z)))/[*2,0*] by Lm2
.= (exp(<i>*<i>*z)+exp(-<i>*(<i>*z)))/[*2,0*] by XCMPLX_1:4
.= (exp((-1r)*z)+exp(-(-1r)*z))/[*2,0*] by COMPLEX1:37,XCMPLX_1:4
.= (exp(-z)+exp(-(-1r)*z))/[*2,0*] by COMPLEX1:46
.= (exp(-z)+exp(--z))/[*2,0*] by COMPLEX1:46
.= (exp(-z)+exp(z))/[*2,0*];
hence thesis by Lm4;
end;
theorem Th17:
sinh_C/.(<i>*z) = <i>*sin_C/.z
proof
A1: <i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
sinh_C/.(<i>*z) = (exp(<i>*z)-exp(-<i>*z))/[*2,0*] by Lm3
.= (<i>*(exp(<i>*z)-exp(-<i>*z)))/(<i>*[*2,0*]) by A1,XCMPLX_1:92
.= <i>*((exp(<i>*z)-exp(-<i>*z))/(<i>*[*2,0*])) by XCMPLX_1:75;
hence thesis by Lm1;
end;
theorem Th18:
cosh_C/.(<i>*z) = cos_C/.z
proof
cosh_C/.(<i>*z) = (exp(<i>*z) + exp(-<i>*z))/[*2,0*] by Lm4;
hence thesis by Lm2;
end;
Lm9:
exp([*x,y*])=[*exp(x),0*]*[*cos(y),sin(y)*]
proof
exp([*x,y*]) = exp([*x+0,0+y*])
.= exp([*x,0*]+[*0,y*]) by COMPLFLD:2
.=exp([*x,0*])*exp([*0,y*]) by SIN_COS:24
.= [*exp(x),0*]*exp([*0,y*]) by SIN_COS:54;
hence thesis by SIN_COS:28;
end;
theorem Th19:
for x,y being Element of REAL holds
exp([*x,y*]) = [*(exp.x)*(cos.y),(exp.x)*(sin.y)*]
proof
let x,y be Element of REAL;
exp([*x,y*])=[*exp(x),0*]*[*cos(y),sin(y)*] by Lm9
.=[*exp(x)*cos(y)-0*sin(y),exp(x)*sin(y)+cos(y)*0*] by HAHNBAN1:2
.=[*exp(x)*cos.y,exp(x)*sin(y)*] by SIN_COS:def 23
.=[*exp.x*cos.y,exp(x)*sin(y)*] by SIN_COS:def 27
.=[*exp.x*cos.y,exp.x*sin(y)*] by SIN_COS:def 27;
hence thesis by SIN_COS:def 21;
end;
theorem Th20:
exp(0c) = [*1,0*]
proof
thus thesis by L0,SIN_COS:54,56;
end;
theorem Th21:
sin_C/.0c = 0c
proof
sin_C/.0c = (exp(0c)-exp(-<i>*0c))/(<i>*[*2,0*]) by Lm1
.=0c/(<i>*[*2,0*]) by XCMPLX_1:14;
hence thesis;
end;
theorem
sinh_C/.0c = 0c
proof
sinh_C/.0c = (exp(0c)-exp(-0c))/[*2,0*] by Lm3
.=0c/[*2,0*] by XCMPLX_1:14;
hence thesis;
end;
theorem Th23:
cos_C/.0c = [*1,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
cos_C/.0c = (exp(0c)+exp(-<i>*0c))/[*2,0*] by Lm2
.= ([*1+1,0+0*])/[*2,0*] by Th20,COMPLFLD:2
.= 1r by A1,COMPLEX1:86;
hence thesis by L1;
end;
theorem
cosh_C/.0c = [*1,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
cosh_C/.0c = ([*1,0*]+[*1,0*])/[*2,0*] by Lm4,Th20,REAL_1:26
.=[*1+1,0+0*]/[*2,0*] by COMPLFLD:2
.=1r by A1,COMPLEX1:86;
hence thesis by L1;
end;
theorem
exp(z) = cosh_C/.z + sinh_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
cosh_C/.z + sinh_C/.z = (exp(z)+exp(-z))/[*2,0*] + sinh_C/.z by Lm4
.= (exp(z)+exp(-z))/[*2,0*] + (exp(z)-exp(-z))/[*2,0*] by Lm3
.= (exp(z)+exp(-z) + (exp(z)-exp(-z)))/[*2,0*] by XCMPLX_1:63
.= (exp(z)+(exp(-z) + (exp(z)-exp(-z))))/[*2,0*] by XCMPLX_1:1
.= (exp(z)+(exp(-z) + exp(z)-exp(-z)))/[*2,0*] by XCMPLX_1:29
.= (exp(z)+exp(z))/[*2,0*] by XCMPLX_1:26
.=[*Re(exp(z))+Re(exp(z)),Im(exp(z))+Im(exp(z))*]/[*2,0*] by COMPLEX1:def 9
.=([*2*Re(exp(z)),Im(exp(z))+Im(exp(z))*])/[*2,0*] by XCMPLX_1:11
.=([*2*Re(exp(z)),2*Im(exp(z))*])/[*2,0*] by XCMPLX_1:11
.=([*Re([*2,0*]*exp(z)),2*Im(exp(z))*])/[*2,0*] by COMSEQ_3:17
.=([*Re([*2,0*]*exp(z)),Im([*2,0*]*exp(z))*])/[*2,0*] by COMSEQ_3:17
.=([*2,0*]*exp(z))/[*2,0*] by COMPLEX1:8
.=exp(z)*([*2,0*]/[*2,0*]) by XCMPLX_1:75
.=exp(z)*1r by A1,COMPLEX1:86;
hence thesis by COMPLEX1:29;
end;
theorem
exp(-z) = cosh_C/.z - sinh_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
cosh_C/.z - sinh_C/.z = (exp(z)+exp(-z))/[*2,0*] - sinh_C/.z by Lm4
.= (exp(z)+exp(-z))/[*2,0*] - (exp(z)-exp(-z))/[*2,0*] by Lm3
.= (exp(-z)+exp(z) - (exp(z)-exp(-z)))/[*2,0*] by XCMPLX_1:121
.= (exp(-z)+(exp(z) - (exp(z)-exp(-z))))/[*2,0*] by XCMPLX_1:29
.= (exp(-z)+((exp(z) - exp(z))+exp(-z)))/[*2,0*] by XCMPLX_1:37
.= (exp(-z)+(exp(-z) + exp(z) - exp(z)))/[*2,0*] by XCMPLX_1:29
.= (exp(-z)+exp(-z))/[*2,0*] by XCMPLX_1:26
.=[*Re(exp(-z))+Re(exp(-z)),Im(exp(-z))+Im(exp(-z))*]/[*2,0*]
by COMPLEX1:def 9
.=([*2*Re(exp(-z)),Im(exp(-z))+Im(exp(-z))*])/[*2,0*] by XCMPLX_1:11
.=([*2*Re(exp(-z)),2*Im(exp(-z))*])/[*2,0*] by XCMPLX_1:11
.=([*Re([*2,0*]*exp(-z)),2*Im(exp(-z))*])/[*2,0*] by COMSEQ_3:17
.=([*Re([*2,0*]*exp(-z)),Im([*2,0*]*exp(-z))*])/[*2,0*] by COMSEQ_3:17
.=([*2,0*]*exp(-z))/[*2,0*] by COMPLEX1:8
.=exp(-z)*([*2,0*]/[*2,0*]) by XCMPLX_1:75
.=exp(-z)*1r by A1,COMPLEX1:86;
hence thesis by COMPLEX1:29;
end;
Lm10:
for x being Element of REAL holds
[*0,x*] = [*x,0*]*<i>
proof
let x be Element of REAL;
[*x,0*]*<i> = [*x*0-0*1,x*1+0*0*] by COMPLEX1:def 8,HAHNBAN1:2;
hence thesis;
end;
theorem
exp(z+[*2*PI,0*]*<i>) = exp(z) &
exp(z+[*0,2*PI*]) = exp(z)
proof
exp(z+[*2*PI,0*]*<i>) = exp(z)
proof
exp(z+[*2*PI,0*]*<i>)
=exp([*Re z,Im z*]+[*2*PI,0*]*[*0,1*]) by COMPLEX1:8,def 8
.=exp([*Re z,Im z*]+[*2*PI*0-0*1,2*PI*1+0*0*]) by HAHNBAN1:2
.=exp([*Re z + 0,Im z + 2*PI*]) by COMPLFLD:2
.=[*exp.(Re z)*cos.(Im z + 2*PI*1),exp.(Re z)*sin.(Im z + 2*PI)*] by Th19
.=[*exp.(Re z)*cos.(Im z),exp.(Re z)*sin.(Im z + 2*PI*1)*] by SIN_COS2:11
.=[*exp.(Re z)*cos.(Im z),exp.(Re z)*sin.(Im z)*] by SIN_COS2:10
.=exp([*Re z,Im z*]) by Th19;
hence thesis by COMPLEX1:8;
end;
hence thesis by Lm10;
end;
theorem Th28:
exp([*0,2*PI*n*]) = [*1,0*] & exp([*2*PI*n,0*]*<i>) = [*1,0*]
proof
exp([*0,2*PI*n*]) = [*1,0*]
proof
exp([*0,2*PI*n*]) = [*cos(0+2*PI*n),sin(0+2*PI*n)*] by SIN_COS:28
.=[*cos.(0+2*PI*n),sin(0+2*PI*n)*] by SIN_COS:def 23
.=[*cos.(0+2*PI*n),sin.(0+2*PI*n)*] by SIN_COS:def 21
.=[*cos.(0+2*PI*n),sin.(0)*] by SIN_COS2:10
.=[*1,sin.(0)*] by SIN_COS:33,SIN_COS2:11;
hence thesis by SIN_COS:33;
end;
hence thesis by Lm10;
end;
theorem Th29:
exp([*0,-2*PI*n*]) = [*1,0*] & exp([*-2*PI*n,0*]*<i>) = [*1,0*]
proof
exp([*0,-2*PI*n*]) = [*1,0*]
proof
exp([*0,-2*PI*n*]) = [*cos(-2*PI*n),sin(-2*PI*n)*] by SIN_COS:28
.=[*cos(2*PI*n),sin(-2*PI*n)*] by SIN_COS:34
.=[*cos(0+2*PI*n),-sin(0+2*PI*n)*] by SIN_COS:34
.=[*cos.(0+2*PI*n),-sin(0+2*PI*n)*] by SIN_COS:def 23
.=[*cos.(0+2*PI*n),-sin.(0+2*PI*n)*] by SIN_COS:def 21
.=[*cos.(0+2*PI*n),-sin.(0)*] by SIN_COS2:10
.=[*1,-sin.(0)*] by SIN_COS:33,SIN_COS2:11;
hence thesis by SIN_COS:33;
end;
hence thesis by Lm10;
end;
theorem
exp([*0,(2*n+1)*PI*]) = [*-1,0*] & exp([*(2*n+1)*PI,0*]*<i>) = [*-1,0*]
proof
exp([*0,(2*n+1)*PI*]) = [*-1,0*]
proof
exp([*0,(2*n+1)*PI*]) = [*cos((2*n+1)*PI),sin((2*n+1)*PI)*] by SIN_COS:28
.= [*cos(PI*(2*n)+1*PI),sin((2*n+1)*PI)*] by XCMPLX_1:8
.= [*cos(PI*(2*n)+1*PI),sin(PI*(2*n)+1*PI)*] by XCMPLX_1:8
.= [*cos(PI*2*n+PI),sin(PI*(2*n)+1*PI)*] by XCMPLX_1:4
.= [*cos(PI*2*n+PI),sin(PI*2*n+PI)*] by XCMPLX_1:4
.= [*cos.(PI*2*n+PI),sin(PI*2*n+PI)*] by SIN_COS:def 23
.= [*cos.(PI*2*n+PI),sin.(PI*2*n+PI)*] by SIN_COS:def 21
.= [*cos.(PI),sin.(PI*2*n+PI)*] by SIN_COS2:11
.= [*-1,sin.(PI)*] by SIN_COS:81,SIN_COS2:10;
hence thesis by SIN_COS:81;
end;
hence thesis by Lm10;
end;
theorem
exp([*0,-(2*n+1)*PI*]) = [*-1,0*] & exp([*-(2*n+1)*PI,0*]*<i>) = [*-1,0*]
proof
exp([*0,-(2*n+1)*PI*]) = [*-1,0*]
proof
exp([*0,-(2*n+1)*PI*])
= [*cos(-(2*n+1)*PI),sin(-(2*n+1)*PI)*] by SIN_COS:28
.= [*cos((2*n+1)*PI),sin(-(2*n+1)*PI)*] by SIN_COS:34
.= [*cos((2*n+1)*PI),-sin((2*n+1)*PI)*] by SIN_COS:34
.= [*cos(PI*(2*n)+1*PI),-sin((2*n+1)*PI)*] by XCMPLX_1:8
.= [*cos(PI*(2*n)+1*PI),-sin(PI*(2*n)+1*PI)*] by XCMPLX_1:8
.= [*cos(PI*2*n+PI),-sin(PI*(2*n)+1*PI)*] by XCMPLX_1:4
.= [*cos(PI*2*n+PI),-sin(PI*2*n+PI)*] by XCMPLX_1:4
.= [*cos.(PI*2*n+PI),-sin(PI*2*n+PI)*] by SIN_COS:def 23
.= [*cos.(PI*2*n+PI),-sin.(PI*2*n+PI)*] by SIN_COS:def 21
.= [*cos.(PI),-sin.(PI*2*n+PI)*] by SIN_COS2:11
.= [*-1,-sin.(PI)*] by SIN_COS:81,SIN_COS2:10;
hence thesis by SIN_COS:81;
end;
hence thesis by Lm10;
end;
theorem
exp([*0,(2*n + 1/2)*PI*]) = [*0,1*] & exp([*(2*n + 1/2)*PI,0*]*<i>) = [*0,1*]
proof
exp([*0,(2*n + 1/2)*PI*]) = [*0,1*]
proof
exp([*0,(2*n+1/2)*PI*])
= [*cos((2*n+1/2)*PI),sin((2*n+1/2)*PI)*] by SIN_COS:28
.= [*cos(PI*(2*n)+1/2*PI),sin((2*n+1/2)*PI)*] by XCMPLX_1:8
.= [*cos(PI*(2*n)+1/2*PI),sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:8
.= [*cos(PI*2*n+1/2*PI),sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:4
.= [*cos(PI*2*n+1/2*PI),sin(PI*2*n+1/2*PI)*] by XCMPLX_1:4
.= [*cos.(PI*2*n+1/2*PI),sin(PI*2*n+1/2*PI)*] by SIN_COS:def 23
.= [*cos.(PI*2*n+1/2*PI),sin.(PI*2*n+1/2*PI)*] by SIN_COS:def 21
.= [*cos.(1/2*PI),sin.(PI*2*n+1/2*PI)*] by SIN_COS2:11
.= [*cos.(1/2*PI),sin.(1/2*PI)*] by SIN_COS2:10
.= [*cos.((1*PI)/2),sin.(1/2*PI)*] by XCMPLX_1:75
.= [*0,sin.(PI/2)*] by SIN_COS:81,XCMPLX_1:75;
hence thesis by SIN_COS:81;
end;
hence thesis by Lm10;
end;
theorem
exp([*0,-(2*n + 1/2)*PI*]) = [*0,-1*] &
exp([*-(2*n + 1/2)*PI,0*]*<i>) = [*0,-1*]
proof
exp([*0,-(2*n + 1/2)*PI*]) = [*0,-1*]
proof
exp([*0,-(2*n+1/2)*PI*])
= [*cos(-(2*n+1/2)*PI),sin(-(2*n+1/2)*PI)*] by SIN_COS:28
.= [*cos((2*n+1/2)*PI),sin(-(2*n+1/2)*PI)*] by SIN_COS:34
.= [*cos((2*n+1/2)*PI),-sin((2*n+1/2)*PI)*] by SIN_COS:34
.= [*cos(PI*(2*n)+1/2*PI),-sin((2*n+1/2)*PI)*] by XCMPLX_1:8
.= [*cos(PI*(2*n)+1/2*PI),-sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:8
.= [*cos(PI*2*n+1/2*PI),-sin(PI*(2*n)+1/2*PI)*] by XCMPLX_1:4
.= [*cos(PI*2*n+1/2*PI),-sin(PI*2*n+1/2*PI)*] by XCMPLX_1:4
.= [*cos.(PI*2*n+1/2*PI),-sin(PI*2*n+1/2*PI)*] by SIN_COS:def 23
.= [*cos.(PI*2*n+1/2*PI),-sin.(PI*2*n+1/2*PI)*] by SIN_COS:def 21
.= [*cos.(1/2*PI),-sin.(PI*2*n+1/2*PI)*] by SIN_COS2:11
.= [*cos.(1/2*PI),-sin.(1/2*PI)*] by SIN_COS2:10
.= [*cos.((1*PI)/2),-sin.(1/2*PI)*] by XCMPLX_1:75
.= [*0,-sin.(PI/2)*] by SIN_COS:81,XCMPLX_1:75;
hence thesis by SIN_COS:81;
end;
hence thesis by Lm10;
end;
Lm11:
for a,b being Element of REAL holds
-[*a,b*] = [*-a,-b*]
proof
let a,b be Element of REAL;
-[*a,b*] = (-1r)*[*a,b*] by COMPLEX1:46
.= [*0*0-1*1,0*1+1*0*]*[*a,b*] by COMPLEX1:37,def 8,HAHNBAN1:2
.= [*(-1)*a-0*b,(-1)*b+0*a*] by HAHNBAN1:2
.= [*-a,(-1)*b*] by XCMPLX_1:180;
hence thesis by XCMPLX_1:180;
end;
theorem
sin_C/.(z + [*2*n*PI,0*]) = sin_C/.z
proof
sin_C/.(z + [*2*n*PI,0*])
= (exp(<i>*(z + [*2*n*PI,0*])) - exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]*<i>) by Lm1
.= (exp(<i>*z + <i>*[*2*n*PI,0*]) - exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]*<i>) by XCMPLX_1:8
.= (exp(<i>*z)*exp(<i>*[*2*n*PI,0*]) - exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]*<i>) by SIN_COS:24
.= (exp(<i>*z)*exp(<i>*[*2*PI*n,0*]) - exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]*<i>) by XCMPLX_1:4
.= (exp(<i>*z)*[*1,0*] - exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]*<i>) by Th28
.= (exp(<i>*z)*[*1,0*] - exp(-(<i>*z + <i>*[*2*n*PI,0*])))
/([*2,0*]*<i>) by XCMPLX_1:8
.= (exp(<i>*z)*[*1,0*] - exp(-<i>*z + -<i>*[*2*n*PI,0*]))
/([*2,0*]*<i>) by XCMPLX_1:140
.= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(-<i>*[*2*n*PI,0*]))
/([*2,0*]*<i>) by SIN_COS:24
.= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(-<i>*[*2*PI*n,0*]))
/([*2,0*]*<i>) by XCMPLX_1:4
.= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(<i>*(-[*2*PI*n,0*])))
/([*2,0*]*<i>) by XCMPLX_1:175
.= (exp(<i>*z)*[*1,0*] - exp(-<i>*z) * exp(<i>*[*-2*PI*n,-0*]))
/([*2,0*]*<i>) by Lm11
.= (exp(<i>*z)*1r - exp(-<i>*z)*1r)/([*2,0*]*<i>) by Th29,L1
.= (exp(<i>*z)*1r - exp(-<i>*z))/([*2,0*]*<i>) by COMPLEX1:29
.= (exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>) by COMPLEX1:29;
hence thesis by Lm1;
end;
theorem
cos_C/.(z + [*2*n*PI,0*]) = cos_C/.z
proof
cos_C/.(z + [*2*n*PI,0*])
= (exp(<i>*(z + [*2*n*PI,0*])) + exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]) by Lm2
.= (exp(<i>*z + <i>*[*2*n*PI,0*]) + exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]) by XCMPLX_1:8
.= (exp(<i>*z)*exp(<i>*[*2*n*PI,0*]) + exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]) by SIN_COS:24
.= (exp(<i>*z)*exp(<i>*[*2*PI*n,0*]) + exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]) by XCMPLX_1:4
.= (exp(<i>*z)*[*1,0*] + exp(-<i>*(z + [*2*n*PI,0*])))
/([*2,0*]) by Th28
.= (exp(<i>*z)*[*1,0*] + exp(-(<i>*z + <i>*[*2*n*PI,0*])))
/([*2,0*]) by XCMPLX_1:8
.= (exp(<i>*z)*[*1,0*] + exp(-<i>*z + -<i>*[*2*n*PI,0*]))
/([*2,0*]) by XCMPLX_1:140
.= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(-<i>*[*2*n*PI,0*]))
/([*2,0*]) by SIN_COS:24
.= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(-<i>*[*2*PI*n,0*]))
/([*2,0*]) by XCMPLX_1:4
.= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(<i>*(-[*2*PI*n,0*])))
/([*2,0*]) by XCMPLX_1:175
.= (exp(<i>*z)*[*1,0*] + exp(-<i>*z) * exp(<i>*[*-2*PI*n,-0*]))
/([*2,0*]) by Lm11
.= (exp(<i>*z)*1r + exp(-<i>*z)*1r)/([*2,0*]) by Th29,L1
.= (exp(<i>*z)*1r + exp(-<i>*z))/([*2,0*]) by COMPLEX1:29
.= (exp(<i>*z) + exp(-<i>*z))/([*2,0*]) by COMPLEX1:29;
hence thesis by Lm2;
end;
theorem Th36:
exp(<i>*z) = cos_C/.z + <i>*sin_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:<i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
cos_C/.z + <i>*sin_C/.z
= (exp(<i>*z) + exp(-<i>*z))/([*2,0*]) + <i>*sin_C/.z by Lm2
.= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
+ <i>*((exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by Lm1
.= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
+ (<i>*(exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by XCMPLX_1:75
.= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
+ (exp(<i>*z) - exp(-<i>*z))/[*2,0*] by A2,XCMPLX_1:92
.= (exp(<i>*z) + exp(-<i>*z) + (exp(<i>*z) - exp(-<i>*z)))/[*2,0*]
by XCMPLX_1:63
.= (exp(<i>*z) + (exp(-<i>*z) +(exp(<i>*z) - exp(-<i>*z))))/[*2,0*]
by XCMPLX_1:1
.= (exp(<i>*z) + (exp(-<i>*z) +exp(<i>*z) - exp(-<i>*z)))/[*2,0*]
by XCMPLX_1:29
.= (exp(<i>*z) + exp(<i>*z))/[*2,0*] by XCMPLX_1:26
.= [*Re exp(<i>*z) + Re exp(<i>*z),Im exp(<i>*z) + Im exp(<i>*z)*]/[*2,0*]
by COMPLEX1:def 9
.= [*2*Re exp(<i>*z),Im exp(<i>*z) + Im exp(<i>*z)*]/[*2,0*] by XCMPLX_1:11
.= [*2*Re exp(<i>*z),2*Im exp(<i>*z)*]/[*2,0*] by XCMPLX_1:11
.= [*Re([*2,0*]*exp(<i>*z)),2*Im exp(<i>*z)*]/[*2,0*] by COMSEQ_3:17
.= [*Re([*2,0*]*exp(<i>*z)),Im([*2,0*]*exp(<i>*z))*]/[*2,0*] by COMSEQ_3:17
.= ([*2,0*]*exp(<i>*z))/[*2,0*] by COMPLEX1:8;
hence thesis by A1,XCMPLX_1:90;
end;
theorem Th37:
exp(-<i>*z) = cos_C/.z - <i>*sin_C/.z
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:<i> <> 0c by ARYTM_0:12,COMPLEX1:def 8,L0;
cos_C/.z - <i>*sin_C/.z
= (exp(<i>*z) + exp(-<i>*z))/([*2,0*]) - <i>*sin_C/.z by Lm2
.= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
- <i>*((exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by Lm1
.= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
- (<i>*(exp(<i>*z) - exp(-<i>*z))/([*2,0*]*<i>)) by XCMPLX_1:75
.= (exp(<i>*z) + exp(-<i>*z))/[*2,0*]
- (exp(<i>*z) - exp(-<i>*z))/[*2,0*] by A2,XCMPLX_1:92
.= (exp(<i>*z) + exp(-<i>*z) - (exp(<i>*z) - exp(-<i>*z)))/[*2,0*]
by XCMPLX_1:121
.= (exp(-<i>*z) + (exp(<i>*z) - (exp(<i>*z) - exp(-<i>*z))))/[*2,0*]
by XCMPLX_1:29
.= (exp(-<i>*z) + (exp(<i>*z) - exp(<i>*z) + exp(-<i>*z)))/[*2,0*]
by XCMPLX_1:37
.= (exp(-<i>*z) + (exp(-<i>*z) + exp(<i>*z) - exp(<i>*z)))/[*2,0*]
by XCMPLX_1:29
.= (exp(-<i>*z) + exp(-<i>*z))/[*2,0*] by XCMPLX_1:26
.= [*Re exp(-<i>*z) + Re exp(-<i>*z),Im exp(-<i>*z) + Im exp(-<i>*z)*]/[*2,0*]
by COMPLEX1:def 9
.= [*2*Re exp(-<i>*z),Im exp(-<i>*z) + Im exp(-<i>*z)*]/[*2,0*]
by XCMPLX_1:11
.= [*2*Re exp(-<i>*z),2*Im exp(-<i>*z)*]/[*2,0*]
by XCMPLX_1:11
.= [*Re([*2,0*]*exp(-<i>*z)),2*Im exp(-<i>*z)*]/[*2,0*]
by COMSEQ_3:17
.= [*Re([*2,0*]*exp(-<i>*z)),Im([*2,0*]*exp(-<i>*z))*]/[*2,0*]
by COMSEQ_3:17
.= ([*2,0*]*exp(-<i>*z))/[*2,0*] by COMPLEX1:8;
hence thesis by A1,XCMPLX_1:90;
end;
Lm12:
for x,y being Element of REAL holds
<i>*[*x,y*] = [*-y,x*]
proof
let x,y be Element of REAL;
<i>*[*x,y*] = [*0*x-1*y,0*y+1*x*] by COMPLEX1:def 8,HAHNBAN1:2
.= [*0-1*y,1*x*];
hence thesis by XCMPLX_1:150;
end;
theorem Th38:
for x being Element of REAL holds
sin_C/.[*x,0*] = [*sin.x,0*]
proof
let x be Element of REAL;
A1:[*sin.x,0*]*[*0,2*] = [*sin.x*0-0*2,sin.x*2+0*0*] by HAHNBAN1:2
.= [*0,2*sin.x*];
A2:[*0,2*] <> 0c
proof
[*2,0*]*<i> = [*-0,2*] by Lm12
.= [*0,2*];
hence thesis by Lm7;
end;
sin_C/.[*x,0*] = (exp(<i>*[*x,0*]) - exp(-<i>*[*x,0*]))/([*2,0*]*<i>) by Lm1
.= (exp([*-0,x*]) - exp(-<i>*[*x,0*]))/([*2,0*]*<i>) by Lm12
.= (exp([*0,x*]) - exp(-[*0,x*]))/([*2,0*]*<i>) by Lm12
.= (exp([*0,x*]) - exp([*-0,-x*]))/([*2,0*]*<i>) by Lm11
.= (exp([*0,x*]) - exp([*0,-x*]))/[*0,2*] by Lm12
.= ([*exp.0*cos.x,exp.0*sin.x*] - exp([*0,-x*]))/[*0,2*] by Th19
.= ([*exp(0)*cos.x,exp.0*sin.x*] - exp([*0,-x*]))/[*0,2*] by SIN_COS:def 27
.= ([*cos.x,1*sin.x*] - exp([*0,-x*]))/[*0,2*] by SIN_COS:56,def 27
.= ([*cos.x,1*sin.x*] - [*exp.0*cos.-x,exp.0*sin.-x*])/[*0,2*] by Th19
.= ([*cos.x,1*sin.x*] - [*exp(0)*cos.-x,exp.0*sin.-x*])/[*0,2*]
by SIN_COS:def 27
.= ([*cos.x,sin.x*] - [*cos.-x,1*sin.-x*])/[*0,2*]
by SIN_COS:56,def 27
.= ([*cos.x,sin.x*] - [*cos.x,sin.-x*])/[*0,2*]
by SIN_COS:33
.= ([*cos.x,sin.x*] - [*cos.x,-sin.x*])/[*0,2*] by SIN_COS:33
.= ([*cos.x,sin.x*] + - [*cos.x,-sin.x*])/[*0,2*] by XCMPLX_0:def 8
.= ([*cos.x,sin.x*] + [*-cos.x,--sin.x*])/[*0,2*] by Lm11
.= [*cos.x+-cos.x,sin.x+sin.x*]/[*0,2*] by COMPLFLD:2
.= [*cos.x-cos.x,sin.x + sin.x*]/[*0,2*] by XCMPLX_0:def 8
.= [*0,sin.x + sin.x*]/[*0,2*] by XCMPLX_1:14
.= ([*sin.x,0*]*[*0,2*])/[*0,2*] by A1,XCMPLX_1:11
.= [*sin.x,0*] by A2,XCMPLX_1:90;
hence thesis;
end;
theorem Th39:
for x being Element of REAL holds
cos_C/.[*x,0*] = [*cos.x,0*]
proof
let x be Element of REAL;
A1:[*2*cos.x,0*] = [*cos.x,0*]*[*2,0*]
proof
[*cos.x,0*]*[*2,0*] = [*cos.x*2-0*0,cos.x*0+0*2*] by HAHNBAN1:2
.=[*2*cos.x,0*];
hence thesis;
end;
A2:[*2,0*] <> 0c by ARYTM_0:12,L0;
cos_C/.[*x,0*] = (exp(<i>*[*x,0*]) + exp(-<i>*[*x,0*]))/[*2,0*] by Lm2
.= (exp([*-0,x*]) + exp(-<i>*[*x,0*]))/[*2,0*] by Lm12
.= (exp([*0,x*]) + exp(-[*0,x*]))/[*2,0*] by Lm12
.= (exp([*0,x*]) + exp([*-0,-x*]))/[*2,0*] by Lm11
.= ([*exp.0*cos.x,exp.0*sin.x*] + exp([*0,-x*]))/[*2,0*] by Th19
.= ([*exp(0)*cos.x,exp.0*sin.x*] + exp([*0,-x*]))/[*2,0*] by SIN_COS:def 27
.= ([*cos.x,1*sin.x*] + exp([*0,-x*]))/[*2,0*] by SIN_COS:56,def 27
.= ([*cos.x,1*sin.x*] + [*exp.0*cos.-x,exp.0*sin.-x*])/[*2,0*] by Th19
.= ([*cos.x,1*sin.x*] + [*exp(0)*cos.-x,exp.0*sin.-x*])/[*2,0*]
by SIN_COS:def 27
.= ([*cos.x,1*sin.x*] + [*exp(0)*cos.-x,exp(0)*sin.-x*])/[*2,0*]
by SIN_COS:def 27
.= ([*cos.x,sin.x*] + [*cos.x,sin.-x*])/[*2,0*] by SIN_COS:33,56
.= ([*cos.x,sin.x*] + [*cos.x,-sin.x*])/[*2,0*] by SIN_COS:33
.= [*cos.x+cos.x,sin.x+-sin.x*]/[*2,0*] by COMPLFLD:2
.= [*cos.x+cos.x,sin.x-sin.x*]/[*2,0*] by XCMPLX_0:def 8
.= [*cos.x+cos.x,0*]/[*2,0*] by XCMPLX_1:14
.=([*cos.x,0*]*[*2,0*])/[*2,0*] by A1,XCMPLX_1:11
.= [*cos.x,0*] by A2,XCMPLX_1:90;
hence thesis;
end;
theorem Th40:
for x being Element of REAL holds
sinh_C/.[*x,0*] = [*sinh.x,0*]
proof
let x be Element of REAL;
A1:[*exp.x-exp.(-x),0*] = [*sinh.x,0*]*[*2,0*]
proof
[*sinh.x,0*]*[*2,0*] = [*sinh.x*2-0*0,sinh.x*0+0*2*] by HAHNBAN1:2
.=[*2*((exp.x - exp.(-x))/2),0*] by SIN_COS2:def 1
.=[*(exp.x - exp.(-x))/(2/2),0*] by XCMPLX_1:82;
hence thesis;
end;
A2:[*2,0*] <> 0c by ARYTM_0:12,L0;
sinh_C/.[*x,0*] = (exp([*x,0*])-exp(-[*x,0*]))/[*2,0*] by Lm3
.= ([*exp.x*cos.0,exp.x*sin.0*] - exp(-[*x,0*]))/[*2,0*] by Th19
.= ([*exp.x,0*] - exp([*-x,-0*]))/[*2,0*] by Lm11,SIN_COS:33
.= ([*exp.x,0*] - [*exp.(-x)*cos.0,exp.(-x)*sin.0*])/[*2,0*] by Th19
.= ([*exp.x,0*] +- [*exp.(-x),0*])/[*2,0*] by SIN_COS:33,XCMPLX_0:def 8
.= ([*exp.x,0*] + [*-exp.(-x),-0*])/[*2,0*] by Lm11
.= ([*exp.x+-exp.(-x),0+0*])/[*2,0*] by COMPLFLD:2
.= ([*sinh.x,0*]*[*2,0*])/[*2,0*] by A1,XCMPLX_0:def 8;
hence thesis by A2,XCMPLX_1:90;
end;
theorem Th41:
for x being Element of REAL holds
cosh_C/.[*x,0*] = [*cosh.x,0*]
proof
let x be Element of REAL;
A1:[*exp.x+exp.(-x),0*] = [*cosh.x,0*]*[*2,0*]
proof
[*cosh.x,0*]*[*2,0*] = [*cosh.x*2-0*0,cosh.x*0+0*2*] by HAHNBAN1:2
.=[*2*((exp.(x) + exp.(-x))/2),0*] by SIN_COS2:def 3
.=[*(exp.(x) + exp.(-x))/(2/2),0*] by XCMPLX_1:82;
hence thesis;
end;
A2:[*2,0*] <> 0c by ARYTM_0:12,L0;
cosh_C/.[*x,0*] = (exp([*x,0*])+exp(-[*x,0*]))/[*2,0*] by Lm4
.= ([*exp.x*cos.0,exp.x*sin.0*] + exp(-[*x,0*]))/[*2,0*] by Th19
.= ([*exp.x,0*] + exp([*-x,-0*]))/[*2,0*] by Lm11,SIN_COS:33
.= ([*exp.x,0*] + [*exp.(-x)*cos.0,exp.(-x)*sin.0*])/[*2,0*] by Th19
.= ([*exp.x+exp.(-x),0+0*])/[*2,0*] by COMPLFLD:2,SIN_COS:33
.= ([*cosh.x,0*]*[*2,0*])/[*2,0*] by A1;
hence thesis by A2,XCMPLX_1:90;
end;
theorem
for x,y being Element of REAL holds
[*x,y*] = [*x,0*] + <i>*[*y,0*]
proof
let x,y being Element of REAL;
[*x,0*] + <i>*[*y,0*] = [*x,0*] + [*-0,y*] by Lm12
.= [*x+0,0+y*] by COMPLFLD:2;
hence thesis;
end;
theorem Th43:
sin_C/.[*x,y*] = [*sin.x*cosh.y,cos.x*sinh.y*]
proof
sin_C/.[*x,y*] = sin_C/.[*x+0,0+y*]
.= sin_C/.([*x,0*]+[*0,y*]) by COMPLFLD:2
.= sin_C/.[*x,0*]*cos_C/.[*0,y*] + cos_C/.[*x,0*]*sin_C/.[*0,y*] by Th4
.= sin_C/.[*x,0*]*cos_C/.(<i>*[*y,0*]) + cos_C/.[*x,0*]*sin_C/.[*0,y*]
by Lm10
.= sin_C/.[*x,0*]*cos_C/.(<i>*[*y,0*]) + cos_C/.[*x,0*]*sin_C/.(<i>*[*y,0*])
by Lm10
.= sin_C/.[*x,0*]*cosh_C/.[*y,0*] + cos_C/.[*x,0*]*sin_C/.(<i>*[*y,0*])
by Th16
.= sin_C/.[*x,0*]*cosh_C/.[*y,0*] + cos_C/.[*x,0*]*(<i>*sinh_C/.[*y,0*])
by Th15
.= [*sin.x,0*]*cosh_C/.[*y,0*] + cos_C/.[*x,0*]*(<i>*sinh_C/.[*y,0*]) by Th38
.= [*sin.x,0*]*cosh_C/.[*y,0*] + [*cos.x,0*]*(<i>*sinh_C/.[*y,0*]) by Th39
.= [*sin.x,0*]*cosh_C/.[*y,0*] + [*cos.x,0*]*(<i>*[*sinh.y,0*]) by Th40
.= [*sin.x,0*]*[*cosh.y,0*] + [*cos.x,0*]*(<i>*[*sinh.y,0*]) by Th41
.= [*sin.x*cosh.y-0*0,sin.x*0+0*cosh.y*] + [*cos.x,0*]*(<i>*[*sinh.y,0*])
by HAHNBAN1:2
.= [*sin.x*cosh.y,0*] + [*cos.x,0*]*[*sinh.y,0*]*<i> by XCMPLX_1:4
.= [*sin.x*cosh.y,0*] + [*cos.x*sinh.y-0*0,cos.x*0+0*sinh.y*]*<i> by HAHNBAN1:
2
.= [*sin.x*cosh.y,0*] + [*0,cos.x*sinh.y*] by Lm10
.= [*sin.x*cosh.y+0,0+cos.x*sinh.y*] by COMPLFLD:2;
hence thesis;
end;
theorem Th44:
sin_C/.[*x,-y*] = [*sin.x*cosh.y,-cos.x*sinh.y*]
proof
sin_C/.[*x,-y*] = [*sin.x*cosh.-y,cos.x*sinh.-y*] by Th43
.= [*sin.x*cosh.y,cos.x*sinh.-y*] by SIN_COS2:19
.= [*sin.x*cosh.y,cos.x*-sinh.y*] by SIN_COS2:19;
hence thesis by XCMPLX_1:175;
end;
theorem Th45:
cos_C/.[*x,y*] = [*cos.x*cosh.y,-sin.x*sinh.y*]
proof
cos_C/.[*x,y*]= cos_C/.[*x+0,0+y*]
.= cos_C/.([*x,0*]+[*0,y*]) by COMPLFLD:2
.= cos_C/.[*x,0*]*cos_C/.[*0,y*]-sin_C/.[*x,0*]*sin_C/.[*0,y*] by Th6
.= cos_C/.[*x,0*]*cos_C/.(<i>*[*y,0*])-sin_C/.[*x,0*]*sin_C/.[*0,y*] by Lm10
.= cos_C/.[*x,0*]*cos_C/.(<i>*[*y,0*])-sin_C/.[*x,0*]*sin_C/.(<i>*[*y,0*])
by Lm10
.= cos_C/.[*x,0*]*cos_C/.(<i>*[*y,0*])-sin_C/.[*x,0*]*(sinh_C/.[*y,0*]*<i>)
by Th15
.= cos_C/.[*x,0*]*cosh_C/.[*y,0*]-sin_C/.[*x,0*]*(sinh_C/.[*y,0*]*<i>)
by Th16
.= cos_C/.[*x,0*]*cosh_C/.[*y,0*]-[*sin.x,0*]*(sinh_C/.[*y,0*]*<i>) by Th38
.= [*cos.x,0*]*cosh_C/.[*y,0*]-[*sin.x,0*]*(sinh_C/.[*y,0*]*<i>) by Th39
.= [*cos.x,0*]*cosh_C/.[*y,0*]-[*sin.x,0*]*([*sinh.y,0*]*<i>) by Th40
.= [*cos.x,0*]*[*cosh.y,0*]-[*sin.x,0*]*([*sinh.y,0*]*<i>) by Th41
.= [*cos.x,0*]*[*cosh.y,0*]-[*sin.x,0*]*[*sinh.y,0*]*<i> by XCMPLX_1:4
.= [*cos.x*cosh.y-0*0,cos.x*0+0*cosh.y*]-[*sin.x,0*]*[*sinh.y,0*]*<i> by
HAHNBAN1:2
.= [*cos.x*cosh.y,0*]-[*sin.x*sinh.y-0*0,sin.x*0+0*sinh.y-0*]*<i> by HAHNBAN1:
2
.= [*cos.x*cosh.y,0*]+-[*sin.x*sinh.y,0*]*<i> by XCMPLX_0:def 8
.= [*cos.x*cosh.y,0*]+-[*-0,sin.x*sinh.y*] by Lm12
.= [*cos.x*cosh.y,0*]+[*-0,-sin.x*sinh.y*] by Lm11
.= [*cos.x*cosh.y+-0,0+-sin.x*sinh.y*] by COMPLFLD:2;
hence thesis;
end;
theorem Th46:
cos_C/.[*x,-y*] = [*cos.x*cosh.y,sin.x*sinh.y*]
proof
cos_C/.[*x,-y*] = [*cos.x*cosh.-y,-sin.x*sinh.-y*] by Th45
.= [*cos.x*cosh.y,-sin.x*sinh.-y*] by SIN_COS2:19
.= [*cos.x*cosh.y,-sin.x*-sinh.y*] by SIN_COS2:19
.= [*cos.x*cosh.y,--sin.x*sinh.y*] by XCMPLX_1:175;
hence thesis;
end;
theorem Th47:
sinh_C/.[*x,y*] = [*sinh.x*cos.y,cosh.x*sin.y*]
proof
sinh_C/.[*x,y*] = sinh_C/.[*--x,y*]
.= sinh_C/.([*y,-x*]*<i>) by Lm12
.= <i>*sin_C/.[*y,-x*] by Th17
.= <i>*[*sin.y*cosh.x,-cos.y*sinh.x*] by Th44
.= [*--sinh.x*cos.y,cosh.x*sin.y*] by Lm12;
hence thesis;
end;
theorem Th48:
sinh_C/.[*x,-y*] = [*sinh.x*cos.y,-cosh.x*sin.y*]
proof
sinh_C/.[*x,-y*] = [*sinh.x*cos.-y,cosh.x*sin.-y*] by Th47
.= [*sinh.x*cos.y,cosh.x*sin.-y*] by SIN_COS:33
.= [*sinh.x*cos.y,cosh.x*-sin.y*] by SIN_COS:33;
hence thesis by XCMPLX_1:175;
end;
theorem Th49:
cosh_C/.[*x,y*] = [*cosh.x*cos.y,sinh.x*sin.y*]
proof
cosh_C/.[*x,y*] = cosh_C/.[*--x,y*]
.=cosh_C/.([*y,-x*]*<i>) by Lm12
.=cos_C/.[*y,-x*] by Th18;
hence thesis by Th46;
end;
theorem Th50:
cosh_C/.[*x,-y*] = [*cosh.x*cos.y,-sinh.x*sin.y*]
proof
cosh_C/.[*x,-y*] = [*cosh.x*cos.-y,sinh.x*sin.-y*] by Th49
.=[*cosh.x*cos.y,sinh.x*sin.-y*] by SIN_COS:33
.=[*cosh.x*cos.y,sinh.x*-sin.y*] by SIN_COS:33;
hence thesis by XCMPLX_1:175;
end;
theorem Th51:
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)
proof
defpred X[Nat] means for z being Element of COMPLEX holds
(cos_C/.z + <i>*sin_C/.z) #N ($1)
= cos_C/.([*$1,0*]*z) + <i>*sin_C/.([*$1,0*]*z);
A1: X[0] by Th21,Th23,L0,L1,COMSEQ_3:11;
A2:for n st X[n] holds X[n+1]
proof
let n be Nat such that
A3:for 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);
for z being Element of COMPLEX holds (cos_C/.z + <i>*sin_C/.z) #N (n+1)
= cos_C/.([*n+1,0*]*z) + <i>*sin_C/.([*n+1,0*]*z)
proof
let z being Element of COMPLEX;
set cn = cos_C/.([*n,0*]*z), sn = sin_C/.([*n,0*]*z),
c1 = cos_C/.z , s1 = sin_C/.z;
A4: (cos_C/.z + <i>*sin_C/.z) #N (n+1)
= (cos_C/.z + <i>*sin_C/.z) GeoSeq.(n+1) by COMSEQ_3:def 2
.= (cos_C/.z + <i>*sin_C/.z) GeoSeq.n * (cos_C/.z + <i>*sin_C/.z)
by COMSEQ_3:def 1
.= (cos_C/.z + <i>*sin_C/.z) #N n * (cos_C/.z + <i>*sin_C/.z)
by COMSEQ_3:def 2
.= (cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z)) * (cos_C/.z + <i>*sin_C/.z)
by A3
.= (cn + <i>*sn)*c1 + (cn + <i>*sn)*(<i>*s1) by XCMPLX_1:8
.= cn*c1 + <i>*sn*c1 + (cn + <i>*sn)*(<i>*s1) by XCMPLX_1:8
.= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + <i>*sn*(<i>*s1)) by XCMPLX_1:8
.= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + (<i>*sn*<i>)*s1) by XCMPLX_1:4
.= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + (-1r)*sn*s1) by COMPLEX1:37,XCMPLX_1:4
.= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + (-1r)*(sn*s1)) by XCMPLX_1:4
.= cn*c1 + <i>*sn*c1 + (cn*(<i>*s1) + -sn*s1) by COMPLEX1:46
.= cn*c1 + <i>*sn*c1 + (<i>*cn*s1 + -sn*s1) by XCMPLX_1:4;
cos_C/.([*n+1,0*]*z) + <i>*sin_C/.([*n+1,0*]*z)
= cos_C/.(([*n,0*] +[*1,0*])*z) + <i>*sin_C/.([*n+1,0+0*]*z) by COMPLFLD:2
.= cos_C/.(([*n,0*] +[*1,0*])*z) + <i>*sin_C/.(([*n,0*]+[*1,0*])*z) by
COMPLFLD:2
.= cos_C/.([*n,0*]*z +[*1,0*]*z) + <i>*sin_C/.(([*n,0*]+[*1,0*])*z)
by XCMPLX_1:8
.= cos_C/.([*n,0*]*z +[*1,0*]*z) + <i>*sin_C/.([*n,0*]*z+[*1,0*]*z)
by XCMPLX_1:8
.= cos_C/.([*n,0*]*z +[*1,0*]*z) +
<i>*(sin_C/.([*n,0*]*z)*cos_C/.([*1,0*]*z)
+ cos_C/.([*n,0*]*z)*sin_C/.([*1,0*]*z)) by Th4
.= cos_C/.([*n,0*]*z)*cos_C/.([*1,0*]*z)
- sin_C/.([*n,0*]*z)*sin_C/.([*1,0*]*z)
+ <i>*(sin_C/.([*n,0*]*z)*cos_C/.([*1,0*]*z)
+ cos_C/.([*n,0*]*z)*sin_C/.([*1,0*]*z)) by Th6
.= cos_C/.([*n,0*]*z)*cos_C/.z
- sin_C/.([*n,0*]*z)*sin_C/.(1r*z)
+ <i>*(sin_C/.([*n,0*]*z)*cos_C/.(1r*z)
+ cos_C/.([*n,0*]*z)*sin_C/.(1r*z)) by COMPLEX1:29,L1
.= cos_C/.([*n,0*]*z)*cos_C/.z
- sin_C/.([*n,0*]*z)*sin_C/.z
+ <i>*(sin_C/.([*n,0*]*z)*cos_C/.(1r*z)
+ cos_C/.([*n,0*]*z)*sin_C/.(1r*z)) by COMPLEX1:29
.= cos_C/.([*n,0*]*z)*cos_C/.z
- sin_C/.([*n,0*]*z)*sin_C/.z
+ <i>*(sin_C/.([*n,0*]*z)*cos_C/.z
+ cos_C/.([*n,0*]*z)*sin_C/.(1r*z)) by COMPLEX1:29
.= cos_C/.([*n,0*]*z)*cos_C/.z
- sin_C/.([*n,0*]*z)*sin_C/.z
+ <i>*(sin_C/.([*n,0*]*z)*cos_C/.z
+ cos_C/.([*n,0*]*z)*sin_C/.z) by COMPLEX1:29
.= cn*c1 - sn*s1 + (<i>*(sn*c1) + <i>*(cn*s1)) by XCMPLX_1:8
.= cn*c1 +- sn*s1 + (<i>*(sn*c1) + <i>*(cn*s1)) by XCMPLX_0:def 8
.= cn*c1 +- sn*s1 + (<i>*(sn*c1) + <i>*cn*s1) by XCMPLX_1:4
.= cn*c1 +- sn*s1 + (<i>*sn*c1 + <i>*cn*s1) by XCMPLX_1:4
.= cn*c1 +( (<i>*sn*c1 + <i>*cn*s1) + -sn*s1 ) by XCMPLX_1:1
.= cn*c1 +( <i>*sn*c1 + (<i>*cn*s1 + -sn*s1) ) by XCMPLX_1:1;
hence thesis by A4,XCMPLX_1:1;
end;
hence thesis;
end;
for n holds X[n] from Ind(A1,A2);
hence thesis;
end;
theorem Th52:
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)
proof
let n be Nat;
let z be Element of COMPLEX;
(cos_C/.z - <i>*sin_C/.z) #N n
=(cos_C/.z + -<i>*sin_C/.z) #N n by XCMPLX_0:def 8
.=(cos_C/.z + <i>*-sin_C/.z) #N n by XCMPLX_1:175
.=(cos_C/.z + <i>*sin_C/.-z) #N n by Th2
.=(cos_C/.-z + <i>*sin_C/.-z) #N n by Th3
.= cos_C/.([*n,0*]*-z) + <i>*sin_C/.([*n,0*]*-z) by Th51
.= cos_C/.(-[*n,0*]*z) + <i>*sin_C/.([*n,0*]*-z) by XCMPLX_1:175
.= cos_C/.(-[*n,0*]*z) + <i>*sin_C/.(-[*n,0*]*z) by XCMPLX_1:175
.= cos_C/.([*n,0*]*z) + <i>*sin_C/.(-[*n,0*]*z) by Th3
.= cos_C/.([*n,0*]*z) + <i>*-sin_C/.([*n,0*]*z) by Th2
.= cos_C/.([*n,0*]*z) + -<i>*sin_C/.([*n,0*]*z) by XCMPLX_1:175;
hence thesis by XCMPLX_0:def 8;
end;
theorem
for n being Nat, z being Element of COMPLEX holds
exp(<i>*[*n,0*]*z) = (cos_C/.z + <i>*sin_C/.z) #N n
proof
let n being Nat;
let z being Element of COMPLEX;
exp(<i>*[*n,0*]*z)
=exp(<i>*([*n,0*]*z)) by XCMPLX_1:4
.=cos_C/.([*n,0*]*z) + <i>*sin_C/.([*n,0*]*z) by Th36;
hence thesis by Th51;
end;
theorem
for n being Nat, z being Element of COMPLEX holds
exp(-<i>*[*n,0*]*z) = (cos_C/.z - <i>*sin_C/.z) #N n
proof
let n being Nat;
let z being Element of COMPLEX;
exp(-<i>*[*n,0*]*z)
=exp(-<i>*([*n,0*]*z)) by XCMPLX_1:4
.=cos_C/.([*n,0*]*z) - <i>*sin_C/.([*n,0*]*z) by Th37;
hence thesis by Th52;
end;
theorem
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*]
proof
let x,y being Element of REAL;
set shx = sinh.x, cy = cos.y, chx = cosh.x, sy = sin.y;
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:[*2,0*]*[*shx*cy+chx*sy,0*] = [*2*(shx*cy+chx*sy),0*]
proof
[*2,0*]*[*shx*cy+chx*sy,0*]
= [*2*(shx*cy+chx*sy)-0*0,2*0+0*(shx*cy+chx*sy)*] by HAHNBAN1:2;
hence thesis;
end;
[*1,-1*]/[*2,0*]*sinh_C/.[*x,y*] + [*1,1*]/[*2,0*]*sinh_C/.[*x,-y*]
= [*1,-1*]/[*2,0*]*[*shx*cy,chx*sy*] + [*1,1*]/[*2,0*]*sinh_C/.[*x,-y*]
by Th47
.= [*1,-1*]/[*2,0*]*[*shx*cy,chx*sy*] + [*1,1*]/[*2,0*]*[*shx*cy,-chx*sy*]
by Th48
.= [*1,-1*]*[*shx*cy,chx*sy*]/[*2,0*] + [*1,1*]/[*2,0*]*[*shx*cy,-chx*sy*]
by XCMPLX_1:75
.= [*1,-1*]*[*shx*cy,chx*sy*]/[*2,0*] + [*1,1*]*[*shx*cy,-chx*sy*]/[*2,0*]
by XCMPLX_1:75
.= ([*1,-1*]*[*shx*cy,chx*sy*] + [*1,1*]*[*shx*cy,-chx*sy*])/[*2,0*]
by XCMPLX_1:63
.= ([*1*(shx*cy)-(-1)*(chx*sy),1*(chx*sy)+(-1)*(shx*cy)*]
+ [*1,1*]*[*shx*cy,-chx*sy*])/[*2,0*] by HAHNBAN1:2
.= ([*shx*cy-(-1)*(chx*sy),chx*sy+(-1)*(shx*cy)*]
+ [*1*shx*cy-1*(-chx*sy),1*(-chx*sy)+1*shx*cy*])/[*2,0*] by HAHNBAN1:2
.= ([*shx*cy--chx*sy,chx*sy+(-1)*(shx*cy)*]
+ [*shx*cy-(-chx*sy),(-chx*sy)+shx*cy*])/[*2,0*] by XCMPLX_1:176
.= ([*shx*cy--chx*sy,chx*sy+-(1*(shx*cy))*]
+ [*shx*cy-(-chx*sy),(-chx*sy)+shx*cy*])/[*2,0*] by XCMPLX_1:175
.= [*shx*cy--chx*sy+(shx*cy--chx*sy),chx*sy+-shx*cy+(-chx*sy+shx*cy)*]
/[*2,0*] by COMPLFLD:2
.= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+chx*sy+-chx*sy+shx*cy*]
/[*2,0*] by XCMPLX_1:1
.= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+(chx*sy+-chx*sy)+shx*cy*]
/[*2,0*] by XCMPLX_1:1
.= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+(chx*sy-chx*sy)+shx*cy*]
/[*2,0*] by XCMPLX_0:def 8
.= [*shx*cy--chx*sy+(shx*cy--chx*sy),-shx*cy+0+shx*cy*]
/[*2,0*] by XCMPLX_1:14
.= [*shx*cy--chx*sy+(shx*cy--chx*sy),shx*cy-shx*cy*]
/[*2,0*] by XCMPLX_0:def 8
.= [*shx*cy--chx*sy+(shx*cy--chx*sy),0*]
/[*2,0*] by XCMPLX_1:14
.= [*shx*cy+--chx*sy+(shx*cy--chx*sy),0*]/[*2,0*] by XCMPLX_0:def 8
.= [*shx*cy+--chx*sy+(shx*cy+--chx*sy),0*]/[*2,0*] by XCMPLX_0:def 8
.= [*2,0*]*[*shx*cy+chx*sy,0*]/[*2,0*] by A2,XCMPLX_1:11;
hence thesis by A1,XCMPLX_1:90;
end;
theorem
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*]
proof
let x,y being Element of REAL;
set shx = sinh.x, cy = cos.y, chx = cosh.x, sy = sin.y;
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
A2:[*2,0*]*[*shx*sy+chx*cy,0*] = [*2*(shx*sy+chx*cy),0*]
proof
[*2,0*]*[*shx*sy+chx*cy,0*]
= [*2*(shx*sy+chx*cy)-0*0,2*0+0*(shx*sy+chx*cy)*] by HAHNBAN1:2;
hence thesis;
end;
[*1,-1*]/[*2,0*]*cosh_C/.[*x,y*] + [*1,1*]/[*2,0*]*cosh_C/.[*x,-y*]
= [*1,-1*]/[*2,0*]*[*chx*cy,shx*sy*] + [*1,1*]/[*2,0*]*cosh_C/.[*x,-y*]
by Th49
.= [*1,-1*]/[*2,0*]*[*chx*cy,shx*sy*] + [*1,1*]/[*2,0*]*[*chx*cy,-shx*sy*]
by Th50
.= [*1,-1*]*[*chx*cy,shx*sy*]/[*2,0*] + [*1,1*]/[*2,0*]*[*chx*cy,-shx*sy*]
by XCMPLX_1:75
.= [*1,-1*]*[*chx*cy,shx*sy*]/[*2,0*] + [*1,1*]*[*chx*cy,-shx*sy*]/[*2,0*]
by XCMPLX_1:75
.= ([*1,-1*]*[*chx*cy,shx*sy*] + [*1,1*]*[*chx*cy,-shx*sy*])/[*2,0*]
by XCMPLX_1:63
.= ([*1*(chx*cy)-(-1)*(shx*sy),1*(shx*sy)+(-1)*(chx*cy)*] +
[*1,1*]*[*chx*cy,-shx*sy*])/[*2,0*]
by HAHNBAN1:2
.= ([*chx*cy-(-1)*(shx*sy),shx*sy+(-1)*(chx*cy)*] +
[*1*(chx*cy)-1*(-shx*sy),1*(-shx*sy)+1*(chx*cy)*])/[*2,0*] by HAHNBAN1:2
.= ([*chx*cy--shx*sy,shx*sy+(-1)*(chx*cy)*] +
[*chx*cy--shx*sy,-shx*sy+chx*cy*])/[*2,0*] by XCMPLX_1:176
.= ([*chx*cy--shx*sy,shx*sy+-1*(chx*cy)*] +
[*chx*cy--shx*sy,-shx*sy+chx*cy*])/[*2,0*] by XCMPLX_1:175
.= [*chx*cy--shx*sy+(chx*cy--shx*sy),shx*sy+-chx*cy+(-shx*sy+chx*cy)*]
/[*2,0*] by COMPLFLD:2
.= [*2*(chx*cy--shx*sy),shx*sy+-chx*cy+(-shx*sy+chx*cy)*]
/[*2,0*] by XCMPLX_1:11
.= [*2*(chx*cy--shx*sy),-chx*cy+shx*sy+-shx*sy+chx*cy*]
/[*2,0*] by XCMPLX_1:1
.= [*2*(chx*cy--shx*sy),-chx*cy+(shx*sy+-shx*sy)+chx*cy*]
/[*2,0*] by XCMPLX_1:1
.= [*2*(chx*cy--shx*sy),-chx*cy+(shx*sy-shx*sy)+chx*cy*]
/[*2,0*] by XCMPLX_0:def 8
.= [*2*(chx*cy--shx*sy),-chx*cy+0+chx*cy*] /[*2,0*] by XCMPLX_1:14
.= [*2*(chx*cy--shx*sy),chx*cy-chx*cy*] /[*2,0*] by XCMPLX_0:def 8
.= [*2*(chx*cy--shx*sy),0*] /[*2,0*] by XCMPLX_1:14
.= [*2*(chx*cy+--shx*sy),0*] /[*2,0*] by XCMPLX_0:def 8
.= [*2,0*]*[*shx*sy+chx*cy,0*]/[*2,0*] by A2;
hence thesis by A1,XCMPLX_1:90;
end;
Lm13:
z + z = [*2,0*]*z
proof
z + z = [*Re z + Re z,Im z+Im z*] by COMPLEX1:def 9
.= [*2*(Re z),Im z+Im z*] by XCMPLX_1:11
.= [*2*(Re z),2*(Im z)*] by XCMPLX_1:11
.= [*Re ([*2,0*]*z),2*(Im z)*] by COMSEQ_3:17
.= [*Re ([*2,0*]*z),Im ([*2,0*]*z)*] by COMSEQ_3:17;
hence thesis by COMPLEX1:8;
end;
theorem
sinh_C/.z*sinh_C/.z = (cosh_C/.([*2,0*]*z) - [*1,0*])/[*2,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
set e1 = exp(z), e2 = exp(-z);
sinh_C/.z*sinh_C/.z
= (exp(z) - exp(-z))/[*2,0*]*sinh_C/.z by Lm3
.= (e1 - e2)/[*2,0*]*((e1 - e2)/[*2,0*]) by Lm3
.= (e1 - e2)*((e1 - e2)/[*2,0*])/[*2,0*] by XCMPLX_1:75
.= (e1 - e2)*(e1 - e2)/[*2,0*]/[*2,0*] by XCMPLX_1:75
.= (e1*e1 + e2*e2 - (e1*e2 + e1*e2))/[*2,0*]/[*2,0*] by Lm6
.= (e1*e1 + e2*e2 - [*2,0*]*(e1*e2))/[*2,0*]/[*2,0*] by Lm13
.= (e1*e1 + e2*e2 - [*2,0*]*1r)/[*2,0*]/[*2,0*] by Lm8,L1
.= (e1*e1 + e2*e2 - [*2,0*])/[*2,0*]/[*2,0*] by COMPLEX1:29
.= (exp(z+z) + e2*e2 - [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
.= (exp(z+z) + exp(-z+-z) - [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
.= (exp([*2,0*]*z) + exp(-z+-z) - [*2,0*])/[*2,0*]/[*2,0*] by Lm13
.= (exp([*2,0*]*z) + exp([*2,0*]*(-z)) - [*2,0*])/[*2,0*]/[*2,0*] by Lm13
.= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] - [*2,0*]/[*2,0*])
/[*2,0*] by XCMPLX_1:121
.= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] - [*1,0*])
/[*2,0*] by A1,COMPLEX1:86,L1
.= (( exp([*2,0*]*z) + exp(-[*2,0*]*(z)) )/[*2,0*] - [*1,0*])
/[*2,0*] by XCMPLX_1:175;
hence thesis by Lm4;
end;
theorem Th58:
cosh_C/.z*cosh_C/.z = (cosh_C/.([*2,0*]*z) + [*1,0*])/[*2,0*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
set e1 = exp(z), e2 = exp(-z);
cosh_C/.z*cosh_C/.z
= (exp(z) + exp(-z))/[*2,0*]*cosh_C/.z by Lm4
.= (e1 + e2)/[*2,0*]*((e1 + e2)/[*2,0*]) by Lm4
.= (e1 + e2)*((e1 + e2)/[*2,0*])/[*2,0*] by XCMPLX_1:75
.= (e1 + e2)*(e1 + e2)/[*2,0*]/[*2,0*] by XCMPLX_1:75
.= (e1*e1 + e2*e2 + e1*e2 + e1*e2)/[*2,0*]/[*2,0*] by Lm5
.= (e1*e1 + e2*e2 + (e1*e2 + e1*e2))/[*2,0*]/[*2,0*] by XCMPLX_1:1
.= (e1*e1 + e2*e2 + [*2,0*]*(e1*e2))/[*2,0*]/[*2,0*] by Lm13
.= (e1*e1 + e2*e2 + [*2,0*]*1r)/[*2,0*]/[*2,0*] by Lm8,L1
.= (e1*e1 + e2*e2 + [*2,0*])/[*2,0*]/[*2,0*] by COMPLEX1:29
.= (exp(z+z) + e2*e2 + [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
.= (exp(z+z) + exp(-z+-z) + [*2,0*])/[*2,0*]/[*2,0*] by SIN_COS:24
.= (exp([*2,0*]*z) + exp(-z+-z) + [*2,0*])/[*2,0*]/[*2,0*] by Lm13
.= (exp([*2,0*]*z) + exp([*2,0*]*(-z)) + [*2,0*])/[*2,0*]/[*2,0*] by Lm13
.= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] + [*2,0*]/[*2,0*])
/[*2,0*] by XCMPLX_1:63
.= (( exp([*2,0*]*z) + exp([*2,0*]*(-z)) )/[*2,0*] + [*1,0*])
/[*2,0*] by A1,COMPLEX1:86,L1
.= (( exp([*2,0*]*z) + exp(-[*2,0*]*(z)) )/[*2,0*] + [*1,0*])
/[*2,0*] by XCMPLX_1:175;
hence thesis by Lm4;
end;
theorem Th59:
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*]
proof
A1:[*2,0*] <> 0c by ARYTM_0:12,L0;
set e1 = exp(z), e2 = exp(-z);
A2:sinh_C/.([*2,0*]*z) = [*2,0*]*(sinh_C/.z)*(cosh_C/.z)
proof
[*2,0*]*(sinh_C/.z)*(cosh_C/.z)
= [*2,0*]*((sinh_C/.z)*(cosh_C/.z)) by XCMPLX_1:4
.= [*2,0*]*((sinh_C/.z)*((e1 + e2)/[*2,0*])) by Lm4
.= [*2,0*]*((e1 - e2)/[*2,0*]*((e1 + e2)/[*2,0*])) by Lm3
.= [*2,0*]*((e1 - e2)*((e1 + e2)/[*2,0*])/[*2,0*]) by XCMPLX_1:75
.= [*2,0*]*((e1 - e2)*(e1 + e2)/[*2,0*]/[*2,0*]) by XCMPLX_1:75
.= [*2,0*]*((e1 - e2)*(e1 + e2)/[*2,0*])/[*2,0*] by XCMPLX_1:75
.= (e1 - e2)*(e1 + e2)/[*2,0*] by A1,XCMPLX_1:90
.= ((e1 - e2)*e1 + (e1 - e2)*e2)/[*2,0*] by XCMPLX_1:8
.= (e1*e1 - e2*e1 + (e1 - e2)*e2)/[*2,0*] by XCMPLX_1:40
.= (e1*e1 - e2*e1 + (e1*e2 - e2*e2))/[*2,0*] by XCMPLX_1:40
.= ((e1*e1 - e2*e1 + e1*e2) - e2*e2)/[*2,0*] by XCMPLX_1:29
.= (e1*e1 - e2*e2)/[*2,0*] by XCMPLX_1:27
.= (exp(z+z) - e2*e2)/[*2,0*] by SIN_COS:24
.= (exp(z+z) - exp(-z+-z))/[*2,0*] by SIN_COS:24
.= (exp([*2,0*]*z) - exp(-z+-z))/[*2,0*] by Lm13
.= (exp([*2,0*]*z) - exp([*2,0*]*-z))/[*2,0*] by Lm13
.= (exp([*2,0*]*z) - exp(-[*2,0*]*z))/[*2,0*] by XCMPLX_1:175;
hence thesis by Lm3;
end;
cosh_C/.([*2,0*]*z) = [*2,0*]*(cosh_C/.z)*(cosh_C/.z) - [*1,0*]
proof
[*2,0*]*(cosh_C/.z)*(cosh_C/.z) - [*1,0*]
= [*2,0*]*((cosh_C/.z)*(cosh_C/.z)) - [*1,0*] by XCMPLX_1:4
.= [*2,0*]*((cosh_C/.([*2,0*]*z) + [*1,0*])/[*2,0*]) - [*1,0*] by Th58
.= ([*2,0*]*(cosh_C/.([*2,0*]*z) + [*1,0*])/[*2,0*]) - [*1,0*]
by XCMPLX_1:75
.= cosh_C/.([*2,0*]*z) + [*1,0*] - [*1,0*] by A1,XCMPLX_1:90;
hence thesis by XCMPLX_1:26;
end;
hence thesis by A2;
end;
theorem Th60:
(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)
proof
set s1 = sinh_C/.z1, s2 = sinh_C/.z2, c1 = cosh_C/.z1, c2 = cosh_C/.z2;
A1:(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))=(s1*s1)*(c2*c2)-(s2*s2)*(c1*c1)
proof
(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
=(s1*c2+c1*s2)*(sinh_C/.(z1-z2)) by Th11
.=(s1*c2+c1*s2)*(s1*c2-c1*s2) by Th12
.=(s1*c2+c1*s2)*(s1*c2)-(s1*c2+c1*s2)*(c1*s2) by XCMPLX_1:40
.=s1*c2*(s1*c2)+c1*s2*(s1*c2)-(s1*c2+c1*s2)*(c1*s2) by XCMPLX_1:8
.=s1*c2*(s1*c2)+c1*s2*(s1*c2)-(s1*c2*(c1*s2)+c1*s2*(c1*s2)) by XCMPLX_1:8
.=s1*c2*(s1*c2)+c1*s2*(s1*c2)-s1*c2*(c1*s2)-c1*s2*(c1*s2) by XCMPLX_1:36
.=s1*c2*(s1*c2)-c1*s2*(c1*s2) by XCMPLX_1:26
.=c2*s1*s1*c2-c1*s2*(c1*s2) by XCMPLX_1:4
.=(s1*s1)*c2*c2-c1*s2*(c1*s2) by XCMPLX_1:4
.=(s1*s1)*(c2*c2)-c1*s2*(c1*s2) by XCMPLX_1:4
.=(s1*s1)*(c2*c2)-s2*c1*c1*s2 by XCMPLX_1:4
.=(s1*s1)*(c2*c2)-s2*(c1*c1)*s2 by XCMPLX_1:4;
hence thesis by XCMPLX_1:4;
end;
A2:(sinh_C/.z1)*(sinh_C/.z1) - (sinh_C/.z2)*(sinh_C/.z2)
=(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
proof
(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
=(s1*s1)*(c2*c2)-(s1*s1)*(s2*s2)+(s1*s1)*(s2*s2)-(s2*s2)*(c1*c1)
by A1,XCMPLX_1:27
.=(s1*s1)*((c2*c2)-(s2*s2))+(s1*s1)*(s2*s2)-(s2*s2)*(c1*c1) by XCMPLX_1:40
.=(s1*s1)*1r+(s1*s1)*(s2*s2)-(s2*s2)*(c1*c1) by Th8
.=(s1*s1)*1r+((s1*s1)*(s2*s2)-(s2*s2)*(c1*c1)) by XCMPLX_1:29
.=(s1*s1)*1r+(s2*s2)*((s1*s1)-(c1*c1)) by XCMPLX_1:40
.=(s1*s1)*1r+(s2*s2)*-((c1*c1)-(s1*s1)) by XCMPLX_1:143
.=(s1*s1)*1r+(s2*s2)*-1r by Th8
.=(s1*s1)*1r+-(s2*s2) by COMPLEX1:46
.=(s1*s1)*1r-(s2*s2) by XCMPLX_0:def 8;
hence thesis by COMPLEX1:29;
end;
(cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z2)*(cosh_C/.z2)
=(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
proof
(sinh_C/.(z1+z2))*(sinh_C/.(z1-z2))
= (s1*s1)*(c2*c2)-(c1*c1)*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1)
by A1,XCMPLX_1:27
.= ((s1*s1)-(c1*c1))*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1) by XCMPLX_1:40
.= (-((c1*c1)-(s1*s1)))*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1)
by XCMPLX_1:143
.= (-1r)*(c2*c2)+(c1*c1)*(c2*c2)-(s2*s2)*(c1*c1) by Th8
.= (-1r)*(c2*c2)+((c1*c1)*(c2*c2)-(s2*s2)*(c1*c1)) by XCMPLX_1:29
.= (-1r)*(c2*c2)+(c1*c1)*((c2*c2)-(s2*s2)) by XCMPLX_1:40
.= (-1r)*(c2*c2)+(c1*c1)*1r by Th8
.= (-1r)*(c2*c2)+c1*c1 by COMPLEX1:29
.= -(c2*c2)+c1*c1 by COMPLEX1:46;
hence thesis by XCMPLX_0:def 8;
end;
hence thesis by A2;
end;
theorem Th61:
(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)
proof
set s1 = sinh_C/.z1, s2 = sinh_C/.z2, c1 = cosh_C/.z1, c2 = cosh_C/.z2;
A1:(cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
= (c1*c2+s1*s2)*(cosh_C/.(z1-z2)) by Th14
.= (c1*c2+s1*s2)*(c1*c2-s1*s2) by Th13
.= (c1*c2+s1*s2)*(c1*c2)-(c1*c2+s1*s2)*(s1*s2) by XCMPLX_1:40
.= c1*c2*(c1*c2)+s1*s2*(c1*c2)-(c1*c2+s1*s2)*(s1*s2) by XCMPLX_1:8
.= c1*c2*(c1*c2)+(c1*c2)*(s1*s2)-(c1*c2*(s1*s2)+s1*s2*(s1*s2)) by XCMPLX_1:8
.= c1*c2*(c1*c2)+(c1*c2)*(s1*s2)-c1*c2*(s1*s2)-s1*s2*(s1*s2) by XCMPLX_1:36
.= c1*c2*(c1*c2)-s1*s2*(s1*s2) by XCMPLX_1:26
.= c2*c1*c1*c2-s1*s2*(s1*s2) by XCMPLX_1:4
.= c2*(c1*c1)*c2-s1*s2*(s1*s2) by XCMPLX_1:4
.= c2*(c1*c1)*c2-s2*s1*s1*s2 by XCMPLX_1:4
.= c1*c1*c2*c2-(s1*s1)*s2*s2 by XCMPLX_1:4;
A2:(cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
=(sinh_C/.z1)*(sinh_C/.z1) + (cosh_C/.z2)*(cosh_C/.z2)
proof
(cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
= c1*c1*c2*c2 - s1*s1*c2*c2 + s1*s1*c2*c2 -s1*s1*s2*s2 by A1,XCMPLX_1:27
.= c1*c1*(c2*c2) - s1*s1*c2*c2 + s1*s1*c2*c2 -s1*s1*s2*s2 by XCMPLX_1:4
.= c1*c1*(c2*c2) - s1*s1*(c2*c2) + s1*s1*c2*c2 -s1*s1*s2*s2 by XCMPLX_1:4
.= c1*c1*(c2*c2) - s1*s1*(c2*c2) + (s1*s1*c2*c2 -s1*s1*s2*s2) by XCMPLX_1:29
.= (c1*c1 - s1*s1)*(c2*c2) + (s1*s1*c2*c2 -s1*s1*s2*s2) by XCMPLX_1:40
.= (c1*c1 - s1*s1)*(c2*c2) + (s1*s1*(c2*c2) -s1*s1*s2*s2) by XCMPLX_1:4
.= (c1*c1 - s1*s1)*(c2*c2) + (s1*s1*(c2*c2) -s1*s1*(s2*s2)) by XCMPLX_1:4
.= (c1*c1 - s1*s1)*(c2*c2) + s1*s1*(c2*c2-s2*s2) by XCMPLX_1:40
.= 1r*(c2*c2) + s1*s1*(c2*c2-s2*s2) by Th8
.= 1r*(c2*c2) + s1*s1*1r by Th8
.= (c2*c2) + s1*s1*1r by COMPLEX1:29;
hence thesis by COMPLEX1:29;
end;
(cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
=(cosh_C/.z1)*(cosh_C/.z1) + (sinh_C/.z2)*(sinh_C/.z2)
proof
(cosh_C/.(z1+z2))*(cosh_C/.(z1-z2))
= c1*c1*c2*c2 - c1*c1*s2*s2 + c1*c1*s2*s2 -s1*s1*s2*s2 by A1,XCMPLX_1:27
.= c1*c1*(c2*c2) - c1*c1*s2*s2 + c1*c1*s2*s2 -s1*s1*s2*s2 by XCMPLX_1:4
.= c1*c1*(c2*c2) - c1*c1*(s2*s2) + c1*c1*s2*s2 -s1*s1*s2*s2 by XCMPLX_1:4
.= c1*c1*(c2*c2) - c1*c1*(s2*s2) + c1*c1*(s2*s2) -s1*s1*s2*s2 by XCMPLX_1:4
.= c1*c1*(c2*c2) - c1*c1*(s2*s2) +c1*c1*(s2*s2)-s1*s1*(s2*s2) by XCMPLX_1:4
.= c1*c1*(c2*c2) - c1*c1*(s2*s2)+(c1*c1*(s2*s2)-s1*s1*(s2*s2)) by XCMPLX_1:29
.= c1*c1*(c2*c2 - s2*s2)+(c1*c1*(s2*s2)-s1*s1*(s2*s2)) by XCMPLX_1:40
.= c1*c1*(c2*c2 - s2*s2)+(c1*c1-s1*s1)*(s2*s2) by XCMPLX_1:40
.= c1*c1*1r+(c1*c1-s1*s1)*(s2*s2) by Th8
.= c1*c1*1r+1r*(s2*s2) by Th8
.= c1*c1+1r*(s2*s2) by COMPLEX1:29;
hence thesis by COMPLEX1:29;
end;
hence thesis by A2;
end;
theorem
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)
proof
set c1 = cosh_C/.z1, c2 = cosh_C/.z2, s1=sinh_C/.z1, s2=sinh_C/.z2;
A1:[*2,0*]*sinh_C/.(z1+z2)*cosh_C/.(z1-z2)
= [*2,0*]*(s1*c2+c1*s2)*cosh_C/.(z1-z2) by Th11
.= [*2,0*]*(s1*c2+c1*s2)*(c1*c2-s1*s2) by Th13
.= [*2,0*]*((s1*c2+c1*s2)*(c1*c2-s1*s2)) by XCMPLX_1:4
.= [*2,0*]*((s1*c2+c1*s2)*(c1*c2)-(s1*c2+c1*s2)*(s1*s2)) by XCMPLX_1:40
.= [*2,0*]*(s1*c2*(c1*c2)+c1*s2*(c1*c2)-(s1*c2+c1*s2)*(s1*s2)) by XCMPLX_1:8
.= [*2,0*]*(c1*s2*(c1*c2)+s1*c2*(c1*c2)-(s1*c2*(s1*s2)+c1*s2*(s1*s2)))
by XCMPLX_1:8
.= [*2,0*]*(c1*s2*(c1*c2)+s1*c2*(c1*c2)-c1*s2*(s1*s2)-s1*c2*(s1*s2))
by XCMPLX_1:36
.= [*2,0*]*((s1*c2*(c1*c2)-c1*s2*(s1*s2))+c1*s2*(c1*c2)-s1*c2*(s1*s2))
by XCMPLX_1:29
.= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(s1*s2)+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
by XCMPLX_1:29
.= [*2,0*]*(s1*c2*c2*c1-c1*s2*(s1*s2)+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*s1*c1-c1*s2*(s1*s2)+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*s1*c1-c1*s2*s2*s1+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*s2*(c1*c2)-s1*c2*(s1*s2)))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(s2*c1*c1*c2-s1*c2*(s1*s2)))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*c1*s2*c2-s1*c2*(s1*s2)))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*c1*s2*c2-c2*s1*s1*s2))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*s1*c1-s2*s2*c1*s1+(c1*c1*s2*c2-s1*s1*c2*s2))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*c1*s1+(c1*c1*s2*c2-s1*s1*c2*s2))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*(c1*s1)+(c1*c1*s2*c2-s1*s1*c2*s2))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*(c1*s1)+(c1*c1*(s2*c2)-s1*s1*c2*s2))
by XCMPLX_1:4
.= [*2,0*]*(c2*c2*(s1*c1)-s2*s2*(c1*s1)+(c1*c1*(s2*c2)-s1*s1*(c2*s2)))
by XCMPLX_1:4
.= [*2,0*]*((c2*c2-s2*s2)*(c1*s1)+(c1*c1*(s2*c2)-s1*s1*(c2*s2)))
by XCMPLX_1:40
.= [*2,0*]*((c2*c2-s2*s2)*(c1*s1)+(c1*c1-s1*s1)*(c2*s2))
by XCMPLX_1:40
.= [*2,0*]*(1r*(c1*s1)+(c1*c1-s1*s1)*(c2*s2)) by Th8
.= [*2,0*]*(1r*(c1*s1)+1r*(c2*s2)) by Th8
.= [*2,0*]*(c1*s1+1r*(c2*s2)) by COMPLEX1:29
.= [*2,0*]*(c1*s1+(c2*s2)) by COMPLEX1:29
.= [*2,0*]*(c1*s1)+[*2,0*]*(c2*s2) by XCMPLX_1:8
.= [*2,0*]*s1*c1+[*2,0*]*(c2*s2) by XCMPLX_1:4
.= [*2,0*]*s1*c1+[*2,0*]*s2*c2 by XCMPLX_1:4
.= sinh_C/.([*2,0*]*z1) + [*2,0*]*s2*c2 by Th59
.= sinh_C/.([*2,0*]*z1) + sinh_C/.([*2,0*]*z2) by Th59;
sinh_C/.([*2,0*]*z1) - sinh_C/.([*2,0*]*z2)
=[*2,0*]*sinh_C/.(z1-z2)*cosh_C/.(z1+z2)
proof
[*2,0*]*sinh_C/.(z1-z2)*cosh_C/.(z1+z2)
= [*2,0*]*(s1*c2-c1*s2)*cosh_C/.(z1+z2) by Th12
.= [*2,0*]*(s1*c2-c1*s2)*(c1*c2+s1*s2) by Th14
.= [*2,0*]*((s1*c2-c1*s2)*(c1*c2+s1*s2)) by XCMPLX_1:4
.= [*2,0*]*((s1*c2-c1*s2)*(c1*c2)+(s1*c2-c1*s2)*(s1*s2)) by XCMPLX_1:8
.= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(c1*c2)+(s1*c2-c1*s2)*(s1*s2)) by XCMPLX_1:40
.= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(c1*c2) + (s1*c2*(s1*s2)-c1*s2*(s1*s2)) )
by XCMPLX_1:40
.= [*2,0*]*(s1*c2*(c1*c2)-c1*s2*(c1*c2) + s1*c2*(s1*s2)-c1*s2*(s1*s2) )
by XCMPLX_1:29
.= [*2,0*]*(s1*c2*(c1*c2)+ -c1*s2*(c1*c2) + s1*c2*(s1*s2)-c1*s2*(s1*s2) )
by XCMPLX_0:def 8
.= [*2,0*]*(s1*c2*(c1*c2)+(s1*c2*(s1*s2)+ -c1*s2*(c1*c2)) -c1*s2*(s1*s2) )
by XCMPLX_1:1
.= [*2,0*]*(s1*c2*(s1*s2)-c1*s2*(c1*c2) + s1*c2*(c1*c2) -c1*s2*(s1*s2) )
by XCMPLX_0:def 8
.= [*2,0*]*(-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) + s1*c2*(c1*c2) -c1*s2*(s1*s2) )
by XCMPLX_1:143
.= [*2,0*]*(-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) +( s1*c2*(c1*c2) -c1*s2*(s1*s2)) )
by XCMPLX_1:29
.= [*2,0*]*(s1*c2*(c1*c2) -c1*s2*(s1*s2)-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
by XCMPLX_0:def 8
.= [*2,0*]*(c2*s1*c1*c2 -c1*s2*(s1*s2)-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*c2*c2 -c1*s2*(s1*s2)-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*c2*c2 -s2*c1*s1*s2-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*c2*c2 -c1*s1*s2*s2-(c1*s2*(c1*c2)-s1*c2*(s1*s2)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*c2*c2 -c1*s1*s2*s2-(c1*s2*c2*c1-s1*c2*(s1*s2)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*c2*c2 -s1*c1*s2*s2-(s2*c2*c1*c1-s1*c2*(s1*s2)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*c2*c2 -s1*c1*s2*s2-(s2*c2*c1*c1-s1*c2*s2*s1) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*c2*c2 -s1*c1*s2*s2-(s2*c2*c1*c1-s2*c2*s1*s1) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*s2*s2-(s2*c2*c1*c1-s2*c2*s1*s1) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*s2*s2-(s2*c2*c1*c1-s2*c2*(s1*s1)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*s2*s2-(s2*c2*(c1*c1)-s2*c2*(s1*s1)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*(c2*c2) -s1*c1*(s2*s2)-(s2*c2*(c1*c1)-s2*c2*(s1*s1)) )
by XCMPLX_1:4
.= [*2,0*]*(s1*c1*(c2*c2-s2*s2)-(s2*c2*(c1*c1)-s2*c2*(s1*s1)) )
by XCMPLX_1:40
.= [*2,0*]*(s1*c1*(c2*c2-s2*s2)-(s2*c2*(c1*c1-s1*s1))) by XCMPLX_1:40
.= [*2,0*]*(s1*c1*1r-(s2*c2*(c1*c1-s1*s1))) by Th8
.= [*2,0*]*(s1*c1*1r-(s2*c2*1r)) by Th8
.= [*2,0*]*(s1*c1-(s2*c2*1r)) by COMPLEX1:29
.= [*2,0*]*(s1*c1-(s2*c2)) by COMPLEX1:29
.= [*2,0*]*(s1*c1)-[*2,0*]*(s2*c2) by XCMPLX_1:40
.= [*2,0*]*s1*c1-[*2,0*]*(s2*c2) by XCMPLX_1:4
.= [*2,0*]*s1*c1-[*2,0*]*s2*c2 by XCMPLX_1:4
.= sinh_C/.([*2,0*]*z1)-[*2,0*]*s2*c2 by Th59;
hence thesis by Th59;
end;
hence thesis by A1;
end;
Lm14:
for z1 holds
(sinh_C/.z1)*(sinh_C/.z1) = (cosh_C/.z1)*(cosh_C/.z1) - [*1,0*]
proof
let z1;
(cosh_C/.z1)*(cosh_C/.z1) - [*1,0*] = (cosh_C/.z1)*(cosh_C/.z1)
- ((cosh_C/.z1)*(cosh_C/.z1) - (sinh_C/.z1)*(sinh_C/.z1))
by Th8,L1
.=(cosh_C/.z1)*(cosh_C/.z1)
- (cosh_C/.z1)*(cosh_C/.z1) + (sinh_C/.z1)*(sinh_C/.z1) by XCMPLX_1:37
.= (sinh_C/.z1)*(sinh_C/.z1)+
(cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z1)*(cosh_C/.z1) by XCMPLX_1:29;
hence thesis by XCMPLX_1:26;
end;
theorem
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)
proof
A1:[*2,0*]*cosh_C/.(z1+z2)*cosh_C/.(z1-z2)
=[*2,0*]*(cosh_C/.(z1+z2)*cosh_C/.(z1-z2 )) by XCMPLX_1:4
.=[*2,0*]*((sinh_C/.z1)*(sinh_C/.z1) + (cosh_C/.z2)*(cosh_C/.z2)) by Th61
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1) - [*1,0*] + (cosh_C/.z2)*(cosh_C/.z2))
by Lm14
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1) - [*1,0*])
+[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:8
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - [*2,0*]*[*1,0*]
+[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:40
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - ([*1,0*]+[*1,0*])
+[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by Lm13
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- ([*1,0*]+[*1,0*])
+[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_0:def 8
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +(- [*1,0*]+-[*1,0*])
+[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:140
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- [*1,0*]+-[*1,0*]
+[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:1
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- [*1,0*]+(-[*1,0*]
+[*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))) by XCMPLX_1:1
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) +- [*1,0*]+
([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))-[*1,0*]) by XCMPLX_0:def 8
.=[*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - [*1,0*]+
([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))-[*1,0*]) by XCMPLX_0:def 8
.=[*2,0*]*(cosh_C/.z1)*(cosh_C/.z1) - [*1,0*]+
([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) - [*1,0*]) by XCMPLX_1:4
.=[*2,0*]*(cosh_C/.z1)*(cosh_C/.z1) - [*1,0*]+
([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2) - [*1,0*]) by XCMPLX_1:4
.=cosh_C/.([*2,0*]*z1)+
([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2) - [*1,0*]) by Th59
.=cosh_C/.([*2,0*]*z1)+cosh_C/.([*2,0*]*z2) by Th59;
cosh_C/.([*2,0*]*z1)-cosh_C/.([*2,0*]*z2)
=[*2,0*]*sinh_C/.(z1+z2)*sinh_C/.(z1-z2)
proof
[*2,0*]*sinh_C/.(z1+z2)*sinh_C/.(z1-z2)
= [*2,0*]*(sinh_C/.(z1+z2)*sinh_C/.(z1-z2)) by XCMPLX_1:4
.= [*2,0*]*((cosh_C/.z1)*(cosh_C/.z1) - (cosh_C/.z2)*(cosh_C/.z2)) by Th60
.= [*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) - [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))
by XCMPLX_1:40
.= [*2,0*]*((cosh_C/.z1)*(cosh_C/.z1)) -[*1,0*]
+[*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:27
.= [*2,0*]*(cosh_C/.z1)*(cosh_C/.z1) -[*1,0*]
+[*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by XCMPLX_1:4
.= cosh_C/.([*2,0*]*z1)+[*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)) by Th59
.= cosh_C/.([*2,0*]*z1)+([*1,0*]- [*2,0*]*((cosh_C/.z2)*(cosh_C/.z2)))
by XCMPLX_1:29
.= cosh_C/.([*2,0*]*z1)+-([*2,0*]*((cosh_C/.z2)*(cosh_C/.z2))-[*1,0*])
by XCMPLX_1:143
.= cosh_C/.([*2,0*]*z1)+-([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2)-[*1,0*])
by XCMPLX_1:4
.= cosh_C/.([*2,0*]*z1)-([*2,0*]*(cosh_C/.z2)*(cosh_C/.z2)-[*1,0*])
by XCMPLX_0:def 8;
hence thesis by Th59;
end;
hence thesis by A1;
end;