:: Several Integrability Formulas of Special Functions
:: by Cuiying Peng , Fuguo Ge and Xiquan Liang
::
:: Received August 28, 2007
:: Copyright (c) 2007-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, PARTFUN1, INTEGRA1, SUBSET_1, REAL_1, RCOMP_1, SIN_COS,
ARYTM_3, XXREAL_0, CARD_1, XXREAL_1, RELAT_1, ARYTM_1, FUNCT_1, SQUARE_1,
COMPLEX1, TARSKI, SIN_COS6, SIN_COS2, POWER, VALUED_1, FDIFF_1, SEQ_1,
FUNCT_2, SEQ_2, ORDINAL2, FUNCOP_1, FUNCT_3, XBOOLE_0, SEQ_4, INTEGRA5,
MEASURE7, REALSET1, XXREAL_2, INTEGRA8, MEASURE5, VALUED_0, NAT_1;
notations TARSKI, XBOOLE_0, ORDINAL1, FUNCT_1, FUNCOP_1, INTEGRA1, RFUNCT_1,
RELAT_1, INTEGRA5, VALUED_0, SIN_COS, SUBSET_1, PARTFUN1, RCOMP_1,
NUMBERS, FDIFF_1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, FCONT_1,
COMSEQ_2, SEQ_2, SEQ_4, SIN_COS2, NAT_1, POWER, SQUARE_1, VALUED_1,
SEQ_1, SIN_COS6, FUNCT_2, MEASURE5;
constructors BINOP_2, FINSEQOP, INTEGRA5, SIN_COS, COMSEQ_3, PARTFUN1, REAL_1,
SQUARE_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1, SIN_COS2, NAT_1,
SIN_COS6, POWER, XXREAL_2, SEQ_4, RELSET_1, SEQ_2, INTEGRA1, COMSEQ_2,
NUMBERS;
registrations RELSET_1, MEMBERED, RCOMP_1, FDIFF_1, INT_1, XXREAL_0, XREAL_0,
NUMBERS, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FCONT_1,
SIN_COS, FCONT_3, MEASURE5, ORDINAL1, SQUARE_1, SIN_COS6;
requirements ARITHM, SUBSET, NUMERALS, BOOLE, REAL;
equalities SIN_COS, INTEGRA5, VALUED_1, SQUARE_1, SUBSET_1;
expansions INTEGRA5;
theorems PARTFUN1, INTEGRA1, FUNCT_1, SEQ_1, FDIFF_1, INTEGRA4, XBOOLE_0,
XBOOLE_1, FUNCOP_1, INTEGRA5, FUNCT_3, SIN_COS, SIN_COS2, FCONT_1,
RFUNCT_1, SEQ_2, RFUNCT_2, IRRAT_1, TAYLOR_1, XCMPLX_1, XREAL_1,
SQUARE_1, FDIFF_7, SIN_COS6, FDIFF_2, SIN_COS5, COMPLEX1, ABSVALUE,
INTEGRA2, FUNCT_2, VALUED_0, VALUED_1, XXREAL_1, XXREAL_2, RELAT_1,
FDIFF_8, XREAL_0;
schemes NAT_1;
begin :: Preliminaries
reserve f,f1,f2,g for PartFunc of REAL,REAL;
reserve A for non empty closed_interval Subset of REAL;
reserve p,r,x,x0 for Real;
reserve n for Element of NAT;
reserve Z for open Subset of REAL;
Lm1: sin(PI/4) > 0
proof
PI/4 < PI/1 by XREAL_1:76;
then
A1: PI/4 < PI+2*PI*0;
0/4 < PI/4 by XREAL_1:74;
hence thesis by A1,SIN_COS6:11;
end;
Lm2: sin(-PI/4) < 0
proof
0/4 < PI/4 by XREAL_1:74;
then
A1: (PI/4)* (-1) < 0*(-1) by XREAL_1:69;
PI/4 < PI/1 by XREAL_1:76;
then
A2: PI*(-1) < (PI/4)*(-1) by XREAL_1:69;
PI+2*PI*(-1) < r & r < 2*PI+2*PI*(-1) implies sin r < 0 by SIN_COS6:12;
hence thesis by A1,A2;
end;
theorem Th1:
sin(x + 2 * n * PI) = sin x
proof
sin.x = sin.(2*PI*n + x) by SIN_COS2:10;
hence thesis;
end;
theorem Th2:
sin(x + (2*n+1)*PI) = -sin x
proof
defpred X[Nat] means sin(x + (2*$1+1)* PI) = -sin x;
A1: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat;
assume
A2: sin(x + (2*n+1)*PI) = -sin x;
sin(x + (2*(n+1)+1)*PI)=sin((x + (2*n+1)*PI)+2*PI)
.=sin(x + (2*n+1)*PI)*cos(2*PI) + cos(x + (2*n+1)*PI)*sin(2*PI) by
SIN_COS:75
.= -sin(x) by A2,SIN_COS:77;
hence thesis;
end;
A3: X[0] by SIN_COS:79;
for n being Nat holds X[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th3:
cos(x + 2 * n* PI) = cos x
proof
cos.x = cos.(x+2*PI*n) by SIN_COS6:10;
hence thesis;
end;
theorem Th4:
cos(x + (2*n+1)*PI) = -cos x
proof
defpred X[Nat] means cos(x + (2*$1+1)* PI) = -cos x;
A1: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat;
assume
A2: cos(x + (2*n+1)*PI) = -cos x;
cos(x + (2*(n+1)+1)*PI)=cos((x + (2*n+1)*PI)+2*PI)
.= cos(x + (2*n+1)*PI)*cos(2*PI) - sin(x + (2*n+1)*PI)*sin(2*PI) by
SIN_COS:75
.= -cos(x) by A2,SIN_COS:77;
hence thesis;
end;
A3: X[0] by SIN_COS:79;
for n being Nat holds X[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th5:
sin(x/2) >= 0 implies sin(x/2)=sqrt((1-cos(x))/2)
proof
assume
A1: sin(x/2) >= 0;
sqrt((1-cos(x))/2)=sqrt((1-cos(2*(x/2)))/2)
.=sqrt((1-(1-2*(sin(x/2))^2))/2) by SIN_COS5:7
.=|.sin(x/2).| by COMPLEX1:72
.=sin(x/2) by A1,ABSVALUE:def 1;
hence thesis;
end;
theorem Th6:
sin(x/2) < 0 implies sin(x/2)=-sqrt((1-cos(x))/2)
proof
assume
A1: sin(x/2) < 0;
sqrt((1-cos(x))/2)=sqrt((1-cos(2*(x/2)))/2)
.=sqrt((1-(1-2*(sin(x/2))^2))/2) by SIN_COS5:7
.=|.sin(x/2).| by COMPLEX1:72
.=-sin(x/2) by A1,ABSVALUE:def 1;
hence thesis;
end;
theorem Th7:
sin(PI/4) = sqrt(2)/2
proof
A1: sqrt 2 > 0 by SQUARE_1:25;
sin((PI/2)/2)=sqrt((1-cos(PI/2))/2) by Lm1,Th5;
then sin(PI/4) = 1 /sqrt 2 by SIN_COS:77,SQUARE_1:18,30
.= (sqrt(2) * 1)/(sqrt(2)*sqrt(2)) by A1,XCMPLX_1:91
.= (sqrt(2) * 1)/(sqrt(2))^2;
hence thesis by SQUARE_1:def 2;
end;
theorem Th8:
sin(-PI/4) = -sqrt(2)/2
proof
A1: cos(-PI/2) = sin(PI/2-(-PI/2))by SIN_COS:79
.= 0 by SIN_COS:77;
A2: sqrt 2 > 0 by SQUARE_1:25;
sin((-PI/2)/2)=-sqrt((1-cos(-PI/2))/2) by Lm2,Th6;
then sin(-PI/4) = -1 /sqrt 2 by A1,SQUARE_1:18,30
.= -(sqrt(2) * 1)/(sqrt(2)*sqrt(2)) by A2,XCMPLX_1:91
.= -(sqrt(2) * 1)/(sqrt(2))^2;
hence thesis by SQUARE_1:def 2;
end;
theorem Th9:
[.-sqrt 2/2,sqrt 2/2.] c= ].-1,1.[
proof
A1: sqrt 2 > 0 by SQUARE_1:25;
sqrt 2 < sqrt 4 by SQUARE_1:27;
then
A2: sqrt 2/2 < 2/2 by SQUARE_1:20,XREAL_1:74;
then sqrt 2/2*(-1) > 1*(-1) by XREAL_1:69;
then
A3: -sqrt 2/2 in ].-1,1.[ by A1,XXREAL_1:4;
sqrt 2/2 > 0 by A1,XREAL_1:139;
then sqrt 2/2 in ].-1,1.[ by A2,XXREAL_1:4;
hence thesis by A3,XXREAL_2:def 12;
end;
theorem Th10:
arcsin (sqrt 2/2) = PI/4
proof
PI/4 < PI/2 by XREAL_1:76;
hence thesis by Th7,SIN_COS6:69;
end;
theorem Th11:
arcsin (-sqrt 2/2) = -PI/4
proof
PI/4 < PI/2 by XREAL_1:76;
then (PI/4)*(-1) > (PI/2)*(-1) by XREAL_1:69;
hence thesis by Th8,SIN_COS6:69;
end;
theorem Th12:
cos(x/2) >=0 implies cos(x/2)=sqrt((1+cos x)/2)
proof
assume
A1: cos(x/2) >=0;
sqrt((1+cos(x))/2)=sqrt((1+cos(2*(x/2)))/2)
.=sqrt((1+(2*(cos(x/2))^2-1))/2) by SIN_COS5:7
.=|.cos(x/2).| by COMPLEX1:72
.= cos(x/2) by A1,ABSVALUE:def 1;
hence thesis;
end;
Lm3: cos(PI/4) > 0
proof
0/2 < PI/2 by XREAL_1:74;
then (PI/2)*(-1) < 0*(-1) by XREAL_1:69;
then
A1: -PI/2 + 2*PI*0 < PI/4;
PI/4 < PI/2+2*PI*0 by XREAL_1:76;
hence thesis by A1,SIN_COS6:13;
end;
theorem Th13:
cos (PI/4) = sqrt 2/2
proof
A1: sqrt 2 > 0 by SQUARE_1:25;
cos ((PI/2)/2) = sqrt((1+cos(PI/2))/2) by Lm3,Th12
.= 1 /sqrt 2 by SIN_COS:77,SQUARE_1:18,30
.= (sqrt(2) * 1)/(sqrt(2)*sqrt(2)) by A1,XCMPLX_1:91
.= (sqrt(2) * 1)/(sqrt(2))^2;
hence thesis by SQUARE_1:def 2;
end;
theorem Th14:
cos(3*PI/4) = -sqrt 2 /2
proof
cos(3*PI/4) = cos(PI/2 + PI/4) .= -sqrt 2/2 by Th7,SIN_COS:79;
hence thesis;
end;
theorem Th15:
arccos (sqrt 2 /2) = PI/4
proof
PI/4 < PI/1 by XREAL_1:76;
hence thesis by Th13,SIN_COS6:92;
end;
theorem Th16:
arccos (-sqrt 2 /2) = 3*PI/4
proof
(3/4)*PI < 1*PI by XREAL_1:68;
hence thesis by Th14,SIN_COS6:92;
end;
theorem Th17:
sinh.1 = (number_e^2 - 1)/(2*number_e)
proof
sinh.1=(number_e - exp_R(-1))/2 by IRRAT_1:def 7,SIN_COS2:def 1
.=(number_e/1 - 1/number_e)/2 by IRRAT_1:def 7,TAYLOR_1:4
.=((number_e * number_e)/(1*number_e) - 1/number_e)/2 by TAYLOR_1:11
,XCMPLX_1:91
.=((number_e)^2/number_e - 1/number_e)/2
.=(number_e^2 - 1)/number_e/2 by XCMPLX_1:120
.=(number_e^2 - 1)/(2*number_e) by XCMPLX_1:78;
hence thesis;
end;
theorem Th18:
cosh.0 = 1
proof
cosh.0 = (exp_R.0+exp_R.(-0))/2 by SIN_COS2:def 3
.= 1 by SIN_COS:51;
hence thesis;
end;
theorem Th19:
cosh.1 = (number_e^2 + 1)/(2*number_e)
proof
cosh.1=(number_e + exp_R(-1))/2 by IRRAT_1:def 7,SIN_COS2:def 3
.=(number_e/1 + 1/number_e)/2 by IRRAT_1:def 7,TAYLOR_1:4
.=((number_e * number_e)/(1*number_e) + 1/number_e)/2 by TAYLOR_1:11
,XCMPLX_1:91
.=((number_e)^2/number_e + 1/number_e)/2
.=(number_e^2 + 1)/number_e/2 by XCMPLX_1:62
.=(number_e^2 + 1)/(2*number_e) by XCMPLX_1:78;
hence thesis;
end;
Lm4: (-f1)(#)(-f2) = f1(#)f2
proof
(-f1)(#)(-f2) = (-1)(#)(f1(#)(-f2)) by RFUNCT_1:12
.= f1(#)(-(-f2)) by RFUNCT_1:13;
hence thesis;
end;
theorem Th20:
for L1 being LinearFunc holds -L1 is LinearFunc
proof
let L1 be LinearFunc;
consider g1 being Real such that
A1: for p holds L1.p = g1*p by FDIFF_1:def 3;
A2: L1 is total by FDIFF_1:def 3;
now
let p;
reconsider pp=p as Element of REAL by XREAL_0:def 1;
thus (-L1).p = -L1.pp by A2,RFUNCT_1:58
.= -g1*p by A1
.= (-g1)*p;
end;
hence thesis by A2,FDIFF_1:def 3;
end;
theorem Th21:
for R1 being RestFunc holds -R1 is RestFunc
proof
let R1 be RestFunc;
A1: R1 is total by FDIFF_1:def 2;
then
A2: dom R1 = REAL by PARTFUN1:def 2;
A3: for h being 0-convergent non-zero Real_Sequence
holds -(R1/*h) = (-R1)/*h
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= dom R1 by A2,VALUED_0:def 3;
hence thesis by RFUNCT_2:10;
end;
now
let h be 0-convergent non-zero Real_Sequence;
A4: (h")(#)(R1/*h) is convergent by FDIFF_1:def 2;
A5: (h")(#)((-R1)/*h) = (h")(#)(-(R1/*h)) by A3
.= - ((h")(#)(R1/*h)) by SEQ_1:19;
hence (h")(#)((-R1)/*h) is convergent by A4,SEQ_2:9;
A6: lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
thus lim ((h")(#)((-R1)/*h)) = - (lim ((h")(#)(R1/*h))) by A4,A5,SEQ_2:10
.= 0 by A6;
end;
hence thesis by A1,FDIFF_1:def 2;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th22:
for f1,x0 st f1 is_differentiable_in x0 holds -f1
is_differentiable_in x0 & diff(-f1,x0)=-diff(f1,x0)
proof
let f1,x0;
assume
A1: f1 is_differentiable_in x0;
then consider N1 be Neighbourhood of x0 such that
A2: N1 c= dom f1 and
A3: ex L being LinearFunc,R being RestFunc st for x st x in N1 holds f1.x - f1.
x0 = L.(x-x0) + R.(x-x0) by FDIFF_1:def 4;
consider L1 being LinearFunc,R1 being RestFunc such that
A4: for x st x in N1 holds f1.x - f1.x0 = L1.(x-x0) + R1.(x-x0) by A3;
reconsider R=-R1 as RestFunc by Th21;
reconsider L=-L1 as LinearFunc by Th20;
A5: L1 is total by FDIFF_1:def 3;
consider N be Neighbourhood of x0 such that
A6: N c= N1;
A7: R1 is total by FDIFF_1:def 2;
A8: now
let x;
assume
A9: x in N;
reconsider xx=x, xx0=x0 as Element of REAL by XREAL_0:def 1;
thus (-f1).x - (-f1).x0 = -(f1.x) - (-f1).x0 by VALUED_1:8
.= -(f1.x) - -(f1.x0) by VALUED_1:8
.= -((f1.x) -(f1.x0))
.= -(L1.(x-x0) + R1.(x-x0)) by A4,A6,A9
.= -L1.(x-x0) + -R1.(x-x0)
.= L.(xx-xx0)+-R1.(x-x0) by A5,RFUNCT_1:58
.= L.(x-x0)+R.(x-x0) by A7,RFUNCT_1:58;
end;
N c= dom f1 by A2,A6,XBOOLE_1:1;
then
A10: N c= dom -f1 by VALUED_1:8;
hence -f1 is_differentiable_in x0 by A8,FDIFF_1:def 4;
hence diff(-f1,x0)=L.1 by A10,A8,FDIFF_1:def 5
.=-L1.jj by A5,RFUNCT_1:58
.=-diff(f1,x0) by A1,A2,A4,FDIFF_1:def 5;
end;
theorem Th23:
for f1,Z st Z c= dom (-f1) & f1 is_differentiable_on Z holds -f1
is_differentiable_on Z & for x st x in Z holds ((-f1)`|Z).x = -diff(f1,x)
proof
let f1,Z;
assume that
A1: Z c= dom (-f1) and
A2: f1 is_differentiable_on Z;
now
let x0;
assume x0 in Z;
then f1 is_differentiable_in x0 by A2,FDIFF_1:9;
hence -f1 is_differentiable_in x0 by Th22;
end;
hence
A3: -f1 is_differentiable_on Z by A1,FDIFF_1:9;
now
let x;
assume
A4: x in Z; then
A5: f1 is_differentiable_in x by A2,FDIFF_1:9;
thus ((-f1)`|Z).x = diff((-f1),x) by A3,A4,FDIFF_1:def 7
.= -diff(f1,x) by A5,Th22;
end;
hence thesis;
end;
theorem
-sin is_differentiable_on REAL
proof
dom (-sin) = [#]REAL by FUNCT_2:def 1;
hence thesis by Th23,SIN_COS:68;
end;
theorem Th25:
-cos is_differentiable_in x & diff(-cos,x) = sin.x
proof
A1: cos is_differentiable_in x by SIN_COS:63;
then diff(-cos,x) = -diff(cos,x) by Th22
.= - -sin.x by SIN_COS:63;
hence thesis by A1,Th22;
end;
theorem Th26:
-cos is_differentiable_on REAL & for x st x in REAL holds diff(- cos,x)=sin.x
proof
dom (-cos) = [#]REAL by FUNCT_2:def 1;
hence thesis by Th23,Th25,SIN_COS:67;
end;
theorem Th27:
sin`|REAL = cos
proof
for x st x in REAL holds diff(sin,x)=cos.x by SIN_COS:68;
hence thesis by FDIFF_1:def 7,SIN_COS:24,68;
end;
theorem Th28:
cos`|REAL = -sin
proof
A1: for x being Element of REAL st x in dom (cos`|REAL) holds (cos`|REAL).x
= (-sin).x
proof
let x be Element of REAL;
assume x in dom (cos`|REAL);
(cos`|REAL).x = diff(cos,x) by FDIFF_1:def 7,SIN_COS:67
.= -sin.x by SIN_COS:63;
hence thesis by VALUED_1:8;
end;
dom (-sin) = REAL by FUNCT_2:def 1;
then dom (cos`|REAL) = dom (-sin) by FDIFF_1:def 7,SIN_COS:67;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th29:
(-cos)`|REAL = sin by Th26,FDIFF_1:def 7,SIN_COS:24;
theorem Th30:
sinh`|REAL = cosh
proof
for x st x in REAL holds diff(sinh,x)=cosh.x by SIN_COS2:34;
hence thesis by FDIFF_1:def 7,SIN_COS2:30,34;
end;
theorem Th31:
cosh`|REAL = sinh
proof
for x st x in REAL holds diff(cosh,x)=sinh.x by SIN_COS2:35;
hence thesis by FDIFF_1:def 7,SIN_COS2:30,35;
end;
theorem Th32:
exp_R`|REAL = exp_R
proof
for x st x in REAL holds diff(exp_R,x)=exp_R.x by SIN_COS:66;
hence thesis by FDIFF_1:def 7,SIN_COS:47,66;
end;
theorem Th33:
Z c= dom tan implies tan is_differentiable_on Z & for x st x in Z holds
((tan)`|Z).x = 1/(cos.x)^2
proof
assume that
A1: Z c= dom tan;
A2: for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z; then
x in dom tan by A1; then
A3: cos.x <> 0 by FDIFF_8:1;
sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
hence thesis by A3,FDIFF_2:14;
end; then
A4: tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan)`|Z).x = 1/(cos.x)^2
proof
let x;
A5: sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
assume
A6: x in Z; then
x in dom tan by A1;
then cos.x <> 0 by FDIFF_8:1;
then
diff (tan,x) = (diff(sin,x) * cos.x - diff(cos,x)*sin.x)/(cos.x)^2 by A5,
FDIFF_2:14
.=((cos.x)*cos.x - diff(cos,x)*sin.x)/(cos.x)^2 by SIN_COS:64
.=((cos.x)*(cos.x)-(-sin.x)*(sin.x))/(cos.x)^2 by SIN_COS:63
.=((cos.x)*(cos.x) + (sin.x)*(sin.x))/(cos.x)^2
.=1/(cos.x)^2 by SIN_COS:28;
hence thesis by A4,A6,FDIFF_1:def 7;
end;
hence thesis by A1,A2,FDIFF_1:9;
end;
theorem Th34:
Z c= dom cot implies cot is_differentiable_on Z &
for x st x in Z holds (cot`|Z).x = - 1/(sin.x)^2
proof
assume that
A1: Z c= dom cot;
A2: for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z; then
x in dom cot by A1; then
A3: sin.x <> 0 by FDIFF_8:2;
sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
hence thesis by A3,FDIFF_2:14;
end;
then
A4: cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (cot`|Z).x = -1/(sin.x)^2
proof
let x;
A5: sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
assume
A6: x in Z; then
x in dom cot by A1;
then sin.x <> 0 by FDIFF_8:2;
then diff (cot,x)=(diff(cos,x) * sin.x - diff(sin,x)*cos.x)/(sin.x)^2 by A5
,FDIFF_2:14
.=((-sin.x)*sin.x - diff(sin,x)*cos.x)/(sin.x)^2 by SIN_COS:63
.=(-(sin.x)*(sin.x)-(cos.x)*(cos.x))/(sin.x)^2 by SIN_COS:64
.=(-((sin.x)*(sin.x) + (cos.x)*(cos.x) ))/(sin.x)^2
.=(-((sin.x)*(sin.x) + (cos.x)^2 ))/(sin.x)^2
.=(-((sin.x)^2 + (cos.x)^2 ))/(sin.x)^2
.=-((cos.x)^2 + (sin.x)^2)/(sin.x)^2by XCMPLX_1:187
.=-1/(sin.x)^2 by SIN_COS:28;
hence thesis by A4,A6,FDIFF_1:def 7;
end;
hence thesis by A1,A2,FDIFF_1:9;
end;
theorem
for r being Real holds rng (REAL --> r) c= REAL
proof
let r be Real;
rng (REAL --> r) c= {r} by FUNCOP_1:13;
hence thesis by XBOOLE_1:1;
end;
definition
let r be Real;
func Cst(r) -> Function of REAL,REAL equals
REAL --> r;
coherence
proof
reconsider r as Element of REAL by XREAL_0:def 1;
REAL --> r is Function of REAL, REAL;
hence thesis;
end;
end;
theorem Th36:
for a,b being Real, A being non empty closed_interval Subset of REAL
holds chi(A,A)=(Cst(1))|A
proof
let a,b be Real, A be non empty closed_interval Subset of REAL;
dom ((Cst(1))|A) = A & for x being object st x in A holds (x in A implies (
(Cst(1))|A).x = 1) & (not x in A implies ((Cst(1))|A).x = 0)
proof
A1: dom (Cst(1))=REAL & dom ((Cst(1))|A)=dom (Cst(1)) /\ A by FUNCOP_1:13
,RELAT_1:61;
hence dom ((Cst(1))|A)=A by XBOOLE_1:28;
let x be object;
assume
A2: x in A;
then x in dom ((Cst(1))|A) by A1,XBOOLE_0:def 4;
then ((Cst 1)|A).x = (REAL-->1).x by FUNCT_1:47
.= 1 by A2,FUNCOP_1:7;
hence thesis by A2;
end;
hence thesis by FUNCT_3:def 3;
end;
theorem Th37:
for a,b being Real,
A being non empty closed_interval Subset of REAL st A=
[.a,b.] holds upper_bound A=b & lower_bound A=a
proof
let a,b be Real, A be non empty closed_interval Subset of REAL;
A1: A=[. lower_bound A, upper_bound A .] by INTEGRA1:4;
assume A=[.a,b.];
hence thesis by A1,INTEGRA1:5;
end;
begin :: Integrability formulas of special functions
theorem
for a,b being Real st a<=b holds integral(Cst(1),a,b)=b-a
proof
let a,b be Real;
assume a<=b;
then [.a,b.]=[' a,b '] by INTEGRA5:def 3;
then reconsider A=[.a,b.] as non empty closed_interval Subset of REAL;
upper_bound A=b & lower_bound A=a by Th37;
then
A1: vol(A)=b-a by INTEGRA1:def 5;
integral(Cst(1),a,b)=integral(Cst(1),A) & (Cst(1))||A = chi(A,A) by Th36,
INTEGRA5:19;
hence thesis by A1,INTEGRA4:2;
end;
Lm5: dom sin = REAL by FUNCT_2:def 1;
Lm6: dom cos = REAL by FUNCT_2:def 1;
Lm7: dom -sin = REAL by FUNCT_2:def 1;
Lm8: dom exp_R = REAL by FUNCT_2:def 1;
Lm9: dom sinh = REAL by FUNCT_2:def 1;
Lm10: dom cosh = REAL by FUNCT_2:def 1;
Lm11: cos is_integrable_on A & cos|A is bounded
proof
cos|A is continuous;
hence thesis by Lm6,INTEGRA5:10,11;
end;
theorem Th39:
integral(cos,A) = sin.(upper_bound A)-sin.(lower_bound A)
proof
A1: for x being Element of REAL st x in dom (sin`|REAL) holds (sin`|REAL).x
= cos.x
proof
let x be Element of REAL;
assume x in dom (sin`|REAL);
(sin`|REAL).x = diff(sin,x) by FDIFF_1:def 7,SIN_COS:68;
hence thesis by SIN_COS:64;
end;
A2: cos is_integrable_on A & cos|A is bounded by Lm11;
dom (sin`|REAL) = dom cos by FDIFF_1:def 7,SIN_COS:24,68;
then sin`|REAL = cos by A1,PARTFUN1:5;
hence thesis by A2,INTEGRA5:13,SIN_COS:68;
end;
theorem
A = [.0,PI/2.] implies integral(cos,A) = 1
proof
assume A=[.0,PI/2.];
then upper_bound A=PI/2 & lower_bound A=0 by Th37;
then integral(cos,A) = 1 - sin.0 by Th39,SIN_COS:77
.= 1 - cos.(PI/2 - 0) by SIN_COS:78
.= 1 - 0 by SIN_COS:77;
hence thesis;
end;
theorem
A = [.0,PI.] implies integral(cos,A) = 0
proof
assume A=[.0,PI.];
then upper_bound A=PI & lower_bound A=0 by Th37;
then integral(cos,A) = 0 - sin.0 by Th39,SIN_COS:76
.= 0 - sin.(0+2*PI) by SIN_COS:78
.= 0 - 0 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI*3/2.] implies integral(cos,A) = -1
proof
assume A=[.0,PI*3/2.];
then upper_bound A=PI*3/2 & lower_bound A=0 by Th37;
then integral(cos,A) = -1 - sin.0 by Th39,SIN_COS:76
.= -1 - sin.(0+2*PI) by SIN_COS:78
.= -1 - 0 by SIN_COS:76;
hence thesis;
end;
theorem
A= [.0,PI*2.] implies integral(cos,A) = 0
proof
assume A=[.0,PI*2.];
then upper_bound A=PI*2 & lower_bound A=0 by Th37;
then integral(cos,A) = 0 - sin.0 by Th39,SIN_COS:76
.= 0 - sin.(0+2*PI) by SIN_COS:78
.= 0 - 0 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.2*n*PI,(2*n+1)*PI.] implies integral(cos,A) = 0
proof
assume A=[.2*n*PI,(2*n+1)*PI.];
then upper_bound A=(2*n+1)*PI & lower_bound A=2*n*PI by Th37;
then integral(cos,A) = sin(0+(2*n+1)*PI) - sin(0+2*n*PI) by Th39
.= -sin(0) - sin(0+2*n*PI) by Th2
.= -sin(0) - sin(0) by Th1
.= -sin(0+2 * PI) - sin(0) by SIN_COS:79
.= 0 - 0 by SIN_COS:77,79;
hence thesis;
end;
theorem
A = [.x+2*n*PI,x+(2*n+1)*PI.] implies integral(cos,A) = -2*sin(x)
proof
assume A=[.x+2*n*PI,x+(2*n+1)*PI.];
then upper_bound A=x+(2*n+1)*PI & lower_bound A=x+2*n*PI by Th37;
then integral(cos,A) = sin(x+(2*n+1)*PI) - sin(x+2*n*PI) by Th39
.= -sin(x) - sin(x+2*n*PI) by Th2
.= -sin(x) - sin(x) by Th1
.= -2*sin(x);
hence thesis;
end;
Lm12: -sin is_integrable_on A & (-sin)|A is bounded
proof
(-sin)|A is continuous;
hence thesis by Lm7,INTEGRA5:10,11;
end;
theorem Th46:
integral(-sin,A) = cos.(upper_bound A)-cos.(lower_bound A)
proof
A1: for x being Element of REAL st x in dom (cos`|REAL) holds (cos`|REAL).x
= (-sin).x
proof
let x be Element of REAL;
assume x in dom (cos`|REAL);
(cos`|REAL).x = diff(cos,x) by FDIFF_1:def 7,SIN_COS:67
.= -sin.x by SIN_COS:63;
hence thesis by VALUED_1:8;
end;
A2: -sin is_integrable_on A & (-sin)|A is bounded by Lm12;
dom (-sin) = REAL by FUNCT_2:def 1;
then dom (cos`|REAL) = dom (-sin) by FDIFF_1:def 7,SIN_COS:67;
then cos`|REAL = -sin by A1,PARTFUN1:5;
hence thesis by A2,INTEGRA5:13,SIN_COS:67;
end;
theorem
A = [.0,PI/2.] implies integral(-sin,A) = -1
proof
assume A=[.0,PI/2.];
then upper_bound A=PI/2 & lower_bound A=0 by Th37;
then integral(-sin,A) = 0 - cos.0 by Th46,SIN_COS:76
.= 0 - sin.(PI/2 - 0) by SIN_COS:78
.= 0 - 1 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI.] implies integral(-sin,A) = -2
proof
assume A=[.0,PI.];
then upper_bound A=PI & lower_bound A=0 by Th37;
then integral(-sin,A) = -1 - cos.0 by Th46,SIN_COS:76
.= -1 - sin.(PI/2 - 0) by SIN_COS:78
.= -1 - 1 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI*3/2.] implies integral(-sin,A) = -1
proof
assume A=[.0,PI*3/2.];
then upper_bound A=PI*3/2 & lower_bound A=0 by Th37;
then integral(-sin,A) = 0 - cos.0 by Th46,SIN_COS:76
.= 0 - sin.(PI/2 - 0) by SIN_COS:78
.= 0 - 1 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI*2.] implies integral(-sin,A) = 0
proof
assume A=[.0,PI*2.];
then upper_bound A=PI*2 & lower_bound A=0 by Th37;
then integral(-sin,A) = 1 - cos.0 by Th46,SIN_COS:76
.= 1 - sin.(PI/2 - 0) by SIN_COS:78
.= 1 - 1 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.2*n*PI,(2*n+1)*PI.] implies integral(-sin,A) = -2
proof
assume A=[.2*n*PI,(2*n+1)*PI.];
then upper_bound A=(2*n+1)*PI & lower_bound A=2*n*PI by Th37;
then integral(-sin,A) = cos(0+(2*n+1)*PI) - cos(0+2*n*PI) by Th46
.= -cos(0) - cos(0+2*n*PI) by Th4
.= -cos(0) - cos(0) by Th3
.= -cos(0+2 * PI) - cos(0) by SIN_COS:79
.= -1 - 1 by SIN_COS:77,79;
hence thesis;
end;
theorem
A = [.x+2*n*PI,x+(2*n+1)*PI.] implies integral(-sin,A) = -2*cos(x)
proof
assume A=[.x+2*n*PI,x+(2*n+1)*PI.];
then upper_bound A=x+(2*n+1)*PI & lower_bound A=x+2*n*PI by Th37;
then integral(-sin,A) = cos(x+(2*n+1)*PI) - cos(x+2*n*PI) by Th46
.= -cos(x) - cos(x+2*n*PI) by Th4
.= -cos(x) - cos(x) by Th3
.= -2*cos(x);
hence thesis;
end;
Lm13: exp_R is_integrable_on A & (exp_R)|A is bounded
proof
exp_R|A is continuous;
hence thesis by Lm8,INTEGRA5:10,11;
end;
theorem Th53:
integral(exp_R,A) = exp_R.(upper_bound A)-exp_R.(lower_bound A)
proof
A1: for x being Element of REAL st x in dom (exp_R`|REAL) holds (exp_R`|REAL
).x = exp_R.x
proof
let x be Element of REAL;
assume x in dom (exp_R`|REAL);
(exp_R`|REAL).x = diff(exp_R,x) by FDIFF_1:def 7,SIN_COS:66;
hence thesis by SIN_COS:65;
end;
A2: exp_R is_integrable_on A & (exp_R)|A is bounded by Lm13;
dom (exp_R`|REAL) = dom exp_R by FDIFF_1:def 7,SIN_COS:47,66;
then exp_R`|REAL = exp_R by A1,PARTFUN1:5;
hence thesis by A2,INTEGRA5:13,SIN_COS:66;
end;
reconsider jj=1 as Real;
theorem
A = [.0,1.] implies integral(exp_R,A) = number_e -1
proof
assume A=[.0,1.];
then A=[.0,jj.];
then upper_bound A=1 & lower_bound A=0 by Th37;
hence thesis by Th53,IRRAT_1:def 7,SIN_COS:51;
end;
Lm14: sinh|A is continuous
proof
sinh|REAL is continuous by FDIFF_1:25,SIN_COS2:34;
hence thesis by FCONT_1:16;
end;
Lm15: sinh is_integrable_on A & sinh|A is bounded
by Lm14,Lm9,INTEGRA5:10,INTEGRA5:11;
theorem Th55:
integral(sinh,A) = cosh.(upper_bound A)-cosh.(lower_bound A)
proof
A1: for x being Element of REAL st x in dom (cosh`|REAL) holds (cosh`|REAL).
x = sinh.x
proof
let x be Element of REAL;
assume x in dom (cosh`|REAL);
(cosh`|REAL).x = diff(cosh,x) by FDIFF_1:def 7,SIN_COS2:35;
hence thesis by SIN_COS2:35;
end;
A2: sinh is_integrable_on A & sinh|A is bounded by Lm15;
dom (cosh`|REAL) = dom sinh by FDIFF_1:def 7,SIN_COS2:30,35;
then cosh`|REAL = sinh by A1,PARTFUN1:5;
hence thesis by A2,INTEGRA5:13,SIN_COS2:35;
end;
theorem
A= [.0,1.] implies integral(sinh,A) = (number_e - 1)^2/(2*number_e)
proof
exp_R(1)>0 by SIN_COS:55;
then
A1: 2*number_e > 0 by IRRAT_1:def 7,XREAL_1:129;
assume A=[.0,1.];
then A=[.0,jj.];
then upper_bound A=1 & lower_bound A=0 by Th37;
then integral(sinh,A) = (number_e^2 + 1)/(2*number_e) - 1 by Th18,Th19,Th55
.= (number_e^2 + 1)/(2*number_e) - (2*number_e)/(2*number_e) by A1,
XCMPLX_1:60
.= ((number_e^2 + 1) - (2*number_e))/(2*number_e) by XCMPLX_1:120
.= (number_e^2 - 2*number_e*1 + 1^2)/(2*number_e)
.= (number_e - 1)^2/(2*number_e);
hence thesis;
end;
Lm16: cosh|A is continuous
proof
cosh|REAL is continuous by FDIFF_1:25,SIN_COS2:35;
hence thesis by FCONT_1:16;
end;
Lm17: cosh is_integrable_on A & cosh|A is bounded
by Lm16,Lm10,INTEGRA5:10,INTEGRA5:11;
theorem Th57:
integral(cosh,A) = sinh.(upper_bound A)-sinh.(lower_bound A)
proof
A1: for x being Element of REAL st x in dom (sinh`|REAL) holds (sinh`|REAL).
x = cosh.x
proof
let x be Element of REAL;
assume x in dom (sinh`|REAL);
(sinh`|REAL).x = diff(sinh,x) by FDIFF_1:def 7,SIN_COS2:34;
hence thesis by SIN_COS2:34;
end;
A2: cosh is_integrable_on A & cosh|A is bounded by Lm17;
dom (sinh`|REAL) = dom cosh by FDIFF_1:def 7,SIN_COS2:30,34;
then sinh`|REAL = cosh by A1,PARTFUN1:5;
hence thesis by A2,INTEGRA5:13,SIN_COS2:34;
end;
theorem
A= [.0,1.] implies integral(cosh,A) = (number_e^2 - 1)/(2*number_e)
proof
assume A=[.0,1.];
then A=[.0,jj.];
then upper_bound A=1 & lower_bound A=0 by Th37;
then integral(cosh,A) = sinh.1 -0 by Th57,SIN_COS2:16
.= (number_e^2 - 1)/(2*number_e) by Th17;
hence thesis;
end;
theorem
A c= Z & dom tan = Z & dom tan = dom f2 & (for x st x in Z holds f2.x
= 1/(cos.x)^2 & cos.x <> 0) & f2|A is continuous implies integral(f2,A) = tan.(
upper_bound A)-tan.(lower_bound A)
proof
assume that
A1: A c= Z and
A2: dom tan = Z and
A3: dom tan = dom f2 and
A4: for x st x in Z holds f2.x = 1/(cos.x)^2 & cos.x <> 0 and
A5: f2|A is continuous;
A6: f2 is_integrable_on A by A1,A2,A3,A5,INTEGRA5:11;
A7: tan is_differentiable_on Z by A2,Th33;
A8: for x being Element of REAL st x in dom (tan`|Z) holds (tan`|Z).x = f2.x
proof
let x be Element of REAL;
assume x in dom ((tan)`|Z);
then
A9: x in Z by A7,FDIFF_1:def 7;
then ((tan)`|Z).x = 1/(cos.x)^2 by A2,Th33
.= f2.x by A4,A9;
hence thesis;
end;
dom (tan`|Z) = dom f2 by A2,A3,A7,FDIFF_1:def 7;
then (tan`|Z) = f2 by A8,PARTFUN1:5;
hence thesis by A1,A2,A3,A5,A6,A7,INTEGRA5:10,13;
end;
theorem
A c= Z & dom cot = Z & dom cot = dom f2 & (for x st x in Z holds f2.x
= -1/(sin.x)^2 & sin.x <> 0) & f2|A is continuous implies integral(f2,A) = cot.
(upper_bound A)-cot.(lower_bound A)
proof
assume that
A1: A c= Z and
A2: dom cot = Z and
A3: dom cot = dom f2 and
A4: for x st x in Z holds f2.x = -1/(sin.x)^2 & sin.x <> 0 and
A5: f2|A is continuous;
A6: f2 is_integrable_on A by A1,A2,A3,A5,INTEGRA5:11;
A7: cot is_differentiable_on Z by A2,Th34;
A8: for x being Element of REAL st x in dom (cot`|Z) holds (cot`|Z).x = f2.x
proof
let x be Element of REAL;
assume x in dom ((cot)`|Z);
then
A9: x in Z by A7,FDIFF_1:def 7;
then (cot`|Z).x = -1/(sin.x)^2 by A2,Th34
.= f2.x by A4,A9;
hence thesis;
end;
dom (cot`|Z) = dom f2 by A2,A3,A7,FDIFF_1:def 7;
then (cot`|Z) = f2 by A8,PARTFUN1:5;
hence thesis by A1,A2,A3,A5,A6,A7,INTEGRA5:10,13;
end;
theorem
dom tanh = dom f2 & (for x st x in REAL holds f2.x = 1/(cosh.x)^2) &
f2|A is continuous implies integral(f2,A) = tanh.(upper_bound A)-tanh.(
lower_bound A)
proof
assume that
A1: dom tanh = dom f2 and
A2: for x st x in REAL holds f2.x = 1/(cosh.x)^2 and
A3: f2|A is continuous;
A4: for x being Element of REAL st x in dom (tanh`|REAL)
holds (tanh`|REAL).x = f2.x
proof
let x be Element of REAL;
assume x in dom (tanh`|REAL);
(tanh`|REAL).x =diff(tanh,x) by FDIFF_1:def 7,SIN_COS2:36
.= 1/(cosh.x)^2 by SIN_COS2:33
.= f2.x by A2;
hence thesis;
end;
dom ((tanh)`|REAL) = dom f2 by A1,FDIFF_1:def 7,SIN_COS2:30,36;
then
A5: ((tanh)`|REAL) = f2 by A4,PARTFUN1:5;
A6: dom tanh = REAL by FUNCT_2:def 1;
then f2 is_integrable_on A by A1,A3,INTEGRA5:11;
hence thesis by A1,A3,A6,A5,INTEGRA5:10,13,SIN_COS2:36;
end;
Lm18: dom ((arcsin)`|].-1,1.[ ) = ].-1,1.[ by FDIFF_1:def 7,SIN_COS6:83;
theorem Th62:
A c=].-1,1.[ & dom ((arcsin)`|].-1,1.[) = dom f2 & (for x holds
x in ].-1,1.[ & f2.x = 1/sqrt(1-x^2)) & f2|A is continuous implies integral(f2,
A) = arcsin.(upper_bound A)-arcsin.(lower_bound A)
proof
assume that
A1: A c=].-1,1.[ and
A2: dom ((arcsin)`|].-1,1.[) = dom f2 and
A3: for x holds x in ].-1,1.[ & f2.x = 1/sqrt(1-x^2) and
A4: f2|A is continuous;
for x being Element of REAL
st x in dom ((arcsin)`|].-1,1.[) holds ((arcsin)`|].-1,1.[).x = f2 .x
proof
let x be Element of REAL;
assume
A5: x in dom ((arcsin)`|].-1,1.[);
then
A6: -1 < x & x < 1 by Lm18,XXREAL_1:4;
((arcsin)`|].-1,1.[).x =diff(arcsin,x) by A5,Lm18,FDIFF_1:def 7,SIN_COS6:83
.= 1 / sqrt(1-x^2) by A6,SIN_COS6:83
.= f2.x by A3;
hence thesis;
end;
then
A7: (arcsin`|].-1,1.[) = f2 by A2,PARTFUN1:5;
A c= dom f2 & f2 is_integrable_on A by A1,A2,A4,Lm18,INTEGRA5:11;
hence thesis by A1,A4,A7,INTEGRA5:10,13,SIN_COS6:83;
end;
theorem Th63:
A c=].-1,1.[ & dom (arccos`|].-1,1.[) = dom f2 & (for x holds x
in ].-1,1.[ & f2.x = -1/sqrt(1-x^2)) & f2|A is continuous implies integral(f2,A
) = arccos.(upper_bound A)-arccos.(lower_bound A)
proof
assume that
A1: A c=].-1,1.[ and
A2: dom ((arccos)`|].-1,1.[) = dom f2 and
A3: for x holds x in ].-1,1.[ & f2.x = -1/sqrt(1-x^2) and
A4: f2|A is continuous;
A5: A c= dom f2 by A1,A2,FDIFF_1:def 7,SIN_COS6:106;
A6: dom (arccos`|].-1,1.[ ) = ].-1,1.[ by FDIFF_1:def 7,SIN_COS6:106;
for x being Element of REAL
st x in dom ((arccos)`|].-1,1.[) holds ((arccos)`|].-1,1.[).x = f2 .x
proof
let x be Element of REAL;
assume
A7: x in dom (arccos`|].-1,1.[);
then
A8: -1 < x & x < 1 by A6,XXREAL_1:4;
((arccos)`|].-1,1.[).x =diff(arccos,x) by A6,A7,FDIFF_1:def 7,SIN_COS6:106
.= -1 / sqrt(1-x^2) by A8,SIN_COS6:106
.= f2.x by A3;
hence thesis;
end;
then
A9: ((arccos)`|].-1,1.[) = f2 by A2,PARTFUN1:5;
f2 is_integrable_on A by A6,A1,A2,A4,INTEGRA5:11;
hence thesis by A1,A4,A5,A9,INTEGRA5:10,13,SIN_COS6:106;
end;
theorem
A = [.-sqrt 2/2,sqrt 2/2.] & dom ((arcsin)`|].-1,1.[) = dom f2 & (for
x holds x in ].-1,1.[ & f2.x = 1/sqrt(1-x^2)) & f2|A is continuous implies
integral(f2,A) = PI/2
proof
assume that
A1: A = [.-sqrt 2/2,sqrt 2/2.] and
A2: ( dom ((arcsin)`|].-1,1.[) = dom f2 & for x holds x in ].-1,1.[ & f2
.x = 1/ sqrt(1-x^2) )& f2|A is continuous;
upper_bound A = sqrt 2/2 & lower_bound A = -sqrt 2/2 by A1,Th37;
then integral(f2,A) = arcsin.(sqrt 2/2) - arcsin.(-sqrt 2/2) by A1,A2,Th9
,Th62
.= arcsin(sqrt 2/2) - arcsin.(-sqrt 2/2) by SIN_COS6:def 2
.= arcsin(sqrt 2/2) - arcsin(-sqrt 2/2) by SIN_COS6:def 2
.=(2*PI)/4 by Th10,Th11;
hence thesis;
end;
theorem
A = [.-sqrt 2/2,sqrt 2/2.] & dom ((arccos)`|].-1,1.[) = dom f2 & (for
x holds x in ].-1,1.[ & f2.x = -1/sqrt(1-x^2)) & f2|A is continuous implies
integral(f2,A) = -PI/2
proof
assume that
A1: A = [.-sqrt 2/2,sqrt 2/2.] and
A2: ( dom ((arccos)`|].-1,1.[) = dom f2 & for x holds x in ].-1,1.[ & f2
.x = -1/ sqrt(1-x^2) )& f2|A is continuous;
upper_bound A = sqrt 2/2 & lower_bound A = -sqrt 2/2 by A1,Th37;
then integral(f2,A) = arccos.(sqrt 2/2)-arccos.(-sqrt 2/2) by A1,A2,Th9,Th63
.= arccos(sqrt 2/2) - arccos.(-sqrt 2/2) by SIN_COS6:def 4
.= arccos(sqrt 2/2) - arccos(-sqrt 2/2) by SIN_COS6:def 4
.=(-2*PI)/4 by Th15,Th16;
hence thesis;
end;
theorem Th66:
f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f
`|Z is_integrable_on A & (f`|Z)|A is bounded & g`|Z is_integrable_on A & (g`|Z)
|A is bounded implies integral(f`|Z+g`|Z,A) = f.(upper_bound A) - f.(
lower_bound A) + g.(upper_bound A) - g.(lower_bound A)
proof
assume that
A1: f is_differentiable_on Z and
A2: g is_differentiable_on Z and
A3: A c= Z and
A4: f`|Z is_integrable_on A and
A5: (f`|Z)|A is bounded and
A6: g`|Z is_integrable_on A and
A7: (g`|Z)|A is bounded;
A8: (f`|Z)||A is integrable & (g`|Z)||A is integrable by A4,A6;
A c= dom(g`|Z) by A2,A3,FDIFF_1:def 7;
then
A9: (g`|Z)||A is Function of A,REAL by FUNCT_2:68,INTEGRA5:6;
A c= dom(f`|Z) by A1,A3,FDIFF_1:def 7;
then
A10: (f`|Z)||A is Function of A,REAL by FUNCT_2:68,INTEGRA5:6;
A11: (f`|Z)||A|A is bounded & (g`|Z)||A|A is bounded by A5,A7,INTEGRA5:9;
integral(f`|Z+g`|Z,A) = integral((f`|Z)||A+(g`|Z)||A) by INTEGRA5:5
.= integral(f`|Z,A) + integral(g`|Z,A) by A8,A10,A9,A11,INTEGRA1:57
.= f.(upper_bound A) - f.(lower_bound A)+ integral(g`|Z,A) by A1,A3,A4,A5,
INTEGRA5:13
.= f.(upper_bound A) - f.(lower_bound A)+ (g.(upper_bound A) - g.(
lower_bound A)) by A2,A3,A6,A7,INTEGRA5:13;
hence thesis;
end;
theorem Th67:
f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f
`|Z is_integrable_on A & (f`|Z)|A is bounded & g`|Z is_integrable_on A & (g`|Z)
|A is bounded implies integral(f`|Z-g`|Z,A) = f.(upper_bound A) - f.(
lower_bound A) - (g.(upper_bound A) - g.(lower_bound A))
proof
assume that
A1: f is_differentiable_on Z and
A2: g is_differentiable_on Z and
A3: A c= Z and
A4: f`|Z is_integrable_on A and
A5: (f`|Z)|A is bounded and
A6: g`|Z is_integrable_on A and
A7: (g`|Z)|A is bounded;
A8: (f`|Z)||A is integrable & (g`|Z)||A is integrable by A4,A6;
A c= dom(g`|Z) by A2,A3,FDIFF_1:def 7;
then
A9: (g`|Z)||A is Function of A,REAL by FUNCT_2:68,INTEGRA5:6;
A c= dom(f`|Z) by A1,A3,FDIFF_1:def 7;
then
A10: (f`|Z)||A is Function of A,REAL by FUNCT_2:68,INTEGRA5:6;
A11: (f`|Z)||A|A is bounded & (g`|Z)||A|A is bounded by A5,A7,INTEGRA5:9;
integral(f`|Z-g`|Z,A) = integral((f`|Z)||A-(g`|Z)||A) by RFUNCT_1:47
.= integral(f`|Z,A) - integral((g`|Z)||A) by A8,A10,A9,A11,INTEGRA2:33
.= f.(upper_bound A) - f.(lower_bound A)- integral(g`|Z,A) by A1,A3,A4,A5,
INTEGRA5:13
.= f.(upper_bound A) - f.(lower_bound A)- (g.(upper_bound A) - g.
lower_bound A) by A2,A3,A6,A7,INTEGRA5:13;
hence thesis;
end;
theorem Th68:
f is_differentiable_on Z & A c= Z & f`|Z is_integrable_on A & (f
`|Z)|A is bounded implies integral((r(#)(f`|Z)),A) = r*f.(upper_bound A) - r*f.
(lower_bound A)
proof
assume that
A1: f is_differentiable_on Z & A c= Z and
A2: f`|Z is_integrable_on A & (f`|Z)|A is bounded;
A3: (f`|Z)||A is integrable & (f`|Z)||A|A is bounded by A2,INTEGRA5:9;
A c= dom(f`|Z) by A1,FDIFF_1:def 7;
then
A4: (f`|Z)||A is Function of A,REAL by FUNCT_2:68,INTEGRA5:6;
integral((r(#)(f`|Z)),A) = integral (r(#)((f`|Z)||A)) by RFUNCT_1:49
.= r * integral ((f`|Z),A) by A4,A3,INTEGRA2:31
.= r*(f.(upper_bound A) - f.(lower_bound A)) by A1,A2,INTEGRA5:13;
hence thesis;
end;
Lm19: sin is_integrable_on A & sin|A is bounded
proof
sin|A is continuous;
hence thesis by Lm5,INTEGRA5:10,11;
end;
theorem Th69:
integral(sin+cos,A) = (-cos).(upper_bound A) - (-cos).(
lower_bound A) + sin.(upper_bound A) - sin.(lower_bound A)
proof
A1: [#]REAL is open Subset of REAL;
A2: sin is_integrable_on A & sin|A is bounded by Lm19;
cos is_integrable_on A & cos|A is bounded by Lm11;
hence thesis by A2,A1,Th26,Th27,Th29,Th66,SIN_COS:68;
end;
theorem
A = [.0,PI/2.] implies integral(sin+cos,A) = 2
proof
assume A = [.0,PI/2.];
then upper_bound A=PI/2 & lower_bound A=0 by Th37;
then integral(sin+cos,A) = (-cos).(PI/2) - (-cos).0 + sin.(PI/2) - sin.0 by
Th69
.= -(cos.(PI/2)) - (-cos).0 + sin.(PI/2) - sin.0 by VALUED_1:8
.= -0 - (-cos.0) + 1 - sin.0 by SIN_COS:76,VALUED_1:8
.= - (-cos.0) + 1 - sin.(0+2 * PI) by SIN_COS:78
.= - (-cos.(0+2*PI)) + 1 - 0 by SIN_COS:76,78
.= 2 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI.] implies integral(sin+cos,A) = 2
proof
assume A = [.0,PI.];
then upper_bound A=PI & lower_bound A=0 by Th37;
then integral(sin+cos,A) = (-cos).(PI) - (-cos).0 + sin.(PI) - sin.0 by Th69
.= -(cos.(PI)) - (-cos).0 + sin.(PI) - sin.0 by VALUED_1:8
.= -(cos.(PI)) - (-cos.0) + sin.(PI) - sin.0 by VALUED_1:8
.= - (-cos.0) + 1 - sin.(0+2 * PI) by SIN_COS:76,78
.= - (-cos.(0+2*PI)) + 1 - 0 by SIN_COS:76,78
.= 2 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI*3/2.] implies integral(sin+cos,A) = 0
proof
assume A = [.0,PI*3/2.];
then upper_bound A=PI*3/2 & lower_bound A=0 by Th37;
then
integral(sin+cos,A) = (-cos).(PI*3/2) - (-cos).0 + sin.(PI*3/2) - sin.0
by Th69
.= -(cos.(PI*3/2)) - (-cos).0 + sin.(PI*3/2) - sin.0 by VALUED_1:8
.= -(cos.(PI*3/2)) - (-cos.0) + sin.(PI*3/2) - sin.0 by VALUED_1:8
.= -(cos.(PI*3/2)) - (-cos.(0+2*PI)) + sin.(PI*3/2) - sin.0 by SIN_COS:78
.= -0 +1 + -1 - 0 by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.0,PI*2.] implies integral(sin+cos,A) = 0
proof
assume A = [.0,PI*2.];
then upper_bound A=PI*2 & lower_bound A=0 by Th37;
then integral(sin+cos,A) = (-cos).(PI*2) - (-cos).0 + sin.(PI*2) - sin.0 by
Th69
.= -(cos.(PI*2)) - (-cos).0 + sin.(PI*2) - sin.0 by VALUED_1:8
.= -(cos.(PI*2)) - (-cos.0) + sin.(PI*2) - sin.0 by VALUED_1:8
.= -(cos.(PI*2)) - (-cos.(0+2*PI)) + sin.(PI*2) - sin.0 by SIN_COS:78
.= -1+1 + 0 - 0 by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.2*n*PI,(2*n+1)*PI.] implies integral(sin+cos,A) = 2
proof
assume A = [.2*n*PI,(2*n+1)*PI.];
then upper_bound A=(2*n+1)*PI & lower_bound A=(2*n*PI) by Th37;
then
integral(sin+cos,A) = (-cos).((2*n+1)*PI) - (-cos).(2*n*PI) + sin.((2*n+
1)*PI) - sin.(2*n*PI) by Th69
.= -(cos.((2*n+1)*PI)) - (-cos).(2*n*PI) + sin.((2*n+1)*PI) - sin.(2*n*
PI) by VALUED_1:8
.= -(cos.((2*n+1)*PI)) - -(cos(0+2*n*PI)) + sin.((2*n+1)*PI) - sin.(0+2*
n*PI) by VALUED_1:8
.= -(cos.((2*n+1)*PI)) - -(cos(0)) + sin.((2*n+1)*PI) - sin.(0+2*n*PI)
by Th3
.= -(cos.((2*n+1)*PI)) + (cos(0)) + sin.((2*n+1)*PI) - sin.(0+2*n*PI)
.= -(cos.((2*n+1)*PI)) + (cos(0+2*PI)) + sin.((2*n+1)*PI) - sin.(0+2*n*
PI) by SIN_COS:79
.= -(cos.((2*n+1)*PI)) + 1 + sin.((2*n+1)*PI) - sin(0+2*n*PI) by SIN_COS:77
.= -(cos.((2*n+1)*PI)) + 1 + sin.((2*n+1)*PI) - sin(0) by Th1
.= -(cos.((2*n+1)*PI)) + 1 + sin.((2*n+1)*PI) - sin(0+2*PI) by SIN_COS:79
.= -(cos(0+(2*n+1)*PI)) + 1 + sin(0+(2*n+1)*PI) by SIN_COS:77
.= -(cos(0+(2*n+1)*PI)) + 1 + -sin(0) by Th2
.= - -cos(0) + 1 + -sin(0) by Th4
.= cos(0) + 1 - sin(0)
.= cos(0+2*PI) + 1 - sin(0) by SIN_COS:79
.= cos(0+2*PI) + 1 - sin(0+2*PI) by SIN_COS:79
.= 2 by SIN_COS:77;
hence thesis;
end;
theorem
A = [.x+2*n*PI,x+(2*n+1)*PI.] implies integral(sin+cos,A) = 2*cos x - 2*sin x
proof
assume A = [.x+2*n*PI,x+(2*n+1)*PI.];
then upper_bound A=x+(2*n+1)*PI & lower_bound A=x+2*n*PI by Th37;
then
integral(sin+cos,A) = (-cos).(x+(2*n+1)*PI) - (-cos).(x+2*n*PI) + sin.(x
+(2*n+1)*PI) - sin.(x+2*n*PI) by Th69
.= -(cos.(x+(2*n+1)*PI)) - (-cos).(x+2*n*PI) + sin.(x+(2*n+1)*PI) - sin.
(x+2*n*PI) by VALUED_1:8
.= -(cos(x+(2*n+1)*PI)) - -(cos(x+2*n*PI)) + sin(x+(2*n+1)*PI) - sin(x+2
*n*PI) by VALUED_1:8
.= -(-cos x) - -(cos(x+2*n*PI)) + sin(x+(2*n+1)*PI) - sin(x+2*n*PI) by Th4
.= -(-cos x) - -cos x + sin(x+(2*n+1)*PI) - sin(x+2*n*PI) by Th3
.= -(-cos x) - -cos x + -sin x - sin(x+2*n*PI) by Th2
.= cos x + cos x -sin x - sin x by Th1
.= 2* cos x - 2*sin x;
hence thesis;
end;
theorem Th76:
integral(sinh+cosh,A) = cosh.(upper_bound A) - cosh.(lower_bound
A) + sinh.(upper_bound A) - sinh.(lower_bound A)
proof
A1: [#]REAL is open Subset of REAL;
cosh|A is continuous by Lm16;
then
A2: cosh is_integrable_on A by Lm10,INTEGRA5:11;
sinh|A is continuous by Lm14;
then
A3: sinh is_integrable_on A by Lm9,INTEGRA5:11;
cosh|A is bounded & sinh|A is bounded by Lm9,Lm10,Lm14,Lm16,INTEGRA5:10;
hence thesis by A2,A3,A1,Th30,Th31,Th66,SIN_COS2:34,35;
end;
theorem
A = [.0,1.] implies integral(sinh+cosh,A) = number_e -1
proof
A1: number_e > 0 by IRRAT_1:def 7,SIN_COS:55;
assume A = [.0,1.];
then upper_bound A=1 & lower_bound A=0 by Th37;
then integral(sinh+cosh,A) = cosh.1 - cosh.0 + sinh.1 - sinh.0 by Th76
.= (number_e^2 + 1)/(2*number_e) + (number_e^2 - 1)/(2*number_e) - 1 by
Th17,Th18,Th19,SIN_COS2:16
.= ((number_e^2 + 1) + (number_e^2 - 1))/(2*number_e) -1 by XCMPLX_1:62
.= (2*number_e^2)/(2*number_e) -1
.= number_e^2/number_e -1 by XCMPLX_1:91
.= number_e*number_e/number_e -1
.= number_e -1 by A1,XCMPLX_1:89;
hence thesis;
end;
theorem Th78:
integral(sin-cos,A) = (-cos).(upper_bound A) - (-cos).(
lower_bound A) - (sin.(upper_bound A) - sin.(lower_bound A))
proof
A1: [#]REAL is open Subset of REAL;
A2: sin is_integrable_on A & sin|A is bounded by Lm19;
cos is_integrable_on A & cos|A is bounded by Lm11;
hence thesis by A2,A1,Th26,Th27,Th29,Th67,SIN_COS:68;
end;
theorem
A = [.0,PI/2.] implies integral(sin-cos,A) = 0
proof
assume A = [.0,PI/2.];
then upper_bound A=PI/2 & lower_bound A=0 by Th37;
then
integral(sin-cos,A) = (-cos).(PI/2) - (-cos).0 - (sin.(PI/2) - sin.0) by Th78
.= -(cos.(PI/2)) - (-cos).0 - (sin.(PI/2) - sin.0) by VALUED_1:8
.= -0 - (-cos.0) - (1 - sin.0) by SIN_COS:76,VALUED_1:8
.= - (-cos.0) - (1 - sin.(0+2 * PI)) by SIN_COS:78
.= - (-cos.(0+2*PI)) - (1 - 0) by SIN_COS:76,78
.= 0 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI.] implies integral(sin-cos,A) = 2
proof
assume A = [.0,PI.];
then upper_bound A=PI & lower_bound A=0 by Th37;
then integral(sin-cos,A) = (-cos).(PI) - (-cos).0 - (sin.(PI) - sin.0) by
Th78
.= -(cos.(PI)) - (-cos).0 - (sin.(PI) - sin.0) by VALUED_1:8
.= -(cos.(PI)) - (-cos.0) - (sin.(PI) - sin.0) by VALUED_1:8
.= - (-cos.0) + 1 - (sin.(0+2 * PI)-0) by SIN_COS:76,78
.= - (-cos.(0+2*PI)) + 1 - 0 by SIN_COS:76,78
.= 2 by SIN_COS:76;
hence thesis;
end;
theorem
A = [.0,PI*3/2.] implies integral(sin-cos,A) = 2
proof
assume A = [.0,PI*3/2.];
then upper_bound A=PI*3/2 & lower_bound A=0 by Th37;
then
integral(sin-cos,A) = (-cos).(PI*3/2) - (-cos).0 - (sin.(PI*3/2) - sin.0
) by Th78
.= -(cos.(PI*3/2)) - (-cos).0 - (sin.(PI*3/2) - sin.0) by VALUED_1:8
.= -(cos.(PI*3/2)) - (-cos.0) - (sin.(PI*3/2) - sin.0) by VALUED_1:8
.= -(cos.(PI*3/2)) - (-cos.(0+2*PI)) - (sin.(PI*3/2) - sin.0) by SIN_COS:78
.= -0 +1 - (-1 - 0) by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.0,PI*2.] implies integral(sin-cos,A) = 0
proof
assume A = [.0,PI*2.];
then upper_bound A=PI*2 & lower_bound A=0 by Th37;
then
integral(sin-cos,A) = (-cos).(PI*2) - (-cos).0 - (sin.(PI*2) - sin.0) by Th78
.= -(cos.(PI*2)) - (-cos).0 - (sin.(PI*2) - sin.0) by VALUED_1:8
.= -(cos.(PI*2)) - (-cos.0) - (sin.(PI*2) - sin.0) by VALUED_1:8
.= -(cos.(PI*2)) - (-cos.(0+2*PI)) - (sin.(PI*2) - sin.0) by SIN_COS:78
.= -1+1 - (0 - 0) by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.2*n*PI,(2*n+1)*PI.] implies integral(sin-cos,A) = 2
proof
assume A = [.2*n*PI,(2*n+1)*PI.];
then upper_bound A=(2*n+1)*PI & lower_bound A=(2*n*PI) by Th37;
then
integral(sin-cos,A) = (-cos).((2*n+1)*PI) - (-cos).(2*n*PI) - (sin.((2*n
+1)*PI) - sin.(2*n*PI)) by Th78
.= -(cos.((2*n+1)*PI)) - (-cos).(2*n*PI) - (sin.((2*n+1)*PI) - sin.(2*n*
PI)) by VALUED_1:8
.= -(cos.((2*n+1)*PI)) - -(cos(0+2*n*PI)) - (sin.((2*n+1)*PI) - sin.(0+2
*n*PI)) by VALUED_1:8
.= -(cos.((2*n+1)*PI)) - -(cos(0)) - (sin.((2*n+1)*PI) - sin.(0+2*n*PI))
by Th3
.= -(cos.((2*n+1)*PI)) + (cos(0)) - (sin.((2*n+1)*PI) - sin.(0+2*n*PI))
.= -(cos.((2*n+1)*PI)) + (cos(0+2*PI)) - (sin.((2*n+1)*PI) - sin.(0+2*n*
PI)) by SIN_COS:79
.= -(cos.((2*n+1)*PI)) + 1 - (sin.((2*n+1)*PI) - sin(0+2*n*PI)) by
SIN_COS:77
.= -(cos.((2*n+1)*PI)) + 1 - (sin.((2*n+1)*PI) - sin(0)) by Th1
.= -(cos.((2*n+1)*PI)) + 1 - (sin.((2*n+1)*PI) - sin(0+2*PI)) by SIN_COS:79
.= -(cos(0+(2*n+1)*PI)) + 1 - sin(0+(2*n+1)*PI) by SIN_COS:77
.= -(cos(0+(2*n+1)*PI)) + 1 - -sin(0) by Th2
.= - -cos(0) + 1 - -sin(0) by Th4
.= cos(0) + 1 + sin(0)
.= cos(0+2*PI) + 1 + sin(0) by SIN_COS:79
.= cos(0+2*PI) + 1 + sin(0+2*PI) by SIN_COS:79
.= 2 by SIN_COS:77;
hence thesis;
end;
theorem
A = [.x+2*n*PI,x+(2*n+1)*PI.] implies integral(sin-cos,A) = 2*cos x + 2*sin x
proof
assume A = [.x+2*n*PI,x+(2*n+1)*PI.];
then upper_bound A=x+(2*n+1)*PI & lower_bound A=x+2*n*PI by Th37;
then
integral(sin-cos,A) = (-cos).(x+(2*n+1)*PI) - (-cos).(x+2*n*PI) - (sin.(
x+(2*n+1)*PI) - sin.(x+2*n*PI)) by Th78
.= -(cos.(x+(2*n+1)*PI)) - (-cos).(x+2*n*PI) - (sin.(x+(2*n+1)*PI) - sin
.(x+2*n*PI)) by VALUED_1:8
.= -(cos(x+(2*n+1)*PI)) - -(cos(x+2*n*PI)) - (sin(x+(2*n+1)*PI) - sin(x+
2*n*PI)) by VALUED_1:8
.= -(-cos x) - -(cos(x+2*n*PI)) - (sin(x+(2*n+1)*PI) - sin(x+2*n*PI)) by
Th4
.= -(-cos x) - -cos x - (sin(x+(2*n+1)*PI) - sin(x+2*n*PI)) by Th3
.= -(-cos x) - -cos x - (-sin x - sin(x+2*n*PI)) by Th2
.= cos x + cos x - (-sin x - sin x) by Th1
.= 2* cos x + 2*sin x;
hence thesis;
end;
theorem
integral(r(#)sin,A) = r*(-cos).(upper_bound A) - r*(-cos).(lower_bound A)
proof
sin|A is bounded & [#]REAL is open Subset of REAL by Lm5,INTEGRA5:10;
hence thesis by Lm5,Th26,Th29,Th68,INTEGRA5:11;
end;
theorem
integral(r(#)cos,A) = r*sin.(upper_bound A) - r*sin.(lower_bound A)
proof
A1: [#]REAL is open Subset of REAL;
cos is_integrable_on A & cos|A is bounded by Lm11;
hence thesis by A1,Th27,Th68,SIN_COS:68;
end;
theorem
integral(r(#)sinh,A) = r*cosh.(upper_bound A) - r*cosh.(lower_bound A)
proof
A1: [#]REAL is open Subset of REAL;
sinh|A is continuous & sinh|A is bounded by Lm9,Lm14,INTEGRA5:10;
hence thesis by A1,Lm9,Th31,Th68,INTEGRA5:11,SIN_COS2:35;
end;
theorem
integral(r(#)cosh,A) = r*sinh.(upper_bound A) - r*sinh.(lower_bound A)
proof
A1: [#]REAL is open Subset of REAL;
cosh|A is continuous & cosh|A is bounded by Lm10,Lm16,INTEGRA5:10;
hence thesis by A1,Lm10,Th30,Th68,INTEGRA5:11,SIN_COS2:34;
end;
theorem
integral(r(#)exp_R,A) = r*exp_R.(upper_bound A) - r*exp_R.(lower_bound A)
proof
(exp_R)|A is bounded & [#]REAL is open Subset of REAL by Lm8,INTEGRA5:10;
hence thesis by Lm8,Th32,Th68,INTEGRA5:11,SIN_COS:66;
end;
theorem Th90:
integral(sin(#)cos,A) = 1/2*(cos.(lower_bound A)*cos.(
lower_bound A)- cos.(upper_bound A)*cos.(upper_bound A))
proof
A1: [#]REAL is open Subset of REAL;
sin|A is continuous;
then
A2: (-cos)`|REAL is_integrable_on A by Lm5,Th29,INTEGRA5:11;
(-sin)|A is continuous;
then
A3: cos`|REAL is_integrable_on A by Lm7,Th28,INTEGRA5:11;
((-cos)`|REAL)|A is bounded & (cos`|REAL)|A is bounded by Lm5,Lm7,Th28,Th29,
INTEGRA5:10;
then
integral(sin(#)cos,A) =(-cos).(upper_bound A)*cos.(upper_bound A)- (-cos
).(lower_bound A)*cos.(lower_bound A) -integral((-cos)(#)(-sin),A) by A2,A3
,A1,Th26,Th28,Th29,INTEGRA5:21,SIN_COS:67
.=(-cos).(upper_bound A)*cos.(upper_bound A)- (-cos).(lower_bound A)*cos
.(lower_bound A) -integral(sin(#)cos,A) by Lm4
.=(-cos.(upper_bound A))*cos.(upper_bound A)- (-cos).(lower_bound A)*cos
.(lower_bound A) -integral(sin(#)cos,A) by VALUED_1:8
.=(-cos.(upper_bound A))*cos.(upper_bound A)- (-cos.(lower_bound A))*cos
.(lower_bound A) -integral(sin(#)cos,A) by VALUED_1:8
.=cos.(lower_bound A)*cos.(lower_bound A)- cos.(upper_bound A)*cos.(
upper_bound A) -integral(sin(#)cos,A);
hence thesis;
end;
theorem
A = [.0,PI/2.] implies integral(sin(#)cos,A) = 1/2
proof
assume A = [.0,PI/2.];
then upper_bound A=PI/2 & lower_bound A=0 by Th37;
then integral(sin(#)cos,A) =1/2*(cos.0*cos.0-cos.(PI/2)*cos.(PI/2)) by Th90
.=1/2*(cos.(0+2*PI)*cos.0-cos.(PI/2)*cos.(PI/2)) by SIN_COS:78
.=1/2*(1*1-0*0) by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.0,PI.] implies integral(sin(#)cos,A) = 0
proof
assume A = [.0,PI.];
then upper_bound A=PI & lower_bound A=0 by Th37;
then integral(sin(#)cos,A) =1/2*(cos.0*cos.0-cos.PI*cos.PI) by Th90
.=1/2*(cos.(0+2*PI)*cos.0-cos.PI*cos.PI) by SIN_COS:78
.=1/2*(1*1-(-1)*(-1)) by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.0,PI*(3/2).] implies integral(sin(#)cos,A) = 1/2
proof
assume A = [.0,PI*(3/2).];
then upper_bound A=PI*(3/2) & lower_bound A=0 by Th37;
then integral(sin(#)cos,A) =1/2*(cos.0*cos.0-cos.(PI*(3/2))*cos.(PI*(3/2)))
by Th90
.=1/2*(cos.(0+2*PI)*cos.0-cos.(PI*(3/2))*cos.(PI*(3/2))) by SIN_COS:78
.=1/2*(1*1-0*0) by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.0,PI*2.] implies integral(sin(#)cos,A) = 0
proof
assume A = [.0,PI*2.];
then upper_bound A=PI*2 & lower_bound A=0 by Th37;
then integral(sin(#)cos,A) =1/2*(cos.0*cos.0-cos.(PI*2)*cos.(PI*2)) by Th90
.=1/2*(cos.(0+2*PI)*cos.0-cos.(PI*2)*cos.(PI*2)) by SIN_COS:78
.=1/2*(1*1-1*1) by SIN_COS:76,78;
hence thesis;
end;
theorem
A = [.2*n*PI,(2*n+1)*PI.] implies integral(sin(#)cos,A) = 0
proof
assume A = [.2*n*PI,(2*n+1)*PI.];
then upper_bound A=(2*n+1)*PI & lower_bound A=2*n*PI by Th37;
then
integral(sin(#)cos,A) =1/2*(cos.(2*n*PI)*cos.(2*n*PI)-cos.((2*n+1)*PI)*
cos.((2*n+1)*PI)) by Th90
.=1/2*(cos(0)*cos(0+2*n*PI)-cos.((2*n+1)*PI)*cos.((2*n+1)*PI)) by Th3
.=1/2*(cos(0)*cos(0)-cos.((2*n+1)*PI)*cos.((2*n+1)*PI)) by Th3
.=1/2*(cos(0+2*PI)*cos(0)-cos.((2*n+1)*PI)*cos.((2*n+1)*PI)) by SIN_COS:79
.=1/2*(1*1-cos.((2*n+1)*PI)*cos.((2*n+1)*PI)) by SIN_COS:77,79
.=1/2*(1*1- (-cos(0))*cos(0+(2*n+1)*PI)) by Th4
.=1/2*(1*1- (-cos(0))*(-cos(0))) by Th4
.=1/2*(1*1- cos(0)*cos(0))
.=1/2*(1*1- cos(0+2*PI)*cos(0)) by SIN_COS:79
.=1/2*(1*1- cos(0+2*PI)*cos(0+2*PI)) by SIN_COS:79;
hence thesis by SIN_COS:77;
end;
theorem
A = [.x+2*n*PI,x+(2*n+1)*PI.] implies integral(sin(#)cos,A) = 0
proof
assume A = [.x+2*n*PI,x+(2*n+1)*PI.];
then upper_bound A=x+(2*n+1)*PI & lower_bound A=x+2*n*PI by Th37;
then
integral(sin(#)cos,A) = 1/2*(cos.(x+2*n*PI)*cos.(x+2*n*PI)-cos.(x+(2*n+1
)*PI)*cos.(x+(2*n+1)*PI)) by Th90
.= 1/2*(cos(x)*cos(x+2*n*PI)-cos(x+(2*n+1)*PI)*cos(x+(2*n+1)*PI)) by Th3
.= 1/2*(cos(x)*cos(x)-cos(x+(2*n+1)*PI)*cos(x+(2*n+1)*PI)) by Th3
.= 1/2*(cos(x)*cos(x)- (-cos(x))*cos(x+(2*n+1)*PI)) by Th4
.= 1/2*(cos(x)*cos(x)- (-cos(x))*(-cos(x))) by Th4
.= 0;
hence thesis;
end;
Lm20: cos(#)cos is_integrable_on A & (cos(#)cos)|A is bounded
proof
dom cos = REAL by FUNCT_2:def 1;
then A c= dom cos /\ dom cos;
then
A1: A c= dom(cos(#)cos) by VALUED_1:def 4;
(cos(#)cos)|A is continuous;
hence thesis by A1,INTEGRA5:10,11;
end;
theorem
integral(sin(#)sin,A)=cos.(lower_bound A)*sin.(lower_bound A)- cos.(
upper_bound A)*sin.(upper_bound A)+integral((cos)(#)(cos),A)
proof
A1: [#]REAL is open Subset of REAL;
A2: (cos(#)cos)||A|A is bounded by Lm20,INTEGRA5:9;
sin|A is continuous;
then
A3: (-cos)`|REAL is_integrable_on A by Lm5,Th29,INTEGRA5:11;
dom(cos(#)cos) = REAL by FUNCT_2:def 1;
then
A4: (cos(#)cos)||A is Function of A,REAL by FUNCT_2:68,INTEGRA5:6;
cos|A is continuous;
then
A5: sin`|REAL is_integrable_on A by Lm6,Th27,INTEGRA5:11;
cos(#)cos is_integrable_on A by Lm20;
then
A6: (cos(#)cos)||A is integrable;
((-cos)`|REAL)|A is bounded & (sin`|REAL)|A is bounded by Lm5,Lm6,Th27,Th29,
INTEGRA5:10;
then integral(sin(#)sin,A) =(-cos).(upper_bound A)*sin.(upper_bound A)- (-
cos).(lower_bound A)*sin.(lower_bound A) -integral((-cos)(#)(cos),A) by A3,A5
,A1,Th26,Th27,Th29,INTEGRA5:21,SIN_COS:68
.=(-cos.(upper_bound A))*sin.(upper_bound A)- (-cos).(lower_bound A)*sin
.(lower_bound A) -integral((-cos)(#)(cos),A) by VALUED_1:8
.=(-cos.(upper_bound A))*sin.(upper_bound A)- (-(cos.(lower_bound A)))*
sin.(lower_bound A) -integral((-cos)(#)(cos),A) by VALUED_1:8
.=cos.(lower_bound A)*sin.(lower_bound A)- cos.(upper_bound A)*sin.(
upper_bound A) -integral(-((cos)(#)(cos)),A) by RFUNCT_1:12
.=cos.(lower_bound A)*sin.(lower_bound A) - cos.(upper_bound A)*sin.(
upper_bound A) -integral((-1)(#)(((cos)(#)(cos))||A)) by RFUNCT_1:49
.=cos.(lower_bound A)*sin.(lower_bound A)- cos.(upper_bound A)*sin.(
upper_bound A) -(-1)*integral((cos)(#)(cos),A) by A6,A2,A4,INTEGRA2:31
.=cos.(lower_bound A)*sin.(lower_bound A)- cos.(upper_bound A)*sin.(
upper_bound A) + integral((cos)(#)(cos),A);
hence thesis;
end;
theorem
integral(sinh(#)sinh,A)=cosh.(upper_bound A)*sinh.(upper_bound A)-
cosh.(lower_bound A)*sinh.(lower_bound A)-integral((cosh)(#)(cosh),A)
proof
A1: [#]REAL is open Subset of REAL;
A2: sinh`|REAL is_integrable_on A & (sinh`|REAL)|A is bounded by Lm17,Th30;
(cosh)`|REAL is_integrable_on A & (cosh`|REAL)|A is bounded by Lm15,Th31;
hence thesis by A2,A1,Th30,Th31,INTEGRA5:21,SIN_COS2:34,35;
end;
theorem
integral(sinh(#)cosh,A) =1/2*((cosh.(upper_bound A))*cosh.(upper_bound
A)- (cosh).(lower_bound A)*cosh.(lower_bound A))
proof
sinh|A is continuous by Lm14;
then
A1: (cosh)`|REAL is_integrable_on A by Lm9,Th31,INTEGRA5:11;
(cosh`|REAL)|A is bounded & [#]REAL is open Subset of REAL by Lm9,Lm14,Th31,
INTEGRA5:10;
then
integral(sinh(#)cosh,A) =(cosh.(upper_bound A))*cosh.(upper_bound A)- (
cosh).(lower_bound A)*cosh.(lower_bound A) -integral(sinh(#)cosh,A) by A1
,Th31,INTEGRA5:21,SIN_COS2:35;
hence thesis;
end;
theorem
integral(exp_R(#)exp_R,A) =1/2*((exp_R.(upper_bound A))^2 -((exp_R).(
lower_bound A))^2)
proof
exp_R|A is continuous;
then
A1: exp_R`|REAL is_integrable_on A by Lm8,Th32,INTEGRA5:11;
(exp_R`|REAL)|A is bounded & [#]REAL is open Subset of REAL by Lm8,Th32,
INTEGRA5:10;
then
integral(exp_R(#)exp_R,A) =(exp_R).(upper_bound A)*exp_R.(upper_bound A)
- (exp_R).(lower_bound A)*exp_R.(lower_bound A) -integral((exp_R)(#)(exp_R),A)
by A1,Th32,INTEGRA5:21,SIN_COS:66
.= (exp_R.(upper_bound A))^2 - ((exp_R).(lower_bound A))*exp_R.(
lower_bound A) -integral(exp_R(#)exp_R,A)
.= (exp_R.(upper_bound A))^2 - ((exp_R).(lower_bound A))^2 -integral(
exp_R(#)exp_R,A);
hence thesis;
end;
Lm21: exp_R(#)(sin + cos) is_integrable_on A & (exp_R(#)(sin +cos))|A is
bounded
proof
A1: dom(sin + cos) = dom sin /\ dom cos by VALUED_1:def 1;
dom sin = REAL & dom cos = REAL by FUNCT_2:def 1;
then A c= dom exp_R /\ dom(sin + cos) by A1,SIN_COS:47;
then
A2: A c= dom(exp_R(#)(sin + cos)) by VALUED_1:def 4;
(exp_R(#)(sin + cos))|A is continuous;
hence thesis by A2,INTEGRA5:10,11;
end;
Lm22: exp_R(#)(cos - sin) is_integrable_on A & (exp_R(#)(cos - sin))|A is
bounded
proof
dom exp_R = REAL & dom(cos - sin) = REAL by FUNCT_2:def 1;
then A c= dom exp_R /\ dom(cos - sin);
then
A1: A c= dom(exp_R(#)(cos - sin)) by VALUED_1:def 4;
(exp_R(#)(cos - sin))|A is continuous;
hence thesis by A1,INTEGRA5:10,11;
end;
theorem
integral(exp_R(#)(sin+cos),A) = (exp_R(#)sin).(upper_bound A)-(exp_R
(#)sin).(lower_bound A)
proof
A1: dom (sin+cos) = REAL by FUNCT_2:def 1;
A2: dom (exp_R(#)(sin+cos)) = dom exp_R /\ dom (sin+cos) by VALUED_1:def 4
.= REAL /\ dom (sin+cos) by SIN_COS:47
.= REAL by A1;
A3: exp_R(#)(sin + cos) is_integrable_on A & (exp_R(#)(sin +cos))|A is
bounded by Lm21;
A4: dom (exp_R(#)sin) = REAL & [#]REAL is open Subset of REAL by FUNCT_2:def 1;
A5: for x being Element of REAL
st x in dom ((exp_R(#)sin)`|REAL) holds ((exp_R(#)sin)`|REAL).x =
(exp_R(#)(sin + cos)).x
proof
let x be Element of REAL;
reconsider xx=x as Real;
assume x in dom ((exp_R(#)sin)`|REAL);
(exp_R(#)(sin + cos)).x = (exp_R.x) * ((sin + cos).x) by VALUED_1:5
.= (exp_R.x) * (sin.xx + cos.xx) by VALUED_1:1;
hence thesis by A4,FDIFF_7:44;
end;
(exp_R(#)sin) is_differentiable_on REAL by A4,FDIFF_7:44;
then dom ((exp_R(#)sin)`|REAL) = dom (exp_R(#)(sin + cos)) by A2,
FDIFF_1:def 7;
then ((exp_R(#)sin)`|REAL) = exp_R(#)(sin + cos) by A5,PARTFUN1:5;
hence thesis by A3,A4,FDIFF_7:44,INTEGRA5:13;
end;
theorem
integral(exp_R(#)(cos-sin),A) = (exp_R(#)cos).(upper_bound A)-(exp_R
(#)cos).(lower_bound A)
proof
A1: dom (exp_R(#)cos) = REAL & [#]REAL is open Subset of REAL by FUNCT_2:def 1;
A2: dom (cos - sin) = REAL by FUNCT_2:def 1;
A3: for x being Element of REAL
st x in dom ((exp_R(#)cos)`|REAL) holds ((exp_R(#)cos)`|REAL).x =
(exp_R(#)(cos - sin)).x
proof
let x be Element of REAL;
assume x in dom ((exp_R(#)cos)`|REAL);
(exp_R(#)(cos - sin)).x = (exp_R.x) * ((cos - sin).x) by VALUED_1:5
.= (exp_R.x) * (cos.x - sin.x) by A2,VALUED_1:13;
hence thesis by A1,FDIFF_7:45;
end;
A4: exp_R(#)(cos - sin) is_integrable_on A & (exp_R(#)(cos - sin))|A is
bounded by Lm22;
A5: dom (exp_R(#)(cos - sin)) = dom exp_R /\ dom (cos - sin) by VALUED_1:def 4
.= REAL /\ dom (cos - sin) by SIN_COS:47
.= REAL by A2;
(exp_R(#)cos) is_differentiable_on REAL by A1,FDIFF_7:45;
then dom ((exp_R(#)cos)`|REAL) = dom (exp_R(#)(cos - sin)) by A5,
FDIFF_1:def 7;
then ((exp_R(#)cos)`|REAL) = exp_R(#)(cos - sin) by A3,PARTFUN1:5;
hence thesis by A4,A1,FDIFF_7:45,INTEGRA5:13;
end;