:: Properties of Trigonometric Function
:: by Takashi Mitsuishi and Yuguang Yang
::
:: Received March 13, 1999
:: Copyright (c) 1999-2026 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 NUMBERS, XREAL_0, SUBSET_1, XXREAL_0, CARD_1, ARYTM_3, RELAT_1,
SQUARE_1, ARYTM_1, SIN_COS, XXREAL_1, ORDINAL2, REAL_1, FDIFF_1, FUNCT_1,
VALUED_0, NAT_1, NEWTON, BINOP_2, PARTFUN1, FUNCOP_1, SEQ_1, VALUED_1,
FUNCT_2, SEQ_2, TARSKI, RCOMP_1, XBOOLE_0, FCONT_1, SIN_COS2, FUNCT_7,
ORDINAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
VALUED_0, FUNCT_1, FUNCT_2, RELSET_1, FCONT_1, FDIFF_1, NAT_1, FUNCOP_1,
SQUARE_1, NEWTON, PARTFUN1, SEQ_2, RCOMP_1, RFUNCT_1, SIN_COS, VALUED_1,
SEQ_1, BINOP_2, XXREAL_0, REAL_1;
constructors PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, BINOP_2, SEQ_2,
RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1, FDIFF_1, SIN_COS, VALUED_1,
RELSET_1, NEWTON, COMSEQ_2, NUMBERS;
registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1,
MEMBERED, RCOMP_1, FDIFF_1, SIN_COS, VALUED_0, VALUED_1, FUNCT_2,
FCONT_3, NEWTON, SEQ_2, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, SUBSET_1;
theorems SEQ_1, SEQ_4, SQUARE_1, RCOMP_1, FUNCT_1, FDIFF_1, FDIFF_2, FUNCT_2,
RFUNCT_1, PARTFUN1, ROLLE, SIN_COS, NEWTON, XREAL_0, XCMPLX_0, XCMPLX_1,
BINOP_2, FUNCOP_1, XREAL_1, VALUED_1, XXREAL_1, VALUED_0, ORDINAL1;
schemes NAT_1, FUNCT_2;
begin :: Monotone increasing and monotone decreasing of sine and cosine.
reserve p,q,r,th,th1 for Real;
reserve n for Nat;
theorem Th1:
p>=0 & r>=0 implies p+r>=2*sqrt(p*r)
proof
assume that
A1: p>=0 and
A2: r>=0;
A3: (sqrt p - sqrt r)^2>=0 by XREAL_1:63;
(sqrt p - sqrt r)^2 =(sqrt p)^2 - 2*sqrt p*sqrt r + (sqrt r)^2
.=p-2*sqrt p*sqrt r + (sqrt r)^2 by A1,SQUARE_1:def 2
.=p -2*sqrt p*sqrt r +r by A2,SQUARE_1:def 2
.=p+r-2*sqrt p*sqrt r;
then 0+2*sqrt p*sqrt r <= p+r by A3,XREAL_1:19;
then 2*(sqrt p*sqrt r) <= p+r;
hence thesis by A1,A2,SQUARE_1:29;
end;
theorem
sin|].0,PI/2.[ is increasing
proof
for th st th in ].0,PI/2.[ holds 0 < diff(sin,th)
proof
let th;
assume th in ].0,PI/2.[;
then cos.th > 0 by SIN_COS:80;
hence thesis by SIN_COS:68;
end;
hence thesis by FDIFF_1:26,ROLLE:9,SIN_COS:24,68;
end;
Lm1: for th st th in ].0,PI/2.[ holds 0 < sin.th
proof
let th;
assume
A1: th in ].0,PI/2.[;
then th < PI/2 by XXREAL_1:4;
then -th>-PI/2 by XREAL_1:24;
then
A2: -th+PI/2 > -PI/2+ PI/2 by XREAL_1:6;
0 < th by A1,XXREAL_1:4;
then 0-th<0;
then -th+PI/2 < 0+PI/2 by XREAL_1:6;
then PI/2-th in ].0,PI/2.[ by A2,XXREAL_1:4;
then cos.(PI/2-th) > 0 by SIN_COS:80;
hence thesis by SIN_COS:78;
end;
theorem
sin|].PI/2,PI.[ is decreasing
proof
for th1 st th1 in ].PI/2,PI.[ holds 0 > diff(sin,th1)
proof
let th1;
assume
A1: th1 in ].PI/2,PI.[;
then th1 < PI by XXREAL_1:4;
then
A2: th1 - PI/2 < PI - PI/2 by XREAL_1:9;
PI/2 < th1 by A1,XXREAL_1:4;
then PI/2 - PI/2 < th1 - PI/2 by XREAL_1:9;
then th1-PI/2 in ].0,PI/2.[ by A2,XXREAL_1:4;
then sin.(th1-PI/2) > 0 by Lm1;
then
A3: 0-sin.(th1-PI/2) < 0;
diff(sin,(th1))=cos.(PI/2+(th1-PI/2)) by SIN_COS:68
.=-sin.(th1-PI/2) by SIN_COS:78;
hence thesis by A3;
end;
hence thesis by FDIFF_1:26,ROLLE:10,SIN_COS:24,68;
end;
theorem
cos|].0,PI/2.[ is decreasing
proof
for th st th in ].0,PI/2.[ holds diff(cos,th) < 0
proof
let th;
assume th in ].0,PI/2.[;
then 0 < sin.(th) by Lm1;
then diff(cos,th) = -sin.(th) & 0-sin.(th) < 0 by SIN_COS:67;
hence thesis;
end;
hence thesis by FDIFF_1:26,ROLLE:10,SIN_COS:24,67;
end;
theorem
cos|].PI/2,PI.[ is decreasing
proof
for th st th in ].PI/2,PI.[ holds diff(cos,th) < 0
proof
let th;
assume
A1: th in ].PI/2,PI.[;
then th < PI by XXREAL_1:4;
then
A2: th - PI/2 < PI - PI/2 by XREAL_1:9;
PI/2 < th by A1,XXREAL_1:4;
then PI/2 - PI/2 < th - PI/2 by XREAL_1:9;
then th-PI/2 in ].0,PI/2.[ by A2,XXREAL_1:4;
then cos.(th-PI/2) > 0 by SIN_COS:80;
then
A3: 0-cos.(th-PI/2) < 0;
diff(cos,(th))=-sin.(PI/2+(th-PI/2)) by SIN_COS:67
.=-cos.(th-PI/2) by SIN_COS:78;
hence thesis by A3;
end;
hence thesis by FDIFF_1:26,ROLLE:10,SIN_COS:24,67;
end;
theorem
sin|].PI,3/2*PI.[ is decreasing
proof
for th st th in ].PI,3/2*PI.[ holds diff(sin,(th))<0
proof
let th such that
A1: th in ].PI,3/2*PI.[;
th < 3/2*PI by A1,XXREAL_1:4;
then
A2: th-PI < 3/2*PI-PI by XREAL_1:9;
PI < th by A1,XXREAL_1:4;
then PI-PI < th-PI by XREAL_1:9;
then th-PI in ].0,PI/2.[ by A2,XXREAL_1:4;
then cos.(th-PI) > 0 by SIN_COS:80;
then
A3: 0-cos.(th-PI) < 0;
diff(sin,(th))= cos.(PI+(th-PI)) by SIN_COS:68
.= -cos.(th-PI) by SIN_COS:78;
hence thesis by A3;
end;
hence thesis by FDIFF_1:26,ROLLE:10,SIN_COS:24,68;
end;
theorem
sin|].3/2*PI,2*PI.[ is increasing
proof
for th st th in ].3/2*PI,2*PI.[ holds diff(sin,(th))>0
proof
let th such that
A1: th in ].3/2*PI,2*PI.[;
th < 2*PI by A1,XXREAL_1:4;
then
A2: th-3/2*PI < 2*PI-3/2*PI by XREAL_1:9;
A3: diff(sin,(th)) = cos.(PI + (PI/2+(th-3/2*PI))) by SIN_COS:68
.= -cos.(PI/2+(th-3/2*PI)) by SIN_COS:78
.= -(-sin.(th-3/2*PI)) by SIN_COS:78
.= sin.(th-3/2*PI);
3/2*PI < th by A1,XXREAL_1:4;
then 3/2*PI-3/2*PI < th-3/2*PI by XREAL_1:9;
then th-3/2*PI in ].0,PI/2.[ by A2,XXREAL_1:4;
hence thesis by A3,Lm1;
end;
hence thesis by FDIFF_1:26,ROLLE:9,SIN_COS:24,68;
end;
theorem
cos|].PI,3/2*PI.[ is increasing
proof
for th st th in ].PI,3/2*PI.[ holds diff(cos,(th))>0
proof
let th such that
A1: th in ].PI,3/2*PI.[;
th < 3/2*PI by A1,XXREAL_1:4;
then
A2: th-PI < 3/2*PI-PI by XREAL_1:9;
A3: diff(cos,(th)) = -sin.(PI+(th-PI)) by SIN_COS:67
.= -(-sin.(th-PI)) by SIN_COS:78
.= sin.(th-PI);
PI < th by A1,XXREAL_1:4;
then PI-PI < th-PI by XREAL_1:9;
then th-PI in ].0,PI/2.[ by A2,XXREAL_1:4;
hence thesis by A3,Lm1;
end;
hence thesis by FDIFF_1:26,ROLLE:9,SIN_COS:24,67;
end;
theorem
cos|].3/2*PI,2*PI.[ is increasing
proof
for th st th in ].3/2*PI,2*PI.[ holds diff(cos,(th))>0
proof
let th such that
A1: th in ].3/2*PI,2*PI.[;
th < 2*PI by A1,XXREAL_1:4;
then
A2: th-3/2*PI < 2*PI-3/2*PI by XREAL_1:9;
A3: diff(cos,(th)) = -sin.(PI + (PI/2+(th-3/2*PI))) by SIN_COS:67
.= -(-sin.(PI/2+(th-3/2*PI))) by SIN_COS:78
.= cos.(th-3/2*PI) by SIN_COS:78;
3/2*PI < th by A1,XXREAL_1:4;
then 3/2*PI-3/2*PI < th-3/2*PI by XREAL_1:9;
then th-3/2*PI in ].0,PI/2.[ by A2,XXREAL_1:4;
hence thesis by A3,SIN_COS:80;
end;
hence thesis by FDIFF_1:26,ROLLE:9,SIN_COS:24,67;
end;
theorem
for n being Nat holds sin.th = sin.(2*PI*n + th)
proof
defpred X[Nat] means for th holds sin.th = sin.(2*PI*$1 + th);
let n be Nat;
A1: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat such that
A2: for th holds sin.th = sin.(2*PI*n + th);
for th holds sin.th = sin.(2*PI*(n+1) + th)
proof
let th;
sin.(2*PI*(n+1) + th) = sin.((2*PI*n+th) + 2*PI)
.= sin.(2*PI*n + th) by SIN_COS:78
.= sin.th by A2;
hence thesis;
end;
hence thesis;
end;
A3: X[0];
for n being Nat holds X[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem
for n being Nat holds cos.th = cos.(2*PI*n + th)
proof
defpred X[Nat] means for th holds cos.th = cos.(2*PI*$1 + th);
let n be Nat;
A1: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat such that
A2: for th holds cos.th = cos.(2*PI*n + th);
for th holds cos.th = cos.(2*PI*(n+1) + th)
proof
let th;
cos.(2*PI*(n+1) + th) = cos.((2*PI*n+th) + 2*PI)
.= cos.(2*PI*n + th) by SIN_COS:78
.= cos.th by A2;
hence thesis;
end;
hence thesis;
end;
A3: X[0];
for n being Nat holds X[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
begin ::Hyperbolic sine, hyperbolic cosine and hyperbolic tangent.
definition
func sinh -> Function of REAL, REAL means
:Def1:
for d being Real holds it.d=(exp_R.d - exp_R.(-d))/2;
existence
proof
deffunc U(Real) = In((exp_R.($1) - exp_R.(-$1))/2,REAL);
consider f being Function of REAL, REAL such that
A1: for d be Element of REAL holds f.d = U(d) from FUNCT_2:sch 4;
take f;
let d be Real;
d in REAL by XREAL_0:def 1;
then f.d = U(d) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume
A2: for d being Real holds f1.d=(exp_R.d - exp_R.(-d))/2;
assume
A3: for d being Real holds f2.d=(exp_R.d - exp_R.(-d))/2;
for d being Element of REAL holds f1.d = f2.d
proof
let d be Element of REAL;
thus f1.d=(exp_R.d - exp_R.(-d))/2 by A2
.=f2.d by A3;
end;
hence f1=f2 by FUNCT_2:63;
end;
end;
definition
let d be object;
func sinh(d) -> number equals
sinh.d;
coherence;
end;
registration
let d be object;
cluster sinh(d) -> real;
coherence;
end;
definition
func cosh -> Function of REAL, REAL means
:Def3:
for d being Real holds it.d=(exp_R.d + exp_R.(-d))/2;
existence
proof
deffunc U(Real) = In((exp_R.$1 + exp_R.(-$1))/2,REAL);
consider f being Function of REAL, REAL such that
A1: for d be Element of REAL holds f.d = U(d) from FUNCT_2:sch 4;
take f;
let d be Real;
d in REAL by XREAL_0:def 1;
then f.d = U(d) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume
A2: for d being Real holds f1.d=(exp_R.d + exp_R.(-d))/2;
assume
A3: for d being Real holds f2.d=(exp_R.d + exp_R.(-d))/2;
for d being Element of REAL holds f1.d = f2.d
proof
let d be Element of REAL;
thus f1.d=(exp_R.d + exp_R.(-d))/2 by A2
.=f2.d by A3;
end;
hence f1=f2 by FUNCT_2:63;
end;
end;
definition
let d be object;
func cosh(d) -> number equals
cosh.d;
coherence;
end;
registration
let d be object;
cluster cosh(d) -> real;
coherence;
end;
definition
func tanh -> Function of REAL, REAL means
:Def5:
for d being Real
holds it.d=(exp_R.d - exp_R.(-d))/(exp_R.d + exp_R.(-d));
existence
proof
deffunc U(Real) =
In((exp_R.$1 - exp_R.(-$1))/(exp_R.$1 + exp_R.(-$1)),REAL);
consider f being Function of REAL, REAL such that
A1: for d be Element of REAL holds f.d = U(d) from FUNCT_2:sch 4;
take f;
let d be Real;
d in REAL by XREAL_0:def 1;
then f.d = U(d) by A1;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of REAL, REAL;
assume
A2: for d being Real holds f1.d=(exp_R.(d) - exp_R.(-d))/(exp_R
.d + exp_R.(-d));
assume
A3: for d being Real holds f2.d=(exp_R.(d) - exp_R.(-d))/(exp_R
.(d) + exp_R.(-d));
for d being Element of REAL holds f1.d = f2.d
proof
let d be Element of REAL;
thus f1.d=(exp_R.(d) - exp_R.(-d))/(exp_R.(d) + exp_R.(-d)) by A2
.=f2.d by A3;
end;
hence f1=f2 by FUNCT_2:63;
end;
end;
definition
let d be object;
func tanh(d) -> number equals
tanh.d;
coherence;
end;
registration
let d be object;
cluster tanh(d) -> real;
coherence;
end;
theorem Th12:
exp_R.(p+q) = exp_R.(p) * exp_R.(q)
proof
exp_R.(p+q) = exp_R(p+q) by SIN_COS:def 23
.= exp_R(p) * exp_R(q) by SIN_COS:50
.= exp_R.(p) * exp_R(q) by SIN_COS:def 23
.= exp_R.(p) * exp_R.(q) by SIN_COS:def 23;
hence thesis;
end;
theorem Th13:
exp_R.0 = 1 by SIN_COS:51,def 23;
theorem Th14:
(cosh.p)^2-(sinh.p)^2=1 & (cosh.p)*(cosh.p)-(sinh.p)*(sinh.p)=1
proof
A1: (sinh.p)*(sinh.p) = ((exp_R.(p) - exp_R.(-p))/2)*(sinh.p) by Def1
.= ((exp_R.(p) - exp_R.(-p))/2)*((exp_R.(p) - exp_R.(-p))/2) by Def1
.= ((exp_R.(p))*(exp_R.(p))-(exp_R.(p))*(exp_R.(-p)) -(exp_R.(-p))*(
exp_R.(p))+(exp_R.(-p))*(exp_R.(-p)))/(2*2)
.= ((exp_R.(p+p))-(exp_R.(p))*(exp_R.(-p)) -(exp_R.(-p))*(exp_R.(p))+(
exp_R.(-p))*(exp_R.(-p)))/4 by Th12
.= ((exp_R.(p+p))-(exp_R.(p+-p)) -(exp_R.(-p))*(exp_R.(p))+(exp_R.(-p))*
(exp_R.(-p)))/4 by Th12
.= ((exp_R.(p+p))-(exp_R.(p+-p)) -(exp_R.(-p))*(exp_R.(p))+(exp_R.(-p+-p
)))/4 by Th12
.= ((exp_R.(p+p)) - 1 - 1 + (exp_R.(-p+-p)))/4 by Th12,Th13;
(cosh.p)*(cosh.p) = ((exp_R.(p) + exp_R.(-p))/2)*(cosh.p) by Def3
.= ((exp_R.(p) + exp_R.(-p))/2)*((exp_R.(p) + exp_R.(-p))/2) by Def3
.= ((exp_R.(p))*(exp_R.(p))+(exp_R.(p))*(exp_R.(-p)) +(exp_R.(-p))*(
exp_R.(p))+(exp_R.(-p))*(exp_R.(-p)))/(2*2)
.= ((exp_R.(p+p))+(exp_R.(p))*(exp_R.(-p)) +(exp_R.(-p))*(exp_R.(p))+(
exp_R.(-p))*(exp_R.(-p)))/4 by Th12
.= ((exp_R.(p+p))+(exp_R.(p+-p)) +(exp_R.(-p))*(exp_R.(p))+(exp_R.(-p))*
(exp_R.(-p)))/4 by Th12
.= ((exp_R.(p+p))+(exp_R.(p+-p)) +(exp_R.(-p))*(exp_R.(p))+(exp_R.(-p+-p
)))/4 by Th12
.= ((exp_R.(p+p)) + 1 + 1 + (exp_R.(-p+-p)))/4 by Th12,Th13
.= ((exp_R.(p+p)) + 2 + (exp_R.(-p+-p)))/4;
hence thesis by A1;
end;
Lm2: cosh.(p+r)=(cosh.p)*(cosh.r) + (sinh.p)*(sinh.r)
proof
(cosh.p)*(cosh.r) + (sinh.p)*(sinh.r) =((exp_R.(p) + exp_R.(-p))/2)*(
cosh.r) +(sinh.p)*(sinh.r) by Def3
.=((exp_R.(p) + exp_R.(-p))/2)*((exp_R.(r) + exp_R.(-r))/2) +(sinh.p)*(
sinh.r) by Def3
.=((exp_R.(p) + exp_R.(-p))/2)*((exp_R.(r) + exp_R.(-r))/2) +((exp_R.(p)
- exp_R.(-p))/2)*(sinh.r) by Def1
.=((exp_R.(p) + exp_R.(-p))/2)*((exp_R.(r) + exp_R.(-r))/2) +((exp_R.(p)
- exp_R.(-p))/2)*((exp_R.(r) - exp_R.(-r))/2) by Def1
.=( 2*((exp_R.(p))*(exp_R.(r))) + 2*((exp_R.(-p))*(exp_R.(-r))) )/4
.=( 2*(exp_R.(p+r)) + 2*((exp_R.(-p))*(exp_R.(-r))) )/4 by Th12
.=( 2*(exp_R.(p+r)) + 2*(exp_R.(-p+-r)) )/4 by Th12
.=(exp_R.(p+r)+exp_R.(-(p+r)))/2
.=cosh.(p+r) by Def3;
hence thesis;
end;
Lm3: sinh.(p+r)=(sinh.p)*(cosh.r) + (cosh.p)*(sinh.r)
proof
(sinh.p)*(cosh.r) + (cosh.p)*(sinh.r) =((exp_R.(p) - exp_R.(-p))/2)*(
cosh.r) + (cosh.p)*(sinh.r) by Def1
.=((exp_R.(p) - exp_R.(-p))/2)*((exp_R.(r) + exp_R.(-r))/2) + (cosh.p)*(
sinh.r) by Def3
.=((exp_R.(p) - exp_R.(-p))/2)*((exp_R.(r) + exp_R.(-r))/2) + ((exp_R.(p
) + exp_R.(-p))/2)*(sinh.r) by Def3
.=((exp_R.(p) - exp_R.(-p))/2)*((exp_R.(r) + exp_R.(-r))/2) + ((exp_R.(p
) + exp_R.(-p))/2)*((exp_R.(r) - exp_R.(-r))/2) by Def1
.=( 2*( (exp_R.(p))*(exp_R.(r)) )+2*( -((exp_R.(-p))*(exp_R.(-r))) ) )/4
.=( 2*(exp_R.(p+r))+2*( -(exp_R.(-p))*(exp_R.(-r)) ) )/4 by Th12
.=( 2*(exp_R.(p+r))+2*( -(exp_R.(-p+-r)) ) )/4 by Th12
.=(exp_R.(p+r)-exp_R.(-(p+r)))/2
.=sinh.(p+r) by Def1;
hence thesis;
end;
theorem Th15:
cosh.p <> 0 & cosh.p > 0 & cosh.0 = 1
proof
exp_R.p > 0 & exp_R.(-p) > 0 by SIN_COS:54;
then
A1: (exp_R.p+exp_R.(-p))/2 > 0 by XREAL_1:139;
cosh.0 = (exp_R.0+exp_R.(-0))/2 by Def3
.= 1 by SIN_COS:51,def 23;
hence thesis by A1,Def3;
end;
theorem Th16:
sinh.0 = 0
proof
sinh.0 = (exp_R.0-exp_R.(-0))/2 by Def1
.= 0;
hence thesis;
end;
theorem Th17:
tanh.p = (sinh.p)/(cosh.p)
proof
(sinh.p)/(cosh.p) =((exp_R.(p) - exp_R.(-p))/2)/(cosh.p) by Def1
.=((exp_R.(p) - exp_R.(-p))/2)/((exp_R.(p) + exp_R.(-p))/2) by Def3
.=(exp_R.(p) - exp_R.(-p))/(exp_R.(p) + exp_R.(-p)) by XCMPLX_1:55
.=tanh.p by Def5;
hence thesis;
end;
Lm4: for a1 be Real holds r<>0 & q<>0 implies (p*q + r*a1)/(r*q + p*a1)
= (p/r + a1/q)/(1 + (p/r)*(a1/q))
proof
let a1 be Real;
assume that
A1: r<>0 and
A2: q<>0;
(p*q + r*a1)/(r*q + p*a1) =( (p*q + r*a1)/(r*q) )/( (r*q + p*a1)/(r*q) )
by A1,A2,XCMPLX_1:6,55
.=( (p*q)/(r*q) + (r*a1)/(r*q) )/( (r*q + p*a1)/(r*q) ) by XCMPLX_1:62
.=( (p*q)/(r*q) + (r*a1)/(r*q) )/ ( (r*q)/(r*q) + (p*a1)/(r*q) ) by
XCMPLX_1:62
.=( p/r + (a1*r)/(q*r) )/( (r*q)/(r*q) + (p*a1)/(r*q) ) by A2,XCMPLX_1:91
.=( p/r + a1/q )/( (r*q)/(r*q) + (p*a1)/(r*q) ) by A1,XCMPLX_1:91
.=( p/r + a1/q )/( 1 + (p*a1)/(r*q) ) by A1,A2,XCMPLX_1:6,60
.=( p/r + a1/q )/( 1 + (p/r)*(a1/q) ) by XCMPLX_1:76;
hence thesis;
end;
Lm5: tanh.(p+r) = (tanh.p + tanh.r)/(1+ (tanh.p)*(tanh.r))
proof
A1: cosh.r <> 0 & cosh.p <> 0 by Th15;
tanh.(p+r) =(sinh.(p+r))/(cosh.(p+r)) by Th17
.=( (sinh.p)*(cosh.r) + (cosh.p)*(sinh.r) )/(cosh.(p+r)) by Lm3
.=( (sinh.p)*(cosh.r) + (cosh.p)*(sinh.r) )/ ( (cosh.p)*(cosh.r) + (sinh
.p)*(sinh.r) ) by Lm2
.=( (sinh.p)/(cosh.p) + (sinh.r)/(cosh.r) )/ ( 1 + ( (sinh.p)/(cosh.p) )
*( (sinh.r)/(cosh.r) ) ) by A1,Lm4
.=( tanh.p + (sinh.r)/(cosh.r) )/ ( 1 + ( (sinh.p)/(cosh.p) )*( (sinh.r)
/(cosh.r) ) ) by Th17
.=( tanh.p + tanh.r )/ ( 1 + ( (sinh.p)/(cosh.p) )*( (sinh.r)/(cosh.r) )
) by Th17
.=( tanh.p + tanh.r )/ ( 1 + ( tanh.p )*( (sinh.r)/(cosh.r) ) ) by Th17
.=( tanh.p + tanh.r )/( 1 + ( tanh.p )*( tanh.r ) ) by Th17;
hence thesis;
end;
theorem Th18:
(sinh.p)^2 = 1/2*(cosh.(2*p) - 1) & (cosh.p)^2 = 1/2*(cosh.(2*p) + 1)
proof
A1: (cosh.p)^2 =( (exp_R.(p) + exp_R.(-p))/2 )*(cosh.p) by Def3
.=( (exp_R.(p) + exp_R.(-p))/2 )*( (exp_R.(p) + exp_R.(-p))/2 ) by Def3
.=( (exp_R.(p))*(exp_R.(p))+(exp_R.(p))*(exp_R.(-p)) +(exp_R.(-p))*(
exp_R.(p))+(exp_R.(-p))*(exp_R.(-p)) )/4
.=( (exp_R.(p+p))+(exp_R.(p))*(exp_R.(-p)) +(exp_R.(p))*(exp_R.(-p))+(
exp_R.(-p))*(exp_R.(-p)) )/4 by Th12
.=( (exp_R.(p+p))+(exp_R.(p))*(exp_R.(-p)) +(exp_R.(p))*(exp_R.(-p))+(
exp_R.(-p+ -p)) )/4 by Th12
.=( (exp_R.(p+p))+(exp_R.(p+ -p)) +(exp_R.(p))*(exp_R.(-p))+(exp_R.(-p+
-p)) )/4 by Th12
.=( (exp_R.(p+p))+(exp_R.(p+ -p)) +(exp_R.(p+ -p))+(exp_R.(-p+ -p)) )/4
by Th12
.=( exp_R.(2*p) + 2*(exp_R.(0)) +exp_R.(-p+-p) )/4
.=( exp_R.(2*p) + 2*1 +exp_R.(-(2*p)) )/4 by SIN_COS:51,def 23
.=1/2*( ( exp_R.(2*p) +exp_R.(-(2*p)) )/2 ) + (1*2)/(2*2)
.=1/2*(cosh.(2*p))+ 1/2*((2*1/2)) by Def3
.=1/2*( cosh.(2*p)+ 1 );
(sinh.p)^2 =( (exp_R.(p) - exp_R.(-p))/2 )*(sinh.p) by Def1
.=( (exp_R.(p) - exp_R.(-p))/2 )*( (exp_R.(p) - exp_R.(-p))/2 ) by Def1
.=( (exp_R.(p))*(exp_R.(p))-(exp_R.(p))*(exp_R.(-p)) -(exp_R.(-p))*(
exp_R.(p))+(exp_R.(-p))*(exp_R.(-p)) )/4
.=( (exp_R.(p+p))-(exp_R.(p))*(exp_R.(-p)) -(exp_R.(p))*(exp_R.(-p))+(
exp_R.(-p))*(exp_R.(-p)) )/4 by Th12
.=( (exp_R.(p+p))-(exp_R.(p))*(exp_R.(-p)) -(exp_R.(p))*(exp_R.(-p))+(
exp_R.(-p+ -p)) )/4 by Th12
.=( (exp_R.(p+p))-(exp_R.(p+ -p)) -(exp_R.(p))*(exp_R.(-p))+(exp_R.(-p+
-p)) )/4 by Th12
.=( ((exp_R.(p+p))+ -(exp_R.(p+ -p)) -(exp_R.(p+ -p)) )+(exp_R.(-p+ -p))
)/4 by Th12
.=( exp_R.(2*p) + 2*(-(exp_R.(0))) +exp_R.(-p+-p) )/4
.=( exp_R.(2*p) + 2*(-1) +exp_R.(-(2*p)) )/4 by SIN_COS:51,def 23
.=1/2*( ( exp_R.(2*p) +exp_R.(-(2*p)) )/2 ) + ((-1)*2)/(2*2)
.=1/2*(cosh.(2*p))+ 1/2*((2*(-1))/2) by Def3
.=1/2*( cosh.(2*p) - 1 );
hence thesis by A1;
end;
Lm6: sinh.(2*p) = 2*(sinh.p)*(cosh.p) & cosh.(2*p) = 2*(cosh.p)^2 - 1
proof
A1: 2*(cosh.p)^2 =2*( 1/2*(cosh.(2*p) + 1) ) by Th18
.=cosh.(2*p) + 1;
2*(sinh.p)*(cosh.p) =2*( (exp_R.(p) - exp_R.(-p))/2 )*(cosh.p) by Def1
.=2*( (exp_R.(p) - exp_R.(-p))/2 )*( (exp_R.(p) + exp_R.(-p))/2 ) by Def3
.=2/4*((exp_R.p)^2 - (exp_R.(-p))^2)
.=2/4*( exp_R.(p+p)- (exp_R.(-p))*(exp_R.(-p)) ) by Th12
.=2/4*(exp_R.(2*p)- exp_R.(-p+ -p)) by Th12
.=( ( exp_R.(2*p)- exp_R.(-(2*p)) )/2 )*1
.=sinh.(2*p) by Def1;
hence thesis by A1;
end;
theorem Th19:
cosh.(-p) = cosh.p & sinh.(-p) = -sinh.p & tanh.(-p) = -tanh.p
proof
A1: cosh.(-p) = (exp_R.(-p) + exp_R.(-(-p)))/2 by Def3
.= cosh.p by Def3;
A2: sinh.(-p) = (exp_R.(-p) - exp_R.(-(-p)))/2 by Def1
.= -(exp_R.(p) - exp_R.(-p))/2
.= -sinh.p by Def1;
then tanh.(-p) = (-sinh.p)/(cosh.(-p)) by Th17
.= -(sinh.p)/(cosh.p) by A1,XCMPLX_1:187
.= -tanh.p by Th17;
hence thesis by A1,A2;
end;
Lm7: cosh.(p-r)=(cosh.p)*(cosh.r) - (sinh.p)*(sinh.r)
proof
cosh.(p-r)=cosh.(p+ -r) .=(cosh.p)*(cosh.-r) + (sinh.p)*(sinh.-r) by Lm2
.=(cosh.p)*(cosh.r) + (sinh.p)*(sinh.-r) by Th19
.=(cosh.p)*(cosh.r) + (sinh.p)*(-sinh.r) by Th19
.=(cosh.p)*(cosh.r) - ((sinh.p)*(sinh.r));
hence thesis;
end;
theorem
cosh.(p+r)=(cosh.p)*(cosh.r) + (sinh.p)*(sinh.r) & cosh.(p-r)=(cosh.p)
*(cosh.r) - (sinh.p)*(sinh.r) by Lm2,Lm7;
Lm8: sinh.(p-r)=(sinh.p)*(cosh.r) - (cosh.p)*(sinh.r)
proof
sinh.(p-r)=sinh.(p+-r) .=(sinh.p)*(cosh.-r) +(cosh.p)*(sinh.-r) by Lm3
.=(sinh.p)*(cosh.r) + (cosh.p)*(sinh.-r) by Th19
.=(sinh.p)*(cosh.r) + (cosh.p)*(-sinh.r) by Th19
.=(sinh.p)*(cosh.r) -((cosh.p)*(sinh.r));
hence thesis;
end;
theorem
sinh.(p+r)=(sinh.p)*(cosh.r) + (cosh.p)*(sinh.r) & sinh.(p-r)=(sinh.p)
*(cosh.r) - (cosh.p)*(sinh.r) by Lm3,Lm8;
Lm9: tanh.(p-r) = (tanh.p - tanh.r)/(1- (tanh.p)*(tanh.r))
proof
tanh.(p-r)=tanh.(p+-r) .=(tanh.p + tanh.-r)/(1+ (tanh.p)*(tanh.-r)) by Lm5
.=(tanh.p + -tanh.r)/(1+ (tanh.p)*(tanh.-r)) by Th19
.=(tanh.p - tanh.r)/(1+ (tanh.p)*(-tanh.r)) by Th19
.=(tanh.p - tanh.r)/(1 -(tanh.p*tanh.r));
hence thesis;
end;
theorem
tanh.(p+r) = (tanh.p + tanh.r)/(1+ (tanh.p)*(tanh.r)) & tanh.(p-r) = (
tanh.p - tanh.r)/(1- (tanh.p)*(tanh.r)) by Lm5,Lm9;
theorem
sinh.(2*p) = 2*(sinh.p)*(cosh.p) & cosh.(2*p) = 2*(cosh.p)^2 - 1 &
tanh.(2*p) = (2*tanh.p)/(1+(tanh.p)^2)
proof
tanh.(2*p)=tanh.(p+p) .=(tanh.p + tanh.p)/(1+ (tanh.p)*(tanh.p)) by Lm5
.=(2*tanh.p)/(1+ (tanh.p)^2);
hence thesis by Lm6;
end;
theorem Th24:
(sinh.p)^2 - (sinh.q)^2 = (sinh.(p+q))*(sinh.(p-q)) & (sinh.(p+q
))*(sinh.(p-q)) = (cosh.p)^2 - (cosh.q)^2 & (sinh.p)^2 - (sinh.q)^2 = (cosh.p)
^2 - (cosh.q)^2
proof
A1: (sinh.(p+q))*(sinh.(p-q)) =((sinh.p)*(cosh.q) + (cosh.p)*(sinh.q))*(sinh
.(p+(-q))) by Lm3
.=((sinh.p)*(cosh.q) + (cosh.p)*(sinh.q)) *((sinh.p)*(cosh.(-q)) + (cosh
.p)*(sinh.(-q))) by Lm3
.=((sinh.p)*(cosh.q) + (cosh.p)*(sinh.q)) *((sinh.p)*(cosh.q) + (cosh.p)
*(sinh.(-q))) by Th19
.=((sinh.p)*(cosh.q) + (cosh.p)*(sinh.q)) *((sinh.p)*(cosh.q) + (cosh.p)
*(-sinh.q)) by Th19
.= (sinh.p)^2*(cosh.q)^2-(sinh.q)^2*(cosh.p)^2;
then
A2: (sinh.(p+q))*(sinh.(p-q)) =(cosh.q)^2*( -((cosh.p)^2-(sinh.p)^2) ) +( ((
cosh.p)^2*(cosh.q)^2)+ -(sinh.q)^2*(cosh.p)^2 )
.=(cosh.q)^2*( -1 ) +( (cosh.p)^2*( (cosh.q)^2-(sinh.q)^2 ) ) by Th14
.=(cosh.q)^2*( -1 )+ ((cosh.p)^2*1) by Th14
.=(cosh.p)^2 -(cosh.q)^2;
(sinh.(p+q))*(sinh.(p-q)) =(sinh.p)^2*( (cosh.q)^2 -(sinh.q)^2 ) + ((
sinh.q)^2*(sinh.p)^2)-(sinh.q)^2*(cosh.p)^2 by A1
.=(sinh.p)^2*1 + (sinh.p)^2*(sinh.q)^2-(sinh.q)^2*(cosh.p)^2 by Th14
.=(sinh.p)^2 + (sinh.q)^2*(-((cosh.p)^2-(sinh.p)^2))
.=(sinh.p)^2 + (sinh.q)^2*(-1) by Th14
.=(sinh.p)^2 - (sinh.q)^2;
hence thesis by A2;
end;
theorem Th25:
(sinh.p)^2 + (cosh.q)^2 = (cosh.(p+q))*(cosh.(p-q)) & (cosh.(p+q
))*(cosh.(p-q)) = (cosh.p)^2 + (sinh.q)^2 & (sinh.p)^2 + (cosh.q)^2 = (cosh.p)
^2 + (sinh.q)^2
proof
A1: (cosh.(p+q))*(cosh.(p-q)) =( (cosh.p)*(cosh.q) + (sinh.p)*(sinh.q) )* (
cosh.(p + -q)) by Lm2
.=( ( (cosh.p)*(cosh.q) ) + ( (sinh.p)*(sinh.q) ) )* ( ( (cosh.p)*(cosh.
-q) ) + ( (sinh.p)*(sinh.-q) ) ) by Lm2
.=( (cosh.p)*(cosh.q) )*( (cosh.p)*(cosh.-q) ) +( (cosh.p)*(cosh.q) )*(
(sinh.p)*(sinh.-q) ) +( (sinh.p)*(sinh.q) )*( (cosh.p)*(cosh.-q) ) +( (sinh.p)*
(sinh.q) )*( (sinh.p)*(sinh.-q) )
.=( (cosh.p)*(cosh.q) )*( (cosh.p)*(cosh.q) ) +( (cosh.p)*(cosh.q) )*( (
sinh.-q)*(sinh.p) ) +( (sinh.p)*(sinh.q) )*( (cosh.p)*(cosh.-q) ) +( (sinh.p)*(
sinh.q) )*( (sinh.-q)*(sinh.p) ) by Th19
.=( (cosh.p)*(cosh.q) )^2 +( (sinh.-q)*(sinh.p) )*( (cosh.p)*(cosh.q) )
+( (sinh.p)*(sinh.q) )*( (cosh.p)*(cosh.q) ) +( (sinh.-q)*(sinh.p) )*( (sinh.p)
*(sinh.q) ) by Th19
.=( (cosh.p)*(cosh.q) )^2 +( (-sinh.q)*(sinh.p) )*( (cosh.p)*(cosh.q) )
+( (sinh.p)*(sinh.q) )*( (cosh.p)*(cosh.q) ) +( (sinh.-q)*(sinh.p) )*( (sinh.p)
*(sinh.q) ) by Th19
.=( (cosh.p)*(cosh.q) )^2 + 0 +( (-1)*(sinh.q)*(sinh.p) )*( (sinh.p)*(
sinh.q) ) by Th19
.=(cosh.p)^2*(cosh.q)^2 - (sinh.q)^2*(sinh.p)^2;
then
A2: (cosh.(p+q))*(cosh.(p-q)) =(cosh.p)^2*( (cosh.q)^2-(sinh.q)^2 ) + ((cosh
.p)^2*(sinh.q)^2) + -((sinh.q)^2*(sinh.p)^2)
.=(cosh.p)^2*1 + ((cosh.p)^2*(sinh.q)^2) + -((sinh.q)^2*(sinh.p)^2) by Th14
.=(cosh.p)^2+(sinh.q)^2*((cosh.p)^2-(sinh.p)^2)
.=(cosh.p)^2+(sinh.q)^2*1 by Th14
.=(cosh.p)^2+(sinh.q)^2;
(cosh.(p+q))*(cosh.(p-q)) =(cosh.q)^2*((cosh.p)^2-(sinh.p)^2) +( (cosh.q
)^2*(sinh.p)^2 + -(sinh.p)^2*(sinh.q)^2 ) by A1
.=(cosh.q)^2*1 +( (cosh.q)^2*(sinh.p)^2-(sinh.p)^2*(sinh.q)^2 ) by Th14
.=(cosh.q)^2+(sinh.p)^2*( (cosh.q)^2-(sinh.q)^2 )
.=(cosh.q)^2+(sinh.p)^2*1 by Th14
.=(cosh.q)^2+(sinh.p)^2;
hence thesis by A2;
end;
theorem
sinh.p + sinh.r = 2*(sinh.(p/2+r/2))*(cosh.(p/2-r/2)) & sinh.p - sinh.
r = 2*(sinh.(p/2-r/2))*(cosh.(p/2+r/2))
proof
A1: 2*(sinh.(p/2-r/2))*(cosh.(p/2+r/2)) =2*( (sinh.(p/2))*(cosh.(r/2))-(cosh
.(p/2))*(sinh.(r/2)) ) *(cosh.(p/2+r/2)) by Lm8
.=2*((sinh.(p/2))*(cosh.(r/2))-(cosh.(p/2))*(sinh.(r/2))) *((cosh.(p/2))
*(cosh.(r/2))+(sinh.(p/2))*(sinh.(r/2))) by Lm2
.=2*( ((cosh.(r/2))*(sinh.(r/2)))*(-((cosh.(p/2))^2-(sinh.(p/2))^2)) +(
sinh.(p/2))*( (cosh.(p/2))*(cosh.(r/2))^2 ) -(cosh.(p/2))*( (sinh.(p/2))*(sinh.
(r/2))^2 ) )
.=2*( ((cosh.(r/2))*(sinh.(r/2)))*(-1) +(sinh.(p/2))*( (cosh.(p/2))*(
cosh.(r/2))^2 ) -(cosh.(p/2))*( (sinh.(p/2))*(sinh.(r/2))^2 ) ) by Th14
.=2*( ((sinh.(p/2))*(cosh.(p/2)))*((cosh.(r/2))^2-(sinh.(r/2))^2) +(-1)*
((cosh.(r/2))*(sinh.(r/2))) )
.=2*( ((sinh.(p/2))*(cosh.(p/2)))*1 +(-1)*((cosh.(r/2))*(sinh.(r/2))) )
by Th14
.= 2*(sinh.(p/2))*(cosh.(p/2))-2*((sinh.(r/2))*(cosh.(r/2)))
.=sinh.(2*(p/2)) - 2*(sinh.(r/2))*(cosh.(r/2)) by Lm6
.=sinh.p - sinh.(2*(r/2)) by Lm6
.=sinh.p - sinh.r;
2*(sinh.(p/2+r/2))*(cosh.(p/2-r/2)) =2*((sinh.(p/2))*(cosh.(r/2))+(cosh.
(p/2))*(sinh.(r/2))) *(cosh.(p/2-r/2)) by Lm3
.=2*((sinh.(p/2))*(cosh.(r/2))+(cosh.(p/2))*(sinh.(r/2))) *((cosh.(p/2))
*(cosh.(r/2))-(sinh.(p/2))*(sinh.(r/2))) by Lm7
.=2*( ((sinh.(r/2))*(cosh.(r/2)))*((cosh.(p/2))^2-(sinh.(p/2))^2) +(sinh
.(p/2))*( (cosh.(p/2))*(cosh.(r/2))^2 ) -(cosh.(p/2))*( (sinh.(p/2))*(sinh.(r/2
))^2 ) )
.=2*( ((sinh.(r/2))*(cosh.(r/2)))*1 +(sinh.(p/2))*( (cosh.(p/2))*(cosh.(
r/2))^2 ) -(cosh.(p/2))*( (sinh.(p/2))*(sinh.(r/2))^2 ) ) by Th14
.=2*( ((sinh.(p/2))*(cosh.(p/2)))*((cosh.(r/2))^2 -(sinh.(r/2))^2 ) +(
sinh.(r/2))*(cosh.(r/2)) )
.=2*( ((sinh.(p/2))*(cosh.(p/2))*1)+(sinh.(r/2))*(cosh.(r/2)) ) by Th14
.=2*(sinh.(p/2))*(cosh.(p/2)) + 2*((sinh.(r/2))*(cosh.(r/2)))
.=sinh.(2*(p/2)) + 2*(sinh.(r/2))*(cosh.(r/2)) by Lm6
.=sinh.p + sinh.(2*(r/2)) by Lm6
.=sinh.p + sinh.r;
hence thesis by A1;
end;
theorem
cosh.p + cosh.r = 2*(cosh.(p/2+r/2))*(cosh.(p/2-r/2)) & cosh.p - cosh.
r = 2*(sinh.(p/2-r/2))*(sinh.(p/2+r/2))
proof
A1: 2*(sinh.(p/2-r/2))*(sinh.(p/2+r/2)) =2*((sinh.(p/2-r/2))*(sinh.(p/2+r/2) ))
.=2*( (cosh.(p/2))^2 - (cosh.(r/2))^2 ) by Th24
.=2*( 1/2*(cosh.(2*(p/2)) + 1)-(cosh.(r/2))^2 ) by Th18
.=2*( 1/2*(cosh.p + 1)-1/2*(cosh.(2*(r/2)) + 1) ) by Th18
.=cosh.p-cosh.r;
2*(cosh.(p/2+r/2))*(cosh.(p/2-r/2)) =2*((cosh.(p/2+r/2))*(cosh.(p/2-r/2) ))
.=2*( (sinh.(p/2))^2+(cosh.(r/2))^2 ) by Th25
.=2*( 1/2*(cosh.(2*(p/2)) - 1)+(cosh.(r/2))^2 ) by Th18
.=2*( 1/2*(cosh.p - 1)+1/2*(cosh.(2*(r/2)) + 1) ) by Th18
.=cosh.r+cosh.p;
hence thesis by A1;
end;
theorem
tanh.p + tanh.r = (sinh.(p+r))/((cosh.p)*(cosh.r)) & tanh.p - tanh.r =
(sinh.(p-r))/((cosh.p)*(cosh.r))
proof
A1: (sinh.(p-r))/((cosh.p)*(cosh.r)) =( (sinh.p)*(cosh.r)-(cosh.p)*(sinh.r)
)/((cosh.p)*(cosh.r)) by Lm8
.= ((sinh.p)*(cosh.r))/((cosh.p)*(cosh.r)) -((cosh.p)*(sinh.r))/((cosh.p
)*(cosh.r)) by XCMPLX_1:120
.=(sinh.p)/(cosh.p)-((cosh.p)*(sinh.r))/((cosh.p)*(cosh.r)) by Th15,
XCMPLX_1:91
.=(sinh.p)/(cosh.p)-(sinh.r)/(cosh.r) by Th15,XCMPLX_1:91
.=tanh.p-(sinh.r)/(cosh.r) by Th17
.=tanh.p-tanh.r by Th17;
(sinh.(p+r))/((cosh.p)*(cosh.r)) =( (sinh.p)*(cosh.r)+(cosh.p)*(sinh.r)
)/((cosh.p)*(cosh.r)) by Lm3
.= ((sinh.p)*(cosh.r))/((cosh.p)*(cosh.r)) +((cosh.p)*(sinh.r))/((cosh.p
)*(cosh.r)) by XCMPLX_1:62
.=(sinh.p)/(cosh.p)+((cosh.p)*(sinh.r))/((cosh.p)*(cosh.r)) by Th15,
XCMPLX_1:91
.=(sinh.p)/(cosh.p)+(sinh.r)/(cosh.r) by Th15,XCMPLX_1:91
.=tanh.p+(sinh.r)/(cosh.r) by Th17
.=tanh.p+tanh.r by Th17;
hence thesis by A1;
end;
theorem
(cosh.p + sinh.p) |^ n = cosh.(n*p) + sinh.(n*p)
proof
defpred X[Nat] means for p holds (cosh.p + sinh.p) |^ $1 = cosh.(
$1*p) + sinh.($1*p);
A1: for n st X[n] holds X[n+1]
proof
let n such that
A2: for p holds (cosh.p + sinh.p) |^ n = cosh.(n*p) + sinh.(n*p);
for p holds (cosh.p + sinh.p) |^ (n+1) = cosh.((n+1)*p) + sinh.((n+1)* p)
proof
let p;
A3: (cosh.(n*p))*(cosh.p)+(sinh.(n*p))*(sinh.p) =((exp_R.(n*p) + exp_R.(
-n*p))/2)*(cosh.p) +(sinh.(n*p))*(sinh.p) by Def3
.=((exp_R.(n*p) + exp_R.(-n*p))/2)*((exp_R.p + exp_R.-p)/2) +(sinh.(
n*p))*(sinh.p) by Def3
.=((exp_R.(n*p) + exp_R.(-n*p))/2)*((exp_R.p + exp_R.-p)/2) +((exp_R
.(n*p) - exp_R.(-n*p))/2)*(sinh.p) by Def1
.=((exp_R.(n*p))/2 + (exp_R.(-n*p))/2)*((exp_R.p)/2 + (exp_R.-p)/2)
+((exp_R.(n*p))/2 - (exp_R.(-n*p))/2)*((exp_R.p - exp_R.-p)/2) by Def1
.=2*( ( (exp_R.(n*p))*(exp_R.p) )/(2*2) ) +2*(((exp_R.(-n*p))/2)*((
exp_R.-p)/2))
.=2*( exp_R.(p*n+p*1)/(2*2) ) +2*( ( (exp_R.(-n*p))*(exp_R.-p) )/(2*
2) ) by Th12
.=2*( exp_R.(p*(n+1))/(2*2) ) +2*( exp_R.(-n*p+-p)/(2*2) ) by Th12
.=(exp_R.(p*(n+1))+exp_R.(-(p*(n+1))))/2
.=cosh.(p*(n+1)) by Def3;
A4: (cosh.(n*p))*(sinh.p)+(sinh.(n*p))*(cosh.p) =((exp_R.(n*p) + exp_R.(
-n*p))/2)*(sinh.p) +(sinh.(n*p))*(cosh.p) by Def3
.=((exp_R.(n*p) + exp_R.(-n*p))/2)*((exp_R.p - exp_R.-p)/2) +(sinh.(
n*p))*(cosh.p) by Def1
.=((exp_R.(n*p) + exp_R.(-n*p))/2)*((exp_R.p - exp_R.-p)/2) +((exp_R
.(n*p) - exp_R.(-n*p))/2)*(cosh.p) by Def1
.=((exp_R.(n*p))/2)*((exp_R.p)/2) - ((exp_R.(n*p))/2)*((exp_R.-p)/2)
+((exp_R.(-n*p))/2)*((exp_R.p)/2) - ((exp_R.(-n*p))/2)*((exp_R.-p)/2) +((exp_R.
(n*p) - exp_R.(-n*p))/2)*((exp_R.p + exp_R.-p)/2) by Def3
.=2*(( (exp_R.(n*p))*(exp_R.p) )/4 ) +2*( -( ((exp_R.(-n*p))*(exp_R.
-p))/(2*2) ))
.=2*( exp_R.(n*p+p)/4 ) +2*( -( ((exp_R.(-n*p))*(exp_R.-p))/4 )) by
Th12
.=2*( exp_R.(n*p+p)/4 ) +2*( -( (exp_R.(-n*p+-p))/4 ) ) by Th12
.=( exp_R.(p*(n+1))- exp_R.(-(p*(n+1))) )/2
.=sinh.(p*(n+1)) by Def1;
(cosh.p + sinh.p) |^ (n+1) =(cosh.p + sinh.p) |^ n * (cosh.p + sinh.
p) by NEWTON:6
.=(cosh.(n*p) + sinh.(n*p)) * (cosh.p + sinh.p) by A2
.=sinh.((n+1)*p)+cosh.((n+1)*p) by A3,A4;
hence thesis;
end;
hence thesis;
end;
A5: X[0] by Th15,Th16,NEWTON:4;
for n holds X[n] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem Th30:
dom sinh=REAL & dom cosh=REAL & dom tanh=REAL by FUNCT_2:def 1;
Lm10: for d being Real holds compreal.d=(-1)*d
proof
let d be Real;
thus compreal.d= -d by BINOP_2:def 7
.= (-1)*d;
end;
Lm11: dom(compreal)=REAL by FUNCT_2:def 1;
Lm12: for f being PartFunc of REAL,REAL st f = compreal holds for p holds f
is_differentiable_in p & diff(f,p) = -1
proof
reconsider f2 = REAL --> In(0,REAL) as Function of REAL,REAL;
deffunc U(Real) = In(-$1,REAL);
let f be PartFunc of REAL,REAL such that
A1: f = compreal;
let p;
consider f1 being Function of REAL,REAL such that
A2: for p be Element of REAL holds f1.p=U(p) from FUNCT_2:sch 4;
A3: dom f2 = REAL by FUNCOP_1:13;
for hy1 be 0-convergent non-zero Real_Sequence holds (hy1")(#)(f2/*hy1) is
convergent & lim ((hy1")(#)(f2/*hy1)) = 0
proof
let hy1 be 0-convergent non-zero Real_Sequence;
A4: for n being Nat holds ((hy1")(#)(f2/*hy1)).n=In(0,REAL)
proof
let n be Nat;
A5: rng hy1 c= dom f2 by A3;
A6: n in NAT by ORDINAL1:def 12;
((hy1")(#)(f2/*hy1)).n = (hy1".n)*((f2/*hy1).n) by SEQ_1:8
.= (hy1.n)"*((f2/*hy1).n) by VALUED_1:10;
then ((hy1")(#)(f2/*hy1)).n =(hy1.n)"*(f2.(hy1.n)) by A6,A5,FUNCT_2:108
.=(hy1.n)"*(0) by FUNCOP_1:7
.= 0;
hence thesis;
end;
then
A7: (hy1")(#)(f2/*hy1) is constant by VALUED_0:def 18;
for n holds lim ((hy1")(#)(f2/*hy1)) = 0
proof
let n;
lim ((hy1")(#)(f2/*hy1)) =((hy1")(#)(f2/*hy1)).n by A7,SEQ_4:26
.=0 by A4;
hence thesis;
end;
hence thesis by A7;
end;
then
A8: f2 is RestFunc by FDIFF_1:def 2;
A9: ex N being Neighbourhood of p st N c= dom compreal & for r st r
in N holds compreal.r - compreal.p = f1.(r-p) + f2.(r-p)
proof
take ].p-1,p+1 .[;
for r st r in ].p-1,p+1 .[ holds compreal.r - compreal.p = f1.(r-p) +
f2.(r-p)
proof
let r;
A10: for d be Real holds f2.d = 0
by XREAL_0:def 1,FUNCOP_1:7;
A11: for p be Real holds f1.p = - p
proof
let p be Real;
p in REAL by XREAL_0:def 1;
then f1.p=U(p) by A2;
hence thesis;
end;
compreal.r-compreal.p =(-1)*r - compreal.p by Lm10
.=(-1)*r -(-1)*p + 0 by Lm10
.=-(r-p) + f2.(r-p) by A10
.=f1.(r-p) + f2.(r-p) by A11;
hence thesis;
end;
hence thesis by Lm11,RCOMP_1:def 6;
end;
reconsider pp = p as Real;
A12: 1 in REAL by XREAL_0:def 1;
for p holds f1.p=(-1)*p
proof
let p;
reconsider pp = p as Element of REAL by XREAL_0:def 1;
f1.p = U(pp) by A2;
hence thesis;
end;
then
A13: f1 is LinearFunc by FDIFF_1:def 3;
then f is_differentiable_in pp by A1,A8,A9,FDIFF_1:def 4;
then diff(f,pp) = f1.1 by A1,A13,A8,A9,FDIFF_1:def 5
.= U(1) by A2,A12;
hence thesis by A1,A13,A8,A9,FDIFF_1:def 4;
end;
Lm13: for f being PartFunc of REAL,REAL st f = compreal holds exp_R*f
is_differentiable_in p & diff(exp_R*f,p) = (-1)*exp_R.(f.p)
proof
let f be PartFunc of REAL,REAL such that
A1: f = compreal;
A2: p is Real & exp_R is_differentiable_in f.p by SIN_COS:65;
A3: f is_differentiable_in p by A1,Lm12;
then diff(exp_R*f,p) =diff(exp_R,f.p)*diff(f,p) by A2,FDIFF_2:13
.=diff(exp_R,f.p)*(-1) by A1,Lm12
.=exp_R.(f.p)*(-1) by SIN_COS:65;
hence thesis by A2,A3,FDIFF_2:13;
end;
Lm14: for f being PartFunc of REAL,REAL st f = compreal holds exp_R.((-1)*p)=
(exp_R*f).p
proof
let f be PartFunc of REAL,REAL;
A1: p in REAL by XREAL_0:def 1;
assume
A2: f = compreal;
then exp_R.((-1)*p) =exp_R.(f.p) by Lm10
.=(exp_R*f).p by A2,A1,FUNCT_2:15;
hence thesis;
end;
Lm15: for f being PartFunc of REAL,REAL st f = compreal holds (exp_R-(exp_R*f)
) is_differentiable_in p & (exp_R+(exp_R*f)) is_differentiable_in p & diff(
exp_R-(exp_R*f),p)=exp_R.p+exp_R.(-p) & diff(exp_R+(exp_R*f),p)=exp_R.p-exp_R.(
-p)
proof
let f be PartFunc of REAL,REAL;
A1: p is Real & exp_R is_differentiable_in p by SIN_COS:65;
assume
A2: f = compreal;
then
A3: exp_R*f is_differentiable_in p by Lm13;
then
A4: diff(exp_R+(exp_R*f),p) =diff(exp_R,p)+diff((exp_R*f),p) by A1,FDIFF_1:13
.=exp_R.p+diff((exp_R*f),p) by SIN_COS:65
.=exp_R.p+ (-1)*exp_R.(f.p) by A2,Lm13
.=exp_R.p+ (-1)*exp_R.((-1)*p) by A2,Lm10
.=exp_R.p-exp_R.(-p);
diff(exp_R-(exp_R*f),p) =diff(exp_R,p)-diff((exp_R*f),p) by A1,A3,FDIFF_1:14
.=exp_R.p-diff((exp_R*f),p) by SIN_COS:65
.=exp_R.p- (-1)*exp_R.(f.p) by A2,Lm13
.=exp_R.p- (-1)*exp_R.((-1)*p) by A2,Lm10
.=exp_R.p+exp_R.(-p);
hence thesis by A1,A3,A4,FDIFF_1:13,14;
end;
Lm16: for f being PartFunc of REAL,REAL st f = compreal holds (1/2)(#)(exp_R-
exp_R*f) is_differentiable_in p & diff(((1/2)(#)(exp_R-exp_R*f)),p) = (1/2)*
diff((exp_R-(exp_R*f)),p)
proof
let f be PartFunc of REAL,REAL;
assume f = compreal;
then p is Real & (exp_R-exp_R*f) is_differentiable_in p by Lm15;
hence thesis by FDIFF_1:15;
end;
Lm17: for ff being PartFunc of REAL,REAL st ff = compreal holds sinh.p=((1/2)
(#)(exp_R-exp_R*ff)).p
proof
A1: p in REAL by XREAL_0:def 1;
let ff be PartFunc of REAL,REAL such that
A2: ff = compreal;
A3: dom (exp_R - exp_R*ff) = dom exp_R /\ dom (exp_R*ff) & dom (exp_R*ff) =
REAL by A2,FUNCT_2:def 1,VALUED_1:12;
A4: dom((1/2)(#)(exp_R-exp_R*ff))=REAL by A2,FUNCT_2:def 1;
sinh.p = (exp_R.p - exp_R.(-p))/2 by Def1
.=(1/2)*(exp_R.p - exp_R.((-1)*p))
.=(1/2)*(exp_R.p - (exp_R*ff).p) by A2,Lm14
.=(1/2)*((exp_R - exp_R*ff).p) by A1,A3,SIN_COS:47,VALUED_1:13
.=((1/2)(#)(exp_R-exp_R*ff)).p by A1,A4,VALUED_1:def 5;
hence thesis;
end;
Lm18: for ff being PartFunc of REAL,REAL st ff = compreal holds sinh = (1/2)
(#)(exp_R-exp_R*ff)
proof
let ff be PartFunc of REAL,REAL;
assume ff = compreal;
then
A1: REAL=dom((1/2)(#)(exp_R-exp_R*ff)) & for p being Element of REAL st p in
REAL holds sinh.p=((1/2)(#)(exp_R-exp_R*ff)).p by Lm17,FUNCT_2:def 1;
REAL=dom(sinh) by FUNCT_2:def 1;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th31:
sinh is_differentiable_in p & diff(sinh,p)=cosh.p
proof
set ff = compreal;
A1: sinh = (1/2)(#)(exp_R-exp_R*ff) by Lm18;
diff(sinh,p) =diff( ((1/2)(#)(exp_R-exp_R*ff)),p ) by Lm18
.=(1/2)*diff((exp_R-(exp_R*ff)),p) by Lm16
.=(1/2)*( exp_R.p+exp_R.(-p) ) by Lm15
.=( exp_R.p+exp_R.(-p) )/2
.=cosh.p by Def3;
hence thesis by A1,Lm16;
end;
Lm19: for ff being PartFunc of REAL,REAL st ff = compreal holds (1/2)(#)(exp_R
+exp_R*ff) is_differentiable_in p & diff(((1/2)(#)(exp_R+exp_R*ff)),p) = (1/2)*
diff((exp_R+(exp_R*ff)),p)
proof
let ff be PartFunc of REAL,REAL;
assume ff = compreal;
then p is Real & (exp_R+exp_R*ff) is_differentiable_in p by Lm15;
hence thesis by FDIFF_1:15;
end;
Lm20: for ff being PartFunc of REAL,REAL st ff = compreal holds cosh.p=((1/2)
(#)(exp_R+exp_R*ff)).p
proof
A1: p in REAL by XREAL_0:def 1;
let ff be PartFunc of REAL,REAL such that
A2: ff = compreal;
A3: dom (exp_R + exp_R*ff) = dom exp_R /\ dom (exp_R*ff) & dom (exp_R*ff) =
REAL by A2,FUNCT_2:def 1,VALUED_1:def 1;
A4: dom((1/2)(#)(exp_R+exp_R*ff))=REAL by A2,FUNCT_2:def 1;
cosh.p =(exp_R.p + exp_R.(-p))/2 by Def3
.=(1/2)*(exp_R.p + exp_R.((-1)*p))
.=(1/2)*(exp_R.p + (exp_R*ff).p) by A2,Lm14
.=(1/2)*((exp_R + exp_R*ff).p) by A1,A3,SIN_COS:47,VALUED_1:def 1
.=((1/2)(#)(exp_R+exp_R*ff)).p by A1,A4,VALUED_1:def 5;
hence thesis;
end;
Lm21: for ff being PartFunc of REAL,REAL st ff = compreal holds cosh = (1/2)
(#)(exp_R+exp_R*ff)
proof
let ff be PartFunc of REAL,REAL;
assume ff = compreal;
then
A1: REAL=dom((1/2)(#)(exp_R+exp_R*ff)) & for p being Element of REAL st p in
REAL holds cosh.p=((1/2)(#)(exp_R+exp_R*ff)).p by Lm20,FUNCT_2:def 1;
REAL=dom(cosh) by FUNCT_2:def 1;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th32:
cosh is_differentiable_in p & diff(cosh,p)=sinh.p
proof
reconsider ff = compreal as PartFunc of REAL,REAL;
A1: cosh = (1/2)(#)(exp_R+exp_R*ff) by Lm21;
diff(cosh,p) =diff( ((1/2)(#)(exp_R+exp_R*ff)),p ) by Lm21
.=(1/2)*diff((exp_R+(exp_R*ff)),p) by Lm19
.=(1/2)*( exp_R.p-exp_R.(-p) ) by Lm15
.=( exp_R.p-exp_R.(-p) )/2
.=sinh.p by Def1;
hence thesis by A1,Lm19;
end;
Lm22: sinh/cosh is_differentiable_in p & diff(sinh/cosh,p) = 1/(cosh.p)^2
proof
A1: p is Real & cosh.p<>0 by Th15;
A2: sinh is_differentiable_in p & cosh is_differentiable_in p by Th31,Th32;
then
diff(sinh/cosh,p) =(diff(sinh,p) * cosh.p - diff(cosh,p)*sinh.p)/(cosh.p
)^2 by A1,FDIFF_2:14
.=((cosh.p)*(cosh.p) - diff(cosh,p) * sinh.p)/(cosh.p)^2 by Th31
.=( (cosh.p)^2 - (sinh.p)*(sinh.p) )/(cosh.p)^2 by Th32
.=1/(cosh.p)^2 by Th14;
hence thesis by A1,A2,FDIFF_2:14;
end;
Lm23: tanh=sinh/cosh
proof
not 0 in rng(cosh)
proof
assume 0 in rng(cosh);
then ex p be Element of REAL st p in dom(cosh) & 0=cosh.p by PARTFUN1:3;
hence contradiction by Th15;
end;
then
A1: dom (sinh/cosh) = dom sinh /\ (dom cosh \ cosh"{0}) & cosh"{0}={} by
FUNCT_1:72,RFUNCT_1:def 1;
for p being Element of REAL st p in REAL holds tanh.p=(sinh/cosh).p
proof
let p;
p in REAL by XREAL_0:def 1;
then (sinh/cosh).p =sinh.p*(cosh.p)" by A1,Th30,RFUNCT_1:def 1
.=(sinh.p)/(cosh.p) by XCMPLX_0:def 9
.=tanh.p by Th17;
hence thesis;
end;
hence thesis by A1,Th30,PARTFUN1:5;
end;
theorem
tanh is_differentiable_in p & diff(tanh,p)=1/(cosh.p)^2 by Lm22,Lm23;
theorem Th34:
sinh is_differentiable_on REAL & diff(sinh,p)=cosh.p
proof
A1: [#]REAL is open Subset of REAL & REAL c= dom(sinh) by FUNCT_2:def 1;
for p st p in REAL holds sinh is_differentiable_in p by Th31;
hence thesis by A1,Th31,FDIFF_1:9;
end;
theorem Th35:
cosh is_differentiable_on REAL & diff(cosh,p)=sinh.p
proof
A1: [#]REAL is open Subset of REAL & REAL c=dom cosh by FUNCT_2:def 1;
for r st r in REAL holds cosh is_differentiable_in r by Th32;
hence thesis by A1,Th32,FDIFF_1:9;
end;
theorem Th36:
tanh is_differentiable_on REAL & diff(tanh,p)=1/(cosh.p)^2
proof
[#]REAL is open Subset of REAL & for p st p in REAL holds tanh
is_differentiable_in p by Lm22,Lm23;
hence thesis by Lm22,Lm23,Th30,FDIFF_1:9;
end;
Lm24: exp_R.p + exp_R.-p >= 2
proof
A1: exp_R.p >= 0 & exp_R.-p>= 0 by SIN_COS:54;
2*sqrt((exp_R.p) * (exp_R.-p)) =2*sqrt(exp_R.(p+-p)) by Th12
.=2*1 by SIN_COS:51,def 23,SQUARE_1:18;
hence thesis by A1,Th1;
end;
theorem
cosh.p >= 1
proof
(exp_R.p + exp_R.-p)/2 >= 2/2 by Lm24,XREAL_1:72;
hence thesis by Def3;
end;
theorem
sinh is_continuous_in p by Th31,FDIFF_1:24;
theorem
cosh is_continuous_in p by Th32,FDIFF_1:24;
theorem
tanh is_continuous_in p by Lm22,Lm23,FDIFF_1:24;
theorem
sinh|REAL is continuous by Th34,FDIFF_1:25;
theorem
cosh|REAL is continuous by Th35,FDIFF_1:25;
theorem
tanh|REAL is continuous by Th36,FDIFF_1:25;
theorem
tanh.p<1 & tanh.p>-1
proof
A1: exp_R.p > 0 & exp_R.(-p) > 0 by SIN_COS:54;
thus tanh.p<1
proof
assume tanh.p>=1;
then
A2: (exp_R.p - exp_R.(-p))/(exp_R.p + exp_R.(-p))>=1 by Def5;
exp_R.p > 0 & exp_R.(-p) > 0 by SIN_COS:54;
then
A3: (exp_R.p - exp_R.(-p))/(exp_R.p + exp_R.(-p))*(exp_R.p + exp_R.(-p)) =
exp_R.p - exp_R.(-p) by XCMPLX_1:87;
(exp_R.p + exp_R.-p) >= 2 by Lm24;
then
(exp_R.p - exp_R.(-p))/(exp_R.p + exp_R.(-p))*(exp_R.p + exp_R.(-p ))
>=1*(exp_R.p + exp_R.(-p)) by A2,XREAL_1:64;
then (exp_R.p - exp_R.(-p))-exp_R.p >= (exp_R.p + exp_R.(-p))-exp_R.p by A3
,XREAL_1:9;
then
A4: -exp_R.(-p)+exp_R.(-p) >= exp_R.(-p)+exp_R.(-p) by XREAL_1:6;
exp_R.(-p) > 0 by SIN_COS:54;
hence contradiction by A4;
end;
assume tanh.p<=-1;
then
A5: (exp_R.p - exp_R.(-p))/(exp_R.p + exp_R.(-p))<=-1 by Def5;
(exp_R.p + exp_R.-p) >= 2 by Lm24;
then
(exp_R.p - exp_R.(-p))/(exp_R.p + exp_R.(-p))*(exp_R.p + exp_R.(-p)) <=
(-1)*(exp_R.p + exp_R.(-p)) by A5,XREAL_1:64;
then exp_R.p - exp_R.(-p)<=-(exp_R.p + exp_R.(-p)) by A1,XCMPLX_1:87;
then
A6: exp_R.p - exp_R.(-p)+exp_R.(-p) <=-exp_R.p + -exp_R.(-p)+exp_R.(-p) by
XREAL_1:6;
exp_R.p > 0 by SIN_COS:54;
hence contradiction by A6;
end;