:: Several Integrability Formulas of Special Functions -- Part {II}
:: by Bo Li , Yanping Zhuang , Yanhong Men and Xiquan Liang
::
:: Received October 14, 2008
:: Copyright (c) 2008-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 REAL_1, SUBSET_1, NUMBERS, INTEGRA1, RCOMP_1, RELAT_1, JGRAPH_2,
ARYTM_3, CARD_1, SIN_COS, VALUED_1, ARYTM_1, FDIFF_1, FUNCT_1, SQUARE_1,
PREPOWER, SIN_COS2, ORDINAL2, XXREAL_2, XXREAL_1, INTEGRA5, XBOOLE_0,
PARTFUN1, TARSKI, ORDINAL4, SIN_COS4, SIN_COS9, XXREAL_0, TAYLOR_1,
SIN_COS6, SEQ_4, MEASURE5;
notations TARSKI, XBOOLE_0, FUNCT_1, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS,
RELAT_1, VALUED_1, XXREAL_0, XCMPLX_0, REAL_1, XREAL_0, PARTFUN1,
PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5,
PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, SIN_COS2, FDIFF_9, SIN_COS4,
SIN_COS6, SIN_COS9, SEQ_4;
constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER,
INTEGRA5, SIN_COS2, SEQ_4, SIN_COS9, PARTFUN2, SIN_COS6, RFUNCT_1,
FDIFF_9, SIN_COS4, RELSET_1, INTEGRA1, COMSEQ_2, COMPLEX1, SERIES_1,
BINOP_2;
registrations VALUED_1, NAT_1, NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1,
ORDINAL1, FUNCT_2, RCOMP_1, FCONT_1, TOPREALB, FCONT_3, MEASURE5,
XREAL_0, SIN_COS, PREPOWER, SQUARE_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SIN_COS, VALUED_1, SUBSET_1, SQUARE_1, SIN_COS4, FDIFF_9, XBOOLE_0;
theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, FUNCT_2, SQUARE_1, XCMPLX_1,
INTEGRA5, INTEGRA8, SIN_COS, FDIFF_4, TAYLOR_1, VALUED_1, FCONT_1,
SIN_COS5, SIN_COS4, SIN_COS2, SIN_COS6, XXREAL_1, XBOOLE_1, FDIFF_5,
FDIFF_7, FDIFF_8, FDIFF_9, SIN_COS9, PREPOWER, FDIFF_6, XREAL_0;
begin :: Differentiation Formulas
reserve r,x,x0,a,b for Real;
reserve n,m for Element of NAT;
reserve A for non empty closed_interval Subset of REAL;
reserve Z for open Subset of REAL;
Lm1: [#]REAL = dom (AffineMap(1/2,0)) by FUNCT_2:def 1;
Lm2: [#]REAL = dom (sin*AffineMap(2,0)) by FUNCT_2:def 1;
Lm3: dom ((1/4)(#)(sin*AffineMap(2,0)))=[#]REAL by FUNCT_2:def 1;
:: f.x = (1/2)*x-(1/4)*sin(2*x)
theorem Th1:
AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))
is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)-(1/4)(#)(sin*
AffineMap(2,0)))`|REAL).x = (sin.x)^2
proof
A1: for x st x in REAL holds AffineMap(2,0).x=2*x + 0 by FCONT_1:def 4;
then
A2: sin*AffineMap(2,0) is_differentiable_on REAL by Lm2,FDIFF_4:37;
then
A3: (1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by Lm3,FDIFF_1:20;
A4: dom (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))) = [#]REAL by
FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(1/2,0).x=(1/2)*x + 0 by FCONT_1:def 4;
then
A6: AffineMap(1/2,0) is_differentiable_on REAL by Lm1,FDIFF_1:23;
hence AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))
is_differentiable_on REAL by A4,A3,FDIFF_1:19;
A7: for x st x in REAL holds (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/2)
*cos(2*x)
proof
let x;
assume
A8: x in REAL;
(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/4)*diff((sin*AffineMap(2,
0)),x) by A2,Lm3,FDIFF_1:20,A8
.=(1/4)*((sin*AffineMap(2,0))`|REAL).x by A2,FDIFF_1:def 7,A8
.=(1/4)*(2*cos.(2*x+0)) by A1,Lm2,FDIFF_4:37,A8
.=(1/2)*cos(2*x);
hence thesis;
end;
A9:
for x st x in REAL holds ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))
)`|REAL).x = (sin.x)^2
proof
let x;
assume
A10: x in REAL;
((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =diff(
AffineMap(1/2,0),x) - diff((1/4)(#)(sin*AffineMap(2,0)),x) by A4,A6,A3,
FDIFF_1:19,A10
.=((AffineMap(1/2,0))`|REAL).x -diff((1/4)(#)(sin*AffineMap(2,0)),x)
by A6,FDIFF_1:def 7,A10
.=(1/2)-diff((1/4)(#)(sin*AffineMap(2,0)),x) by A5,Lm1,FDIFF_1:23,A10
.=(1/2)-(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x by A3,FDIFF_1:def 7,A10
.=(1/2)-(1/2)*cos(2*x) by A7,A10
.=(1-cos(2*x))/2
.=(sin(x))^2 by SIN_COS5:20;
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A9;
end;
:: f.x = (1/2)*x+(1/4)*sin(2*x)
theorem Th2:
AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))
is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)+(1/4)(#)(sin*
AffineMap(2,0)))`|REAL).x = (cos.x)^2
proof
A1: for x st x in REAL holds AffineMap(2,0).x=2*x + 0 by FCONT_1:def 4;
then
A2: sin*AffineMap(2,0) is_differentiable_on REAL by Lm2,FDIFF_4:37;
then
A3: (1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by Lm3,FDIFF_1:20;
A4: dom (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))) = [#]REAL by
FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(1/2,0).x=(1/2)*x + 0 by FCONT_1:def 4;
then
A6: AffineMap(1/2,0) is_differentiable_on REAL by Lm1,FDIFF_1:23;
hence AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))
is_differentiable_on REAL by A4,A3,FDIFF_1:18;
A7: for x st x in REAL holds (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/2)
*cos(2*x)
proof
let x;
assume
A8: x in REAL;
(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/4)*diff((sin*AffineMap(2,
0)),x) by A2,Lm3,FDIFF_1:20,A8
.=(1/4)*((sin*AffineMap(2,0))`|REAL).x by A2,FDIFF_1:def 7,A8
.=(1/4)*(2*cos.(2*x+0)) by A1,Lm2,FDIFF_4:37,A8
.=(1/2)*cos(2*x);
hence thesis;
end;
A9:
for x st x in REAL holds ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))
)`|REAL).x = (cos.x)^2
proof
let x;
assume
A10: x in REAL;
((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =diff(
AffineMap(1/2,0),x) + diff((1/4)(#)(sin*AffineMap(2,0)),x) by A4,A6,A3,
FDIFF_1:18,A10
.=((AffineMap(1/2,0))`|REAL).x +diff((1/4)(#)(sin*AffineMap(2,0)),x)
by A6,FDIFF_1:def 7,A10
.=(1/2)+diff((1/4)(#)(sin*AffineMap(2,0)),x) by A5,Lm1,FDIFF_1:23,A10
.=(1/2)+(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x by A3,FDIFF_1:def 7,A10
.=(1/2)+(1/2)*cos(2*x) by A7,A10
.=(1+cos(2*x))/2
.=(cos(x))^2 by SIN_COS5:21;
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A9;
end;
:: f.x = (1/(n+1))*(sin.x)^(n+1)
theorem Th3:
(1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL & for x
holds (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x = ((sin.x) #Z n)*cos.x
proof
A1: [#]REAL = dom((1/(n+1))(#)( #Z (n+1)*sin)) by FUNCT_2:def 1;
#Z (n+1)*sin is_differentiable_in x0
proof
sin is_differentiable_in x0 by SIN_COS:64;
hence thesis by TAYLOR_1:3;
end;
then
[#]REAL = dom ( #Z (n+1)*sin) & for x0 st x0 in REAL holds #Z (n+1)*sin
is_differentiable_in x0 by FUNCT_2:def 1;
then
A2: #Z (n+1)*sin is_differentiable_on REAL by FDIFF_1:9;
hence (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL by A1,FDIFF_1:20;
A3: for x st x in REAL holds (( #Z (n+1)*sin)`|REAL).x=(n+1) * ((sin.x) #Z n
)*cos.x
proof
set m=n+1;
let x;
assume
A4: x in REAL;
sin is_differentiable_in x by SIN_COS:64;
then diff(( #Z m*sin),x) = m * (sin.x) #Z (m-1) *diff(sin,x) by TAYLOR_1:3
.= m * (sin.x) #Z (m-1) *(cos .x) by SIN_COS:64;
hence thesis by A2,FDIFF_1:def 7,A4;
end;
A5:
for x st x in REAL holds (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(sin.x
) #Z n *cos.x
proof
let x;
assume
A6: x in REAL;
(((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(1/(n+1))*diff( #Z (n+1)*sin
,x) by A1,A2,FDIFF_1:20,A6
.=(1/(n+1))*((( #Z (n+1)*sin)`|REAL).x) by A2,FDIFF_1:def 7,A6
.=(1/(n+1))*((n+1) * (sin.x) #Z n *cos.x) by A3,A6
.=(1/(n+1))*(n+1) * (sin.x) #Z n *cos.x
.=(n+1)/(n+1) * (sin.x) #Z n *cos.x by XCMPLX_1:99
.=1*(sin.x) #Z n *cos.x by XCMPLX_1:60;
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A5;
end;
:: f.x = (-1/(n+1))*(cos.x)^(n+1)
theorem Th4:
(-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL & for x
holds (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x = ((cos.x) #Z n)*sin.x
proof
A1: [#]REAL = dom((-1/(n+1))(#)( #Z (n+1)*cos)) by FUNCT_2:def 1;
#Z (n+1)*cos is_differentiable_in x0
proof
cos is_differentiable_in x0 by SIN_COS:63;
hence thesis by TAYLOR_1:3;
end;
then
A2: for x0 st x0 in REAL holds #Z (n+1)*cos is_differentiable_in x0;
[#]REAL = dom ( #Z (n+1)) & REAL = dom ( #Z (n+1)*cos) by FUNCT_2:def 1;
then
A3: #Z (n+1)*cos is_differentiable_on REAL by A2,FDIFF_1:9;
hence(-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL by A1,FDIFF_1:20;
A4: for x st x in REAL holds (( #Z (n+1)*cos)`|REAL).x=(-(n+1)) * ((cos.x)
#Z n)*sin.x
proof
set m=n+1;
let x;
assume
A5:x in REAL;
cos is_differentiable_in x by SIN_COS:63;
then diff(( #Z m*cos),x) = m * (cos.x) #Z (m-1) *diff(cos,x) by TAYLOR_1:3
.= m * (cos.x) #Z (m-1) *(-sin .x) by SIN_COS:63
.= (-m) * (cos.x) #Z (m-1) *sin .x;
hence thesis by A3,FDIFF_1:def 7,A5;
end;
A6:
for x st x in REAL holds (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(cos
.x) #Z n *sin.x
proof
let x;
assume
A7:x in REAL;
(((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(-1/(n+1))*diff( #Z (n+1)*
cos,x) by A1,A3,FDIFF_1:20,A7
.=(-1/(n+1))*((( #Z (n+1)*cos)`|REAL).x) by A3,FDIFF_1:def 7,A7
.=(-1/(n+1))*((-(n+1)) * (cos.x) #Z n *sin.x) by A4,A7
.=(1/(n+1))*(n+1) * (cos.x) #Z n *sin.x
.=(n+1)/(n+1) * (cos.x) #Z n *sin.x by XCMPLX_1:99
.=1*(cos.x) #Z n *sin.x by XCMPLX_1:60;
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A6;
end;
:: f.x=sin.((m+n)*x)/(2*(m+n))+sin.((m-n)*x)/(2*(m-n))
theorem Th5:
m+n<>0 & m-n<>0 implies ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
(1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) is_differentiable_on REAL & for x holds
(((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)
))`|REAL).x = cos.(m*x) *cos.(n*x)
proof
assume that
A1: m+n <> 0 and
A2: m-n<>0;
A3: dom (sin*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds
AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A4: sin*AffineMap(m-n,0) is_differentiable_on REAL by FDIFF_4:37;
A5: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
then
A6: (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)) is_differentiable_on REAL by A4,
FDIFF_1:20;
A7: for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|
REAL).x=(1/2)*cos((m-n)*x)
proof
let x;
assume
A8: x in REAL;
(((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))*
diff((sin*AffineMap(m-n,0)),x) by A5,A4,FDIFF_1:20,A8
.=(1/(2*(m-n)))*((sin*AffineMap(m-n,0))`|REAL).x by A4,FDIFF_1:def 7,A8
.=(1/(2*(m-n)))*((m-n)* cos.((m-n)*x+0)) by A3,FDIFF_4:37,A8
.=(m-n)*(1/(2*(m-n)))* cos.((m-n)*x+0)
.=((1*(m-n))/(2*(m-n)))* cos.((m-n)*x+0) by XCMPLX_1:74
.=(1/2)* cos((m-n)*x) by A2,XCMPLX_1:91;
hence thesis;
end;
A9: dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
A10: dom (sin*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds
AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A11: sin*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:37;
A12: [#]REAL = dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) by FUNCT_2:def 1;
then
A13: (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)) is_differentiable_on REAL by A11,
FDIFF_1:20;
hence((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
(1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) is_differentiable_on REAL
by A9,A6,FDIFF_1:18;
A14: for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL
).x=(1/2)*cos((m+n)*x)
proof
let x;
assume
A15: x in REAL;
(((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x =(1/(2*(m+n)))*
diff((sin*AffineMap(m+n,0)),x) by A12,A11,FDIFF_1:20,A15
.=(1/(2*(m+n)))*((sin*AffineMap(m+n,0))`|REAL).x by A11,FDIFF_1:def 7,A15
.=(1/(2*(m+n)))*((m+n)* cos.((m+n)*x+0)) by A10,FDIFF_4:37,A15
.=(m+n)*(1/(2*(m+n)))* cos.((m+n)*x+0)
.=((1*(m+n))/(2*(m+n)))* cos.((m+n)*x+0) by XCMPLX_1:74
.=(1/2)* cos((m+n)*x) by A1,XCMPLX_1:91;
hence thesis;
end;
A16:
for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(
2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x = cos.(m*x) *cos.(n*x)
proof
let x;
assume
A17: x in REAL;
(((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0)))`|REAL).x = diff((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)),x) +
diff((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)),x) by A9,A13,A6,FDIFF_1:18,A17
.= (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x +diff((1/(2*(m-n
)))(#)(sin*AffineMap(m-n,0)),x) by A13,FDIFF_1:def 7,A17
.= (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x +(((1/(2*(m-n)))
(#)(sin*AffineMap(m-n,0)))`|REAL).x by A6,FDIFF_1:def 7,A17
.= (1/2)*cos((m+n)*x)+(((1/(2*(m-n))) (#)(sin*AffineMap(m-n,0)))`|REAL
).x by A14,A17
.= (1/2)*cos((m+n)*x)+(1/2)* cos((m-n)*x) by A7,A17
.= (1/2)*(cos((m+n)*x)+cos((m-n)*x))
.= (1/2)*(2*(cos(((m+n)*x+(m-n)*x)/2) *cos(((m+n)*x-(m-n)*x)/2))) by
SIN_COS4:17
.= cos.(m*x)*cos.(n*x);
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A16;
end;
:: f.x=sin.((m-n)*x)/(2*(m-n))-sin.((m+n)*x)/(2*(m+n))
theorem Th6:
m+n<>0 & m-n<>0 implies ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
(1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) is_differentiable_on REAL & for x holds
(((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)
))`|REAL).x = sin.(m*x)*sin.(n*x)
proof
assume that
A1: m+n <> 0 and
A2: m-n <> 0;
A3: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
A4: dom (sin*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds
AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A5: sin*AffineMap(m-n,0) is_differentiable_on REAL by FDIFF_4:37;
then
A6: (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)) is_differentiable_on REAL by A3,
FDIFF_1:20;
A7: for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|
REAL).x=(1/2)*cos((m-n)*x)
proof
let x;
assume
A8: x in REAL;
(((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))*
diff((sin*AffineMap(m-n,0)),x) by A3,A5,FDIFF_1:20,A8
.=(1/(2*(m-n)))*((sin*AffineMap(m-n,0))`|REAL).x by A5,FDIFF_1:def 7,A8
.=(1/(2*(m-n)))*((m-n)* cos.((m-n)*x+0)) by A4,FDIFF_4:37,A8
.=(m-n)*(1/(2*(m-n)))* cos.((m-n)*x+0)
.=((1*(m-n))/(2*(m-n)))* cos.((m-n)*x+0) by XCMPLX_1:74
.=(1/2)* cos((m-n)*x) by A2,XCMPLX_1:91;
hence thesis;
end;
A9: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1;
A10: dom (sin*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds
AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A11: sin*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:37;
A12: REAL = dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) by FUNCT_2:def 1;
then
A13: (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)) is_differentiable_on REAL by A3,A11
,FDIFF_1:20;
hence ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
(1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) is_differentiable_on REAL
by A9,A6,FDIFF_1:19;
A14: for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL
).x=(1/2)*cos((m+n)*x)
proof
let x;
assume
A15: x in REAL;
(((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x =(1/(2*(m+n)))*
diff((sin*AffineMap(m+n,0)),x) by A12,A3,A11,FDIFF_1:20,A15
.=(1/(2*(m+n)))*((sin*AffineMap(m+n,0))`|REAL).x by A11,FDIFF_1:def 7,A15
.=(1/(2*(m+n)))*((m+n)* cos.((m+n)*x+0)) by A10,FDIFF_4:37,A15
.=(m+n)*(1/(2*(m+n)))* cos.((m+n)*x+0)
.=((1*(m+n))/(2*(m+n)))* cos.((m+n)*x+0) by XCMPLX_1:74
.=(1/2)* cos((m+n)*x) by A1,XCMPLX_1:91;
hence thesis;
end;
A16:
for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(
2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x = sin.(m*x) *sin.(n*x)
proof
let x;
assume
A17: x in REAL;
(((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0)))`|REAL).x = diff((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)),x) -
diff((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)),x) by A9,A13,A6,FDIFF_1:19,A17
.= (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x -diff((1/(2*(m+n
)))(#)(sin*AffineMap(m+n,0)),x) by A6,FDIFF_1:def 7,A17
.= (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x -(((1/(2*(m+n)))
(#)(sin*AffineMap(m+n,0)))`|REAL).x by A13,FDIFF_1:def 7,A17
.= (1/2)*cos((m-n)*x)-(((1/(2*(m+n))) (#)(sin*AffineMap(m+n,0)))`|REAL
).x by A7,A17
.= (1/2)*cos((m-n)*x)-(1/2)* cos((m+n)*x) by A14,A17
.= (1/2)*(cos((m-n)*x)-cos((m+n)*x))
.= (1/2)*(-2*(sin(((m-n)*x+(m+n)*x)/2) *sin(((m-n)*x-(m+n)*x)/2))) by
SIN_COS4:18
.= (1/2)*(-2*(sin(m*x)*sin(-(n*x))))
.= (1/2)*(-2*(sin(m*x)*(-sin(n*x)))) by SIN_COS:31
.= sin.(m*x)*sin.(n*x);
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A16;
end;
:: f.x=-cos.((m+n)*x)/(2*(m+n))-cos.((m-n)*x)/(2*(m-n))
theorem Th7:
m+n<>0 & m-n<>0 implies ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))
) - (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) is_differentiable_on REAL & for x
holds ((-((1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0)))`|REAL).x = sin.(m*x) * cos.(n*x)
proof
assume that
A1: m+n <> 0 and
A2: m-n <> 0;
A3: dom (cos*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds
AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A4: cos*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:38;
A5: for x st x in REAL holds ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|
REAL).x=(1/2)*sin((m+n)*x)
proof
let x;
assume
A6: x in REAL;
A7: dom (((-1)/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))=[#]REAL by FUNCT_2:def 1;
((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x =((((-1)*(1/(2*(m
+n)))) (#)(cos*AffineMap(m+n,0)))`|REAL).x by RFUNCT_1:17
.=(((-(1/(2*(m+n))))(#)(cos*AffineMap(m+n,0)))`|REAL).x
.=((((-1)/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x by XCMPLX_1:187
.=((-1)/(2*(m+n)))*diff((cos*AffineMap(m+n,0)),x) by A4,A7,FDIFF_1:20,A6
.=((-1)/(2*(m+n)))*((cos*AffineMap(m+n,0))`|REAL).x by A4,FDIFF_1:def 7,
A6
.=((-1)/(2*(m+n)))*(-(m+n)* sin.((m+n)*x+0)) by A3,FDIFF_4:38,A6
.=(-(-1)/(2*(m+n)))*(m+n)* sin.((m+n)*x+0)
.=(1/(2*(m+n)))*(m+n)* sin.((m+n)*x+0) by XCMPLX_1:190
.=((1*(m+n))/(2*(m+n)))* sin.((m+n)*x+0) by XCMPLX_1:74
.=(1/2)* sin((m+n)*x) by A1,XCMPLX_1:91;
hence thesis;
end;
A8: dom (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1;
dom ((1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1;
then (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = (-1)(#) ((1/(2*(m+n)))(#)(
cos* AffineMap(m+n,0))) & (1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))
is_differentiable_on REAL by A4,FDIFF_1:20;
then
A9: (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) is_differentiable_on REAL by A8,
FDIFF_1:20;
A10: REAL = dom ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(
cos*AffineMap(m-n,0))) by FUNCT_2:def 1;
A11: dom (cos*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds
AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A12: cos*(AffineMap(m-n,0)) is_differentiable_on REAL by FDIFF_4:38;
A13: dom ((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1;
then
A14: (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)) is_differentiable_on REAL by A12,
FDIFF_1:20;
hence ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))
) - (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) is_differentiable_on REAL
by A8,A10,A9,FDIFF_1:19;
A15: for x st x in REAL holds (((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|
REAL).x=-(1/2)*sin((m-n)*x)
proof
let x;
assume
A16: x in REAL;
(((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))*
diff((cos*AffineMap(m-n,0)),x) by A13,A12,FDIFF_1:20,A16
.=(1/(2*(m-n)))*((cos*AffineMap(m-n,0))`|REAL).x by A12,FDIFF_1:def 7,A16
.=(1/(2*(m-n)))*(-(m-n)* sin.((m-n)*x+0)) by A11,FDIFF_4:38,A16
.=(-1/(2*(m-n)))*(m-n)* sin.((m-n)*x+0)
.=((-1)/(2*(m-n)))*(m-n)* sin.((m-n)*x+0) by XCMPLX_1:187
.=(((-1)*(m-n))/(2*(m-n)))* sin.((m-n)*x+0) by XCMPLX_1:74
.=(-1)/2* sin((m-n)*x) by A2,XCMPLX_1:91;
hence thesis;
end;
A17:
for x st x in REAL holds ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))- (1/
(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x = sin.(m*x) *cos.(n*x)
proof
let x;
assume
A18: x in REAL;
((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0)))`|REAL).x = diff((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))),x)
-diff((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)),x)
by A8,A10,A9,A14,FDIFF_1:19,A18
.= ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x -diff((1/(2*(m-
n)))(#)(cos*AffineMap(m-n,0)),x) by A9,FDIFF_1:def 7,A18
.= ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x -(((1/(2*(m-n))
)(#)(cos*AffineMap(m-n,0)))`|REAL).x by A14,FDIFF_1:def 7,A18
.= (1/2)*sin((m+n)*x)-(((1/(2*(m-n))) (#)(cos*AffineMap(m-n,0)))`|REAL
).x by A5,A18
.= (1/2)*sin((m+n)*x)-(-(1/2)* sin((m-n)*x)) by A15,A18
.= (1/2)*(sin((m+n)*x)+sin((m-n)*x))
.= (1/2)*(2*(cos(((m+n)*x-(m-n)*x)/2) *sin(((m+n)*x+(m-n)*x)/2))) by
SIN_COS4:15
.= sin.(m*x)*cos.(n*x);
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A17;
end;
:: f.x = (1/(n^2))*sin.(n*x)-(1/n)*x*cos.(n*x)
theorem Th8:
n<>0 implies ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0)
)(#)(cos*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2))
(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x=x*
sin.(n*x)
proof
A1: dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
AffineMap(n,0)))) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1/n,0))=REAL & for x st x in REAL holds AffineMap(1/n,0)
.x=(1 /n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A3: AffineMap(1/n,0) is_differentiable_on REAL by A1,FDIFF_1:23;
A4: for x st x in REAL holds AffineMap(n,0).x=n*x + 0 by FCONT_1:def 4;
A5: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
then
A6: sin*(AffineMap(n,0)) is_differentiable_on REAL by A4,FDIFF_4:37;
A7: dom ((1/(n^2))(#)(sin*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
then
A8: (1/(n^2))(#)(sin*AffineMap(n,0)) is_differentiable_on REAL by A1,A6,
FDIFF_1:20;
assume
A9: n<>0;
A10: for x st x in REAL holds (((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x =
(1/n)*cos(n*x)
proof
let x;
assume
A11: x in REAL;
(((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x =(1/(n^2))*diff((sin*
AffineMap(n,0)),x) by A7,A1,A6,FDIFF_1:20,A11
.=(1/(n^2))*((sin*AffineMap(n,0))`|REAL).x by A6,FDIFF_1:def 7,A11
.=(1/(n^2))*(n * cos.(n*x+0)) by A5,A4,FDIFF_4:37,A11
.= n*(1/(n*n))*(cos.(n*x+0))
.= (n*1)/(n*n)*(cos.(n*x+0)) by XCMPLX_1:74
.= (1/n)*(cos.(n*x+0)) by A9,XCMPLX_1:91;
hence thesis;
end;
A12: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
then
A13: cos*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:38;
A14: dom ((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
then
A15: ((AffineMap(1/n,0))(#)(cos*AffineMap(n,0))) is_differentiable_on REAL
by A1,A3,A13,FDIFF_1:21;
hence ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0)
)(#)(cos*AffineMap(n,0))) is_differentiable_on REAL
by A1,A8,FDIFF_1:19;
A16: for x st x in REAL holds (((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|
REAL).x = (1/n)*cos.(n*x)-x* sin.(n*x)
proof
let x;
assume
A17: x in REAL;
(((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = ((cos*
AffineMap(n,0)).x)*diff(AffineMap(1/n,0),x) + (AffineMap(1/n,0).x)*diff(cos*(
AffineMap(n,0)),x) by A14,A1,A3,A13,FDIFF_1:21,A17
.= ((cos*AffineMap(n,0)).x)*((AffineMap(1/n,0)`|REAL).x) +(AffineMap(1
/n,0).x)*diff((cos*AffineMap(n,0)),x) by A3,FDIFF_1:def 7,A17
.= ((cos*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *diff((cos*
AffineMap(n,0)),x) by A1,A2,FDIFF_1:23,A17
.= ((cos*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *(((cos*
AffineMap(n,0))`|REAL).x) by A13,FDIFF_1:def 7,A17
.= ((cos*AffineMap(n,0)).x)*(1/n) +(AffineMap(1/n,0).x)*(-n* sin.(n*x+
0)) by A12,A4,FDIFF_4:38,A17
.= ((cos*AffineMap(n,0)).x)*(1/n) +((1/n)*x + 0)*(-n* sin.(n*x+0)) by
FCONT_1:def 4
.= (cos.(AffineMap(n,0).x))*(1/n) +((1/n)*x)*(-n* sin.(n*x+0)) by A12,
FUNCT_1:12,A17
.= (1/n)*cos.(n*x)+(-((1/n)*n*x* sin.(n*x))) by FCONT_1:def 4
.= (1/n)*cos.(n*x)+(-(1*x* sin.(n*x))) by A9,XCMPLX_1:87
.= (1/n)*cos.(n*x)-x* sin.(n*x);
hence thesis;
end;
A18:
for x st x in REAL holds (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap
(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = x*sin.(n*x)
proof
let x;
assume
A19: x in REAL;
(((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
AffineMap(n,0)))`|REAL).x = diff((1/(n^2))(#)(sin*AffineMap(n,0)),x) - diff((
AffineMap(1/n,0))(#)(cos*AffineMap(n,0)),x) by A1,A8,A15,FDIFF_1:19,A19
.= ((((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x) - diff(AffineMap(1/n
,0)(#)(cos*AffineMap(n,0)),x) by A8,FDIFF_1:def 7,A19
.= (1/n)*cos(n*x)-diff(AffineMap(1/n,0) (#)(cos*AffineMap(n,0)),x)
by A10,A19
.= (1/n)*cos(n*x)-(((AffineMap(1/n,0) (#)(cos*AffineMap(n,0)))`|REAL).
x) by A15,FDIFF_1:def 7,A19
.= (1/n)*cos(n*x)-((1/n)*cos.(n*x)-x* sin.(n*x)) by A16,A19
.= x* sin.(n*x);
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A18;
end;
:: f.x = (1/(n^2))*cos.(n*x)+(1/n)*x*sin.(n*x)
theorem Th9:
n<>0 implies ((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0)
)(#)(sin*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2))
(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x=x*
cos.(n*x)
proof
A1: dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
AffineMap(n,0)))) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1/n,0))=REAL & for x st x in REAL holds AffineMap(1/n,0)
.x=(1 /n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A3: AffineMap(1/n,0) is_differentiable_on REAL by A1,FDIFF_1:23;
A4: for x st x in REAL holds AffineMap(n,0).x=n*x + 0 by FCONT_1:def 4;
A5: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
then
A6: cos*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:38;
A7: dom ((1/(n^2))(#)(cos*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
then
A8: (1/(n^2))(#)(cos*AffineMap(n,0)) is_differentiable_on REAL by A1,A6,
FDIFF_1:20;
assume
A9: n<>0;
A10: for x st x in REAL holds (((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x =
-(1/n)*sin(n*x)
proof
let x;
assume
A11: x in REAL;
(((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x =(1/(n^2))*diff((cos*
AffineMap(n,0)),x) by A7,A1,A6,FDIFF_1:20,A11
.=(1/(n^2))*((cos*AffineMap(n,0))`|REAL).x by A6,FDIFF_1:def 7,A11
.=(1/(n^2))*(-n * sin.(n*x+0)) by A5,A4,FDIFF_4:38,A11
.=(-1)*(n*(1/(n*n)))*(sin.(n*x+0))
.=(-1)*(n/((n*n)/1))*(sin.(n*x+0)) by XCMPLX_1:79
.=(-1)*((n*1)/(n*n))*(sin.(n*x+0))
.=(-1)*(1/n)*(sin.(n*x+0)) by A9,XCMPLX_1:91;
hence thesis;
end;
A12: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
then
A13: sin*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:37;
A14: dom ((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))=REAL by FUNCT_2:def 1;
then
A15: ((AffineMap(1/n,0))(#)(sin*AffineMap(n,0))) is_differentiable_on REAL
by A1,A3,A13,FDIFF_1:21;
hence((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0)
)(#)(sin*AffineMap(n,0))) is_differentiable_on REAL
by A1,A8,FDIFF_1:18;
A16: for x st x in REAL holds (((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|
REAL).x = (1/n)*sin.(n*x)+x* cos.(n*x)
proof
let x;
assume
A17: x in REAL;
(((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = ((sin*
AffineMap(n,0)).x)*diff((AffineMap(1/n,0)),x) + ((AffineMap(1/n,0)).x)*diff((
sin*AffineMap(n,0)),x) by A14,A1,A3,A13,FDIFF_1:21,A17
.= ((sin*AffineMap(n,0)).x)*((AffineMap(1/n,0)`|REAL).x) +((AffineMap(
1/n,0)).x)*diff((sin*AffineMap(n,0)),x) by A3,FDIFF_1:def 7,A17
.= ((sin*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *diff((sin*
AffineMap(n,0)),x) by A1,A2,FDIFF_1:23,A17
.= ((sin*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *(((sin*
AffineMap(n,0))`|REAL).x) by A13,FDIFF_1:def 7,A17
.= ((sin*AffineMap(n,0)).x)*(1/n) +(AffineMap(1/n,0).x)*(n* cos.(n*x+0
)) by A12,A4,FDIFF_4:37,A17
.= ((sin*AffineMap(n,0)).x)*(1/n) +((1/n)*x + 0)*(n* cos.(n*x+0)) by
FCONT_1:def 4
.= (sin.(AffineMap(n,0).x))*(1/n) +((1/n)*x)*(n* cos.(n*x+0)) by A12,
FUNCT_1:12,A17
.= (1/n)*sin.(n*x)+(1/n)*n*x* cos.(n*x) by FCONT_1:def 4
.= (1/n)*sin.(n*x)+1*x* cos.(n*x) by A9,XCMPLX_1:87
.= (1/n)*sin.(n*x)+x* cos.(n*x);
hence thesis;
end;
A18:
for x st x in REAL holds (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap
(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = x*cos.(n*x)
proof
let x;
assume
A19: x in REAL;
(((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
AffineMap(n,0)))`|REAL).x = diff((1/(n^2))(#)(cos*AffineMap(n,0)),x) + diff((
AffineMap(1/n,0))(#)(sin*AffineMap(n,0)),x) by A1,A8,A15,FDIFF_1:18,A19
.= ((((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x) + diff((AffineMap(1/
n,0))(#)(sin*AffineMap(n,0)),x) by A8,FDIFF_1:def 7,A19
.= -(1/n)*sin(n*x)+diff(AffineMap(1/n,0) (#)(sin*AffineMap(n,0)),x) by
A10,A19
.= -(1/n)*sin(n*x)+(((AffineMap(1/n,0) (#)(sin*AffineMap(n,0)))`|REAL)
.x) by A15,FDIFF_1:def 7,A19
.= -(1/n)*sin(n*x)+((1/n)*sin.(n*x)+x* cos.(n*x)) by A16,A19
.= x* cos.(n*x);
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A18;
end;
:: f.x = x*cosh.x-sinh.x
theorem Th10:
(AffineMap(1,0))(#)cosh-sinh is_differentiable_on REAL & for x
holds (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x=x*sinh.x
proof
A1: dom ((AffineMap(1,0))(#)cosh-sinh) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
.x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A3: AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
A4: dom ((AffineMap(1,0))(#)cosh) = [#]REAL by FUNCT_2:def 1;
then
A5: ((AffineMap(1,0))(#)cosh) is_differentiable_on REAL by A3,FDIFF_1:21
,SIN_COS2:35;
hence (AffineMap(1,0))(#)cosh-sinh is_differentiable_on REAL
by A1,FDIFF_1:19,SIN_COS2:34;
A6: for x st x in REAL holds (((AffineMap(1,0))(#)cosh)`|REAL).x = cosh.x+x*
sinh.x
proof
let x;
assume
A7: x in REAL;
(((AffineMap(1,0))(#)cosh)`|REAL).x = cosh.x*diff((AffineMap(1,0)),x)+
((AffineMap(1,0)).x) *diff(cosh,x) by A4,A3,FDIFF_1:21,SIN_COS2:35,A7
.= cosh.x*(((AffineMap(1,0))`|REAL).x) +((AffineMap(1,0)).x)*diff(cosh
,x) by A3,FDIFF_1:def 7,A7
.= cosh.x*1+((AffineMap(1,0)).x)*diff(cosh,x) by A2,FDIFF_1:23,A7
.= cosh.x+((AffineMap(1,0)).x)*sinh.x by SIN_COS2:35
.= cosh.x+(1*x + 0)*sinh.x by FCONT_1:def 4
.= cosh.x+x*sinh.x;
hence thesis;
end;
A8:
for x st x in REAL holds (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x = x* sinh.x
proof
let x;
assume
A9: x in REAL;
(((AffineMap(1,0))(#)cosh - sinh)`|REAL).x = diff(((AffineMap(1,0))(#)
cosh),x) - diff(sinh,x) by A1,A5,FDIFF_1:19,SIN_COS2:34,A9
.= (((AffineMap(1,0))(#)cosh)`|REAL).x - diff(sinh,x)
by A5,FDIFF_1:def 7,A9
.= cosh.x+x*sinh.x-diff(sinh,x) by A6,A9
.= cosh.x+x*sinh.x-cosh.x by SIN_COS2:34
.= x*sinh.x;
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A8;
end;
:: f.x = x*sinh.x-cosh.x
theorem Th11:
(AffineMap(1,0))(#)sinh-cosh is_differentiable_on REAL & for x
holds (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x=x*cosh.x
proof
A1: dom ((AffineMap(1,0))(#)sinh-cosh) = [#]REAL by FUNCT_2:def 1;
A2: dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
.x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then
A3: AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
A4: dom ((AffineMap(1,0))(#)sinh) = [#]REAL by FUNCT_2:def 1;
then
A5: ((AffineMap(1,0))(#)sinh) is_differentiable_on REAL by A3,FDIFF_1:21
,SIN_COS2:34;
hence (AffineMap(1,0))(#)sinh-cosh is_differentiable_on REAL
by A1,FDIFF_1:19,SIN_COS2:35;
A6: for x st x in REAL holds (((AffineMap(1,0))(#)sinh)`|REAL).x = sinh.x+x*
cosh.x
proof
let x;
assume
A7: x in REAL;
(((AffineMap(1,0))(#)sinh)`|REAL).x = sinh.x*diff((AffineMap(1,0)),x)+
((AffineMap(1,0)).x) *diff(sinh,x) by A4,A3,FDIFF_1:21,SIN_COS2:34,A7
.= sinh.x*(((AffineMap(1,0))`|REAL).x) +((AffineMap(1,0)).x)*diff(sinh
,x) by A3,FDIFF_1:def 7,A7
.= sinh.x*1+((AffineMap(1,0)).x)*diff(sinh,x) by A2,FDIFF_1:23,A7
.= sinh.x+((AffineMap(1,0)).x)*(cosh.x) by SIN_COS2:34
.= sinh.x+(1*x + 0)*cosh.x by FCONT_1:def 4
.= sinh.x+x*cosh.x;
hence thesis;
end;
A8:
for x st x in REAL holds (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x = x*(
cosh.x)
proof
let x;
assume
A9: x in REAL;
(((AffineMap(1,0))(#)sinh - cosh)`|REAL).x = diff(((AffineMap(1,0))(#)
sinh),x) - diff(cosh,x) by A1,A5,FDIFF_1:19,SIN_COS2:35,A9
.= (((AffineMap(1,0))(#)sinh)`|REAL).x - diff(cosh,x)
by A5,FDIFF_1:def 7,A9
.= sinh.x+x*cosh.x-diff(cosh,x) by A6,A9
.= sinh.x+x*cosh.x-sinh.x by SIN_COS2:35
.= x*cosh.x;
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A8;
end;
:: f.x = (1/(a*(n+1)))*(a*x+b)^(n+1)
theorem Th12:
a*(n+1) <> 0 implies (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))
is_differentiable_on REAL & for x holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(
a,b)))`|REAL).x = (a*x+b) #Z n
proof
assume
A1: a*(n+1) <> 0;
A2: [#]REAL = dom((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))) by FUNCT_2:def 1;
A3: [#]REAL = dom (AffineMap(a,b)) by FUNCT_2:def 1;
A4: for x st x in REAL holds AffineMap(a,b).x=a*x + b by FCONT_1:def 4;
then
A5: AffineMap(a,b) is_differentiable_on REAL by A3,FDIFF_1:23;
#Z (n+1)*AffineMap(a,b) is_differentiable_in x
proof
x in REAL by XREAL_0:def 1;
then AffineMap(a,b) is_differentiable_in x by A3,A5,FDIFF_1:9;
hence thesis by TAYLOR_1:3;
end;
then
[#]REAL = dom ( #Z (n+1)*AffineMap(a,b)) & for x st x in REAL holds #Z (
n+1) *AffineMap(a,b) is_differentiable_in x by FUNCT_2:def 1;
then
A6: #Z (n+1)*AffineMap(a,b) is_differentiable_on REAL by FDIFF_1:9;
hence (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))
is_differentiable_on REAL by A2,FDIFF_1:20;
A7: for x st x in REAL holds (( #Z (n+1)*AffineMap(a,b))`|REAL).x=a*(n+1)*(
AffineMap(a,b).x) #Z n
proof
set m=n+1;
let x;
assume
A8: x in REAL;
AffineMap(a,b) is_differentiable_in x by A3,A5,FDIFF_1:9,A8;
then diff(( #Z m*AffineMap(a,b)),x) = m * (AffineMap(a,b).x) #Z (m-1) *
diff(AffineMap(a,b),x) by TAYLOR_1:3
.= m * (AffineMap(a,b).x) #Z (m-1) * ((AffineMap(a,b))`|REAL).x by A5,
FDIFF_1:def 7,A8
.= m * (AffineMap(a,b).x) #Z (m-1) *a by A3,A4,FDIFF_1:23,A8;
hence thesis by A6,FDIFF_1:def 7,A8;
end;
A9:
for x st x in REAL holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))
`|REAL).x =(a*x+b) #Z n
proof
let x;
assume
A10: x in REAL;
(((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x =(1/(a*(n+1)))
*diff( #Z (n+1)*AffineMap(a,b),x) by A2,A6,FDIFF_1:20,A10
.=(1/(a*(n+1)))*((( #Z (n+1)*AffineMap(a,b))`|REAL).x) by A6,
FDIFF_1:def 7,A10
.=(1/(a*(n+1)))*(a*(n+1) * (AffineMap(a,b).x) #Z n ) by A7,A10
.=(1/(a*(n+1)))*(a*(n+1)) * (AffineMap(a,b).x) #Z n
.=(a*(n+1))/(a*(n+1)) * (AffineMap(a,b).x) #Z n by XCMPLX_1:99
.=1*(AffineMap(a,b).x) #Z n by A1,XCMPLX_1:60
.=(a*x+b) #Z n by FCONT_1:def 4;
hence thesis;
end;
let x;
x in REAL by XREAL_0:def 1;
hence thesis by A9;
end;
begin :: Integrability Formulas
:: f.x = (sin.x)^2
theorem Th13:
integral(sin^2,A) = (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0
))).(upper_bound A) -(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).
(lower_bound A)
proof
A1: for x being Element of REAL
st x in dom ((AffineMap(1/2,0) -(1/4)(#)(sin*AffineMap(2,0)))`|REAL
) holds ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (sin^2).x
proof
let x be Element of REAL;
assume x in dom ((AffineMap(1/2,0) -(1/4)(#)(sin*AffineMap(2,0)))`|REAL);
((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (sin.x)^2
by Th1
.= (sin^2).x by VALUED_1:11;
hence thesis;
end;
A2: dom (sin^2)=REAL by SIN_COS:24,VALUED_1:11;
then
dom ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = dom (sin^2
) by Th1,FDIFF_1:def 7;
then
A3: ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = sin^2 by A1,
PARTFUN1:5;
(sin^2)|A is bounded by A2,INTEGRA5:10;
hence thesis by A2,A3,Th1,INTEGRA5:11,13;
end;
Lm4: dom (AffineMap(2,0)) = [#]REAL by FUNCT_2:def 1;
Lm5: dom (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))=REAL by FUNCT_2:def 1;
reconsider pp = PI as Element of REAL by XREAL_0:def 1;
Lm6: 0 in REAL by XREAL_0:def 1;
theorem
A = [.0,PI.] implies integral(sin^2,A) = PI/2
proof
assume A=[.0,PI.];
then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37;
then
integral(sin^2,A)
=(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).pp -
(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Th13
.= AffineMap(1/2,0).(PI)-((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap
(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Lm5,VALUED_1:13
.= AffineMap(1/2,0).(PI)-((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap
(1/2,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by Lm5,VALUED_1:13,Lm6
.= (1/2)*(PI)+0 -((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap(1/2,0).
0-((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(PI)-(1/4)*(sin*AffineMap(2,0)).pp -(AffineMap(1/2,0).0-((1/4
)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
.= (1/2)*(PI)-(1/4)*(sin.(AffineMap(2,0).(PI))) -(AffineMap(1/2,0).0-((1
/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
.= (1/2)*(PI)-(1/4)*(sin.(2*PI+0)) -(AffineMap(1/2,0).0-((1/4)(#)(sin*
AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(PI)-(1/4)*sin.(2*PI+0) -(0-((1/4)(#)(sin*AffineMap(2,0))).0)
by FCONT_1:48
.= (1/2)*(PI)-(1/4)*sin.(2*PI+0) -0+((1/4)(#)(sin*AffineMap(2,0))).0
.= (1/2)*(PI)-(1/4)*sin.(2*PI+0) +(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
.= (1/2)*(PI)-(1/4)*sin.(2*PI+0) +(1/4)*(sin.(AffineMap(2,0).0)) by Lm4,
FUNCT_1:13,Lm6
.= (1/2)*(PI)-(1/4)*sin.(0+2*PI*1)+(1/4)*sin.0 by FCONT_1:48
.= (1/2)*(PI)-(1/4)*sin.0+(1/4)*sin.0 by SIN_COS6:8
.= PI/2;
hence thesis;
end;
reconsider dp = 2*PI, ddp = 2*(2*PI)+0 as Element of REAL by XREAL_0:def 1;
theorem
A = [.0,2*PI.] implies integral(sin^2,A) = PI
proof
assume A=[.0,2*PI.];
then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
then
integral(sin^2,A)
=(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).dp
-(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Th13
.= AffineMap(1/2,0).(2*PI)-((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(
AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Lm5,VALUED_1:13
.= AffineMap(1/2,0).(2*PI)-((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(
AffineMap(1/2,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by Lm5,VALUED_1:13,Lm6
.= (1/2)*(2*PI)+0 -((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(AffineMap(1/2
,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(2*PI)-(1/4)*(sin*AffineMap(2,0)).(2*PI) -(AffineMap(1/2,0).0-(
(1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
.= (1/2)*(2*PI)-(1/4)*(sin.(AffineMap(2,0).dp)) -(AffineMap(1/2,0).0
-((1/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
.= (1/2)*(2*PI)-(1/4)*(sin.ddp) -(AffineMap(1/2,0).0-((1/4)(#)(
sin*AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) -(0-((1/4)(#)(sin*AffineMap(2,0))).
0) by FCONT_1:48
.= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) -0+((1/4)(#)(sin*AffineMap(2,0))).0
.= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) +(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
.= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) +(1/4)*(sin.(AffineMap(2,0).0))
by Lm4,Lm6
,FUNCT_1:13
.= (1/2)*(2*PI)-(1/4)*sin.(0+2*PI*2)+(1/4)*sin.0 by FCONT_1:48
.= (1/2)*(2*PI)-(1/4)*sin.0+(1/4)*sin.0 by SIN_COS6:8
.= PI;
hence thesis;
end;
:: f.x = (cos.x)^2
theorem Th16:
integral(cos^2,A) = (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0
))).(upper_bound A) -(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).
(lower_bound A)
proof
A1: for x being Element of REAL
st x in dom ((AffineMap(1/2,0) +(1/4)(#)(sin*AffineMap(2,0)))`|
REAL) holds ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (cos^2)
.x
proof
let x be Element of REAL;
assume x in dom ((AffineMap(1/2,0) +(1/4)(#)(sin*AffineMap(2,0)))`|REAL);
((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (cos.x)^2
by Th2
.= (cos^2).x by VALUED_1:11;
hence thesis;
end;
A2: dom (cos^2)=REAL by SIN_COS:24,VALUED_1:11;
then
dom ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = dom (cos^2
) by Th2,FDIFF_1:def 7;
then
A3: ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = cos^2 by A1,
PARTFUN1:5;
(cos^2)|A is bounded by A2,INTEGRA5:10;
hence thesis by A2,A3,Th2,INTEGRA5:11,13;
end;
theorem
A = [.0,PI.] implies integral(cos^2,A) = PI/2
proof
assume A=[.0,PI.];
then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37;
then
integral(cos^2,A)=(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).(PI) -
(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by Th16
.= AffineMap(1/2,0).(PI)+((1/4)(#)(sin*AffineMap(2,0))).pp -(AffineMap
(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by VALUED_1:1
.= AffineMap(1/2,0).(PI)+((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap
(1/2,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:1,Lm6
.= (1/2)*(PI)+0 +((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap(1/2,0).
0+((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(PI)+(1/4)*(sin*AffineMap(2,0)).(PI) -(AffineMap(1/2,0).0+((1/4
)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
.= (1/2)*(PI)+(1/4)*(sin.(AffineMap(2,0).pp)) -(AffineMap(1/2,0).0+((1
/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
.= (1/2)*(PI)+(1/4)*(sin.(2*PI+0)) -(AffineMap(1/2,0).0+((1/4)(#)(sin*
AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(0+((1/4)(#)(sin*AffineMap(2,0))).0)
by FCONT_1:48
.= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
.= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(1/4)*(sin.(AffineMap(2,0).0)) by Lm4,
FUNCT_1:13,Lm6
.= (1/2)*(PI)+(1/4)*sin.(0+2*PI*1)-(1/4)*sin.0 by FCONT_1:48
.= (1/2)*(PI)+(1/4)*sin.0-(1/4)*sin.0 by SIN_COS6:8
.= PI/2;
hence thesis;
end;
theorem
A = [.0,2*PI.] implies integral(cos^2,A) = PI
proof
assume A=[.0,2*PI.];
then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
then
integral(cos^2,A)=(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).(2*PI)
-(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by Th16
.= AffineMap(1/2,0).(2*PI)+((1/4)(#)(sin*AffineMap(2,0))).dp -(
AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by VALUED_1:1
.= AffineMap(1/2,0).(2*PI)+((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(
AffineMap(1/2,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:1,Lm6
.= (1/2)*(2*PI)+0 +((1/4)(#)(sin*AffineMap(2,0))).dp -(AffineMap(1/2
,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(2*PI)+(1/4)*(sin*AffineMap(2,0)).(2*PI) -(AffineMap(1/2,0).0+(
(1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6
.= (1/2)*(2*PI)+(1/4)*(sin.(AffineMap(2,0).dp)) -(AffineMap(1/2,0).0
+((1/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13
.= (1/2)*(2*PI)+(1/4)*(sin.ddp) -(AffineMap(1/2,0).0+((1/4)(#)(
sin*AffineMap(2,0))).0) by FCONT_1:def 4
.= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(0+((1/4)(#)(sin*AffineMap(2,0))).
0) by FCONT_1:48
.= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(1/4)*(sin*AffineMap(2,0)).0 by
VALUED_1:6
.= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(1/4)*(sin.(AffineMap(2,0).0)) by Lm4
,FUNCT_1:13,Lm6
.= (1/2)*(2*PI)+(1/4)*sin.(0+2*PI*2)-(1/4)*sin.0 by FCONT_1:48
.= (1/2)*(2*PI)+(1/4)*sin.0-(1/4)*sin.0 by SIN_COS6:8
.= PI;
hence thesis;
end;
:: f.x = (sin.x)^n*(cos.x)
theorem Th19:
integral(( #Z n*sin)(#)cos,A) = ((1/(n+1))(#)( #Z (n+1)*sin)).(
upper_bound A) -((1/(n+1))(#)( #Z (n+1)*sin)).(lower_bound A)
proof
A1: [#]REAL = dom (( #Z n*sin)(#)cos) by FUNCT_2:def 1;
A2: for x being Element of REAL
st x in dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) holds (((1/(n+1)
)(#)( #Z (n+1)*sin))`|REAL).x = (( #Z n*sin)(#)cos).x
proof
let x be Element of REAL;
assume x in dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL);
(((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(sin.x) #Z n *cos.x by Th3
.=( #Z n).(sin.x)*cos.x by TAYLOR_1:def 1
.=(( #Zn)*sin).x*cos.x by FUNCT_1:13,SIN_COS:24
.= ((( #Z n)*sin)(#)cos).x by A1,VALUED_1:def 4;
hence thesis;
end;
#Z n*sin is_differentiable_in x0
proof
sin is_differentiable_in x0 by SIN_COS:64;
hence thesis by TAYLOR_1:3;
end;
then dom ( #Z n*sin)=REAL & for x0 st x0 in REAL holds #Z n*sin
is_differentiable_in x0 by FUNCT_2:def 1;
then #Z n*sin is_differentiable_on REAL by A1,FDIFF_1:9;
then
A3: (( #Z n*sin)(#)cos)|REAL is continuous by A1,FDIFF_1:21,25,SIN_COS:67;
then (( #Z n*sin)(#)cos)|A is continuous by FCONT_1:16;
then
A4: ( #Z n)*sin(#)cos is_integrable_on A by A1,INTEGRA5:11;
(1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL by Th3;
then dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) = dom (( #Z n*sin)(#)cos) by
A1,FDIFF_1:def 7;
then
A5: (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) = (( #Z n*sin)(#)cos) by A2,
PARTFUN1:5;
(( #Z n)*sin(#)cos)|A is bounded by A1,A3,INTEGRA5:10;
hence thesis by A4,A5,Th3,INTEGRA5:13;
end;
theorem
A = [.0,PI.] implies integral(( #Z n*sin)(#)cos,A) = 0
proof
assume A=[.0,PI.];
then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37;
then
integral(( #Z n*sin)(#)cos,A)=((1/(n+1))(#)( #Z (n+1)*sin)).(PI) -((1/(n
+1))(#)( #Z (n+1)*sin)).0 by Th19
.= 1/(n+1)*( #Z (n+1)*sin).PI -((1/(n+1))(#)( #Z (n+1)*sin)).0 by
VALUED_1:6
.= 1/(n+1)*( #Z (n+1)*sin).PI -1/(n+1)*( #Z (n+1)*sin).0 by VALUED_1:6
.= 1/(n+1)*(( #Z (n+1)).(sin.pp)) -1/(n+1)*( #Z (n+1)*sin).0 by FUNCT_1:13
,SIN_COS:24
.= 1/(n+1)*(( #Z (n+1)).(sin.PI)) -1/(n+1)*(( #Z (n+1)).(sin.0)) by
FUNCT_1:13,SIN_COS:24,Lm6
.= 0 by SIN_COS:30,76;
hence thesis;
end;
theorem
A = [.0,2*PI.] implies integral(( #Z n*sin)(#)cos,A) = 0
proof
assume A=[.0,2*PI.];
then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
then
integral(( #Z n*sin)(#)cos,A)=((1/(n+1))(#)( #Z (n+1)*sin)).(2*PI) -((1/
(n+1))(#)( #Z (n+1)*sin)).0 by Th19
.= 1/(n+1)*( #Z (n+1)*sin).(2*PI) -((1/(n+1))(#)( #Z (n+1)*sin)).0 by
VALUED_1:6
.= 1/(n+1)*( #Z (n+1)*sin).dp -1/(n+1)*( #Z (n+1)*sin).0 by VALUED_1:6
.= 1/(n+1)*(( #Z (n+1)).(sin.(2*PI))) -1/(n+1)*( #Z (n+1)*sin).0 by
FUNCT_1:13,SIN_COS:24
.= 1/(n+1)*(( #Z (n+1)).(sin.(2*PI))) -1/(n+1)*(( #Z (n+1)).(sin.0)) by
FUNCT_1:13,SIN_COS:24,Lm6
.= 0 by SIN_COS:30,76;
hence thesis;
end;
:: f.x = (cos.x)^n*(sin.x)
theorem Th22:
integral(( #Z n*cos)(#)sin,A) = ((-1/(n+1))(#)( #Z (n+1)*cos)).(
upper_bound A) -((-1/(n+1))(#)( #Z (n+1)*cos)).(lower_bound A)
proof
A1: [#]REAL=dom (( #Z n*cos)(#)sin) by FUNCT_2:def 1;
A2: for x being Element of REAL
st x in dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) holds (((-1/(n+
1))(#)( #Z (n+1)*cos))`|REAL).x = (( #Z n*cos)(#)sin).x
proof
let x be Element of REAL;
assume x in dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL);
(((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(cos.x) #Z n *sin.x by Th4
.=( #Z n).(cos.x)*sin.x by TAYLOR_1:def 1
.=(( #Zn)*cos).x*sin.x by FUNCT_1:13,SIN_COS:24
.= ((( #Z n)*cos)(#)sin).x by A1,VALUED_1:def 4;
hence thesis;
end;
#Z n*cos is_differentiable_in x0
proof
cos is_differentiable_in x0 by SIN_COS:63;
hence thesis by TAYLOR_1:3;
end;
then dom ( #Z n*cos)=REAL & for x0 st x0 in REAL holds #Z n*cos
is_differentiable_in x0 by FUNCT_2:def 1;
then #Z n*cos is_differentiable_on REAL by A1,FDIFF_1:9;
then
A3: (( #Z n*cos)(#)sin)|REAL is continuous by A1,FDIFF_1:21,25,SIN_COS:68;
then (( #Z n*cos)(#)sin)|A is continuous by FCONT_1:16;
then
A4: ( #Z n*cos)(#)sin is_integrable_on A by A1,INTEGRA5:11;
(-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL by Th4;
then
dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) = dom (( #Z n*cos)(#)sin) by A1,
FDIFF_1:def 7;
then
A5: (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) = (( #Z n*cos)(#)sin) by A2,
PARTFUN1:5;
(( #Z n*cos)(#)sin)|A is bounded by A1,A3,INTEGRA5:10;
hence thesis by A4,A5,Th4,INTEGRA5:13;
end;
theorem
A = [.0,2*PI.] implies integral(( #Z n*cos)(#)sin,A) = 0
proof
assume A=[.0,2*PI.];
then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37;
then
integral(( #Z n*cos)(#)sin,A)=((-1/(n+1))(#)( #Z (n+1)*cos)).(2*PI) -((-
1/(n+1))(#)( #Z (n+1)*cos)).0 by Th22
.= (-1/(n+1))*( #Z (n+1)*cos).(2*PI) -((-1/(n+1))(#)( #Z (n+1)*cos)).0
by VALUED_1:6
.= (-1/(n+1))*( #Z (n+1)*cos).(2*PI) -(-1/(n+1))*( #Z (n+1)*cos).0 by
VALUED_1:6
.= (-1/(n+1))*(( #Z (n+1)).(cos.dp)) -(-1/(n+1))*( #Z (n+1)*cos).0
by FUNCT_1:13,SIN_COS:24
.= (-1/(n+1))*(( #Z (n+1)).(cos.(2*PI))) -(-1/(n+1))*(( #Z (n+1)).(cos.0
)) by FUNCT_1:13,SIN_COS:24,Lm6
.= 0 by SIN_COS:30,76;
hence thesis;
end;
reconsider pd = PI/2, mpd = - PI/2 as Element of REAL by XREAL_0:def 1;
theorem
A = [.-PI/2,PI/2.] implies integral(( #Z n*cos)(#)sin,A) = 0
proof
assume A=[.-PI/2,PI/2.];
then upper_bound A=PI/2 & lower_bound A=-PI/2 by INTEGRA8:37;
then
integral(( #Z n*cos)(#)sin,A)=((-1/(n+1))(#)( #Z (n+1)*cos)).(PI/2) -((-
1/(n+1))(#)( #Z (n+1)*cos)).(-PI/2) by Th22
.= (-1/(n+1))*( #Z (n+1)*cos).(PI/2) -((-1/(n+1))(#)( #Z (n+1)*cos)).(-
PI/2) by VALUED_1:6
.= (-1/(n+1))*( #Z (n+1)*cos).(PI/2) -(-1/(n+1))*( #Z (n+1)*cos).(-PI/2)
by VALUED_1:6
.= (-1/(n+1))*(( #Z (n+1)).(cos.pd)) -(-1/(n+1))*( #Z (n+1)*cos).mpd
by FUNCT_1:13,SIN_COS:24
.= (-1/(n+1))*(( #Z (n+1)).(cos.pd)) -(-1/(n+1))*(( #Z (n+1)).(cos.(
-PI/2))) by FUNCT_1:13,SIN_COS:24
.= (-1/(n+1))*(( #Z (n+1)).(cos.(PI/2))) -(-1/(n+1))*(( #Z (n+1)).(cos.(
PI/2))) by SIN_COS:30
.= 0;
hence thesis;
end;
:: f.x = cos.(m*x)*cos.(n*x)
theorem
m+n<>0 & m-n<>0 implies integral((cos*AffineMap(m,0))(#)(cos*AffineMap
(n,0)),A) = ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0))).(upper_bound A) -((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
(1/(2*(m-n
)))(#)(sin*AffineMap(m-n,0))).(lower_bound A)
proof
assume
A1: m+n<>0 & m-n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
proof
let x;
assume x in REAL;
(AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
.=n*x;
hence thesis;
end;
A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: dom (cos*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(m,0).x=m*x
proof
let x;
assume x in REAL;
(AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4
.=m*x;
hence thesis;
end;
A6: for x being Element of REAL
st x in dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)
))(#)(sin*AffineMap(m-n,0)))`|REAL) holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,
0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x = ((cos*AffineMap(m,0))
(#)(cos*AffineMap(n,0))).x
proof
let x be Element of REAL;
assume x in dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(
sin*AffineMap(m-n,0)))`|REAL);
(((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0)))`|REAL).x = cos.(m*x)*cos.(n*x) by A1,Th5
.= cos.(AffineMap(m,0).x)*cos.(n*x) by A5
.= (cos.(AffineMap(m,0).x))*(cos.((AffineMap(n,0)).x)) by A2
.= ((cos*AffineMap(m,0)).x) *(cos.(AffineMap(n,0).x)) by A4,FUNCT_1:12
.= ((cos*AffineMap(m,0)).x)*((cos*AffineMap(n,0)).x) by A3,FUNCT_1:12
.= ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5;
hence thesis;
end;
A7: [#]REAL = dom ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by
FUNCT_2:def 1;
((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap
(m-n,0))) is_differentiable_on REAL by A1,Th5;
then dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0)))`|REAL) = dom ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))
by A7,FDIFF_1:def 7;
then
A8: (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0)))`|REAL) = (cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)) by A6,
PARTFUN1:5;
((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is continuous;
then
A9: ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A7,
INTEGRA5:11;
((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10;
hence thesis by A1,A9,A8,Th5,INTEGRA5:13;
end;
:: f.x = sin.(m*x)*sin.(n*x)
theorem
m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(sin*AffineMap
(n,0)),A) = ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0))).(upper_bound A) -((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
(1/(2*(m+n
)))(#)(sin*AffineMap(m+n,0))).(lower_bound A)
proof
assume
A1: m+n<>0 & m-n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
proof
let x;
assume x in REAL;
(AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
.=n*x;
hence thesis;
end;
A3: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: dom (sin*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(m,0).x=m*x
proof
let x;
assume x in REAL;
(AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4
.=m*x;
hence thesis;
end;
A6: for x being Element of REAL
st x in dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)
))(#)(sin*AffineMap(m+n,0)))`|REAL) holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,
0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x = ((sin*AffineMap(m,0))
(#)(sin*AffineMap(n,0))).x
proof
let x be Element of REAL;
assume x in dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(
sin*AffineMap(m+n,0)))`|REAL);
(((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0)))`|REAL).x = sin.(m*x)*sin.(n*x) by A1,Th6
.= sin.(AffineMap(m,0).x)*sin.(n*x) by A5
.= (sin.(AffineMap(m,0).x))*(sin.(AffineMap(n,0).x)) by A2
.= ((sin*(AffineMap(m,0))).x) *(sin.(AffineMap(n,0).x)) by A4,FUNCT_1:12
.= ((sin*AffineMap(m,0)).x)*((sin*AffineMap(n,0)).x) by A3,FUNCT_1:12
.= ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))).x by VALUED_1:5;
hence thesis;
end;
A7: REAL=dom ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))) by FUNCT_2:def 1;
((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))|A is continuous;
then
A8: ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))) is_integrable_on A by A7,
INTEGRA5:11;
((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap
(m+n,0))) is_differentiable_on REAL by A1,Th6;
then dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0)))`|REAL) = dom ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))
by A7,FDIFF_1:def 7;
then
A9: (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0)))`|REAL) = (sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)) by A6,
PARTFUN1:5;
((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10;
hence thesis by A1,A8,A9,Th6,INTEGRA5:13;
end;
:: f.x = sin.(m*x)*cos.(n*x)
theorem
m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(cos*AffineMap
(n,0)),A) = ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0))).(upper_bound A) -((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))
- (1/(2*(
m-n)))(#)(cos*AffineMap(m-n,0))).(lower_bound A)
proof
assume
A1: m+n<>0 & m-n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
proof
let x;
assume x in REAL;
(AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
.=n*x;
hence thesis;
end;
A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: dom (sin*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1;
A5: for x st x in REAL holds AffineMap(m,0).x=m*x
proof
let x;
assume x in REAL;
(AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4
.=m*x;
hence thesis;
end;
A6: for x being Element of REAL
st x in dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m
-n)))(#)(cos*AffineMap(m-n,0)))`|REAL) holds (((-(1/(2*(m+n)))(#)(cos*AffineMap
(m+n,0)))- (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x = ((sin*AffineMap(m
,0))(#)(cos*AffineMap(n,0))).x
proof
let x be Element of REAL;
assume
x in dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)
(cos*AffineMap(m-n,0)))`|REAL);
(((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0)))`|REAL).x = sin.(m*x)*cos.(n*x) by A1,Th7
.= sin.(AffineMap(m,0).x)*cos.(n*x) by A5
.= (sin.(AffineMap(m,0).x))*(cos.(AffineMap(n,0).x)) by A2
.= ((sin*AffineMap(m,0)).x)*(cos.(AffineMap(n,0).x)) by A4,FUNCT_1:12
.= ((sin*AffineMap(m,0)).x)*((cos*AffineMap(n,0)).x) by A3,FUNCT_1:12
.= ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5;
hence thesis;
end;
A7: [#]REAL=dom ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by FUNCT_2:def 1;
((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is continuous;
then
A8: ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A7,
INTEGRA5:11;
((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0))) is_differentiable_on REAL by A1,Th7;
then dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0)))`|REAL) = dom ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))
by A7,FDIFF_1:def 7;
then
A9: (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0)))`|REAL) = (sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)) by A6,
PARTFUN1:5;
((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10;
hence thesis by A1,A8,A9,Th7,INTEGRA5:13;
end;
:: f.x = x*sin.(n*x)
theorem
n<>0 implies integral((AffineMap(1,0))(#)(sin*AffineMap(n,0)),A) = ((1
/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0))).
(upper_bound
A) -((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0)
)).(lower_bound A)
proof
assume
A1: n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
proof
let x;
assume x in REAL;
(AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
.=n*x;
hence thesis;
end;
A3: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: for x st x in REAL holds AffineMap(1,0).x=x
proof
let x;
assume x in REAL;
(AffineMap(1,0)).x = 1*x + 0 by FCONT_1:def 4
.=x;
hence thesis;
end;
A5: for x being Element of REAL
st x in dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))
(#)(cos*AffineMap(n,0)))`|REAL) holds (((1/(n^2))(#)(sin*AffineMap(n,0))- (
AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = ((AffineMap(1,0))(#)(sin*
AffineMap(n,0))).x
proof
let x be Element of REAL;
assume
x in dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos
*AffineMap(n,0)))`|REAL);
(((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
AffineMap(n,0)))`|REAL).x = x*sin.(n*x) by A1,Th8
.= x*(sin.(AffineMap(n,0).x)) by A2
.= x*(sin*AffineMap(n,0)).x by A3,FUNCT_1:12
.= (AffineMap(1,0).x)*(sin*AffineMap(n,0)).x by A4
.= ((AffineMap(1,0))(#)(sin*AffineMap(n,0))).x by VALUED_1:5;
hence thesis;
end;
A6: dom ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) = [#]REAL by FUNCT_2:def 1;
((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(
n,0))) is_differentiable_on REAL by A1,Th8;
then dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*
AffineMap(n,0)))`|REAL) = dom ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) by A6,
FDIFF_1:def 7;
then
A7: (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap
(n,0)))`|REAL) = (AffineMap(1,0))(#)(sin*AffineMap(n,0)) by A5,PARTFUN1:5;
((AffineMap(1,0))(#)(sin*AffineMap(n,0)))|A is continuous;
then
A8: ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) is_integrable_on A by A6,
INTEGRA5:11;
((AffineMap(1,0))(#)(sin*AffineMap(n,0)))|A is bounded by A6,INTEGRA5:10;
hence thesis by A1,A8,A7,Th8,INTEGRA5:13;
end;
:: f.x = x*cos.(n*x)
theorem
n<>0 implies integral((AffineMap(1,0))(#)(cos*AffineMap(n,0)),A) = ((1
/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0))).
(upper_bound
A) -((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0)
)).(lower_bound A)
proof
assume
A1: n<>0;
A2: for x st x in REAL holds AffineMap(n,0).x=n*x
proof
let x;
assume x in REAL;
(AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4
.=n*x;
hence thesis;
end;
A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1;
A4: for x st x in REAL holds AffineMap(1,0).x=x
proof
let x;
assume x in REAL;
(AffineMap(1,0)).x = 1*x + 0 by FCONT_1:def 4
.=x;
hence thesis;
end;
A5: for x being Element of REAL
st x in dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))
(#)(sin*AffineMap(n,0)))`|REAL) holds (((1/(n^2))(#)(cos*AffineMap(n,0))+ (
AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = ((AffineMap(1,0))(#)(cos*
AffineMap(n,0))).x
proof
let x be Element of REAL;
assume
x in dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin
*AffineMap(n,0)))`|REAL);
(((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
AffineMap(n,0)))`|REAL).x = x*cos.(n*x) by A1,Th9
.= x*(cos.(AffineMap(n,0).x)) by A2
.= x*(cos*AffineMap(n,0)).x by A3,FUNCT_1:12
.= (AffineMap(1,0).x)*(cos*AffineMap(n,0)).x by A4
.= ((AffineMap(1,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5;
hence thesis;
end;
A6: dom ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) = [#]REAL by FUNCT_2:def 1;
((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(
n,0))) is_differentiable_on REAL by A1,Th9;
then dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*
AffineMap(n,0)))`|REAL) = dom ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) by A6,
FDIFF_1:def 7;
then
A7: (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap
(n,0)))`|REAL) = (AffineMap(1,0))(#)(cos*AffineMap(n,0)) by A5,PARTFUN1:5;
((AffineMap(1,0))(#)(cos*AffineMap(n,0)))|A is continuous;
then
A8: ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A6,
INTEGRA5:11;
((AffineMap(1,0))(#)(cos*AffineMap(n,0)))|A is bounded by A6,INTEGRA5:10;
hence thesis by A1,A8,A7,Th9,INTEGRA5:13;
end;
theorem
integral((AffineMap(1,0))(#)sinh,A) = ((AffineMap(1,0))(#)cosh-sinh).(
upper_bound A) -((AffineMap(1,0))(#)cosh-sinh).(lower_bound A)
proof
A1: for x being Element of REAL
st x in dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL) holds (((
AffineMap(1,0))(#)cosh-sinh)`|REAL).x = ((AffineMap(1,0))(#)sinh).x
proof
let x be Element of REAL;
assume x in dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL);
(((AffineMap(1,0))(#)cosh-sinh)`|REAL).x = (1*x+0)*sinh.x by Th10
.= ((AffineMap(1,0)).x)*sinh.x by FCONT_1:def 4
.= ((AffineMap(1,0))(#)sinh).x by VALUED_1:5;
hence thesis;
end;
A2: dom ((AffineMap(1,0))(#)sinh) = [#]REAL by FUNCT_2:def 1;
then dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL) = dom ((AffineMap(1,0))(#)
sinh) by Th10,FDIFF_1:def 7;
then
A3: (((AffineMap(1,0))(#)cosh-sinh)`|REAL) = (AffineMap(1,0))(#)sinh by A1,
PARTFUN1:5;
dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
.x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
then
A4: ((AffineMap(1,0))(#)sinh)|REAL is continuous by A2,FDIFF_1:21,25
,SIN_COS2:34;
then
A5: ((AffineMap(1,0))(#)sinh)|A is continuous by FCONT_1:16;
((AffineMap(1,0))(#)sinh)|A is bounded by A2,A4,INTEGRA5:10;
hence thesis by A2,A5,A3,Th10,INTEGRA5:11,13;
end;
theorem
integral((AffineMap(1,0))(#)cosh,A) = ((AffineMap(1,0))(#)sinh-cosh).(
upper_bound A) -((AffineMap(1,0))(#)sinh-cosh).(lower_bound A)
proof
A1: for x being Element of REAL
st x in dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL) holds (((
AffineMap(1,0))(#)sinh-cosh)`|REAL).x = ((AffineMap(1,0))(#)cosh).x
proof
let x be Element of REAL;
assume x in dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL);
(((AffineMap(1,0))(#)sinh-cosh)`|REAL).x = (1*x+0)*cosh.x by Th11
.= ((AffineMap(1,0)).x)*(cosh.x) by FCONT_1:def 4
.= ((AffineMap(1,0))(#)cosh).x by VALUED_1:5;
hence thesis;
end;
A2: dom ((AffineMap(1,0))(#)cosh) = [#]REAL by FUNCT_2:def 1;
then dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL) = dom ((AffineMap(1,0))(#)
cosh) by Th11,FDIFF_1:def 7;
then
A3: (((AffineMap(1,0))(#)sinh-cosh)`|REAL) = (AffineMap(1,0))(#)cosh by A1,
PARTFUN1:5;
dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0)
.x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1;
then AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23;
then
A4: ((AffineMap(1,0))(#)cosh)|REAL is continuous by A2,FDIFF_1:21,25
,SIN_COS2:35;
then
A5: ((AffineMap(1,0))(#)cosh)|A is continuous by FCONT_1:16;
((AffineMap(1,0))(#)cosh)|A is bounded by A2,A4,INTEGRA5:10;
hence thesis by A2,A5,A3,Th11,INTEGRA5:11,13;
end;
:: f.x = (a*x+b)^n
theorem
a*(n+1) <> 0 implies integral( #Z n*AffineMap(a,b),A) = ((1/(a*(n+1)))
(#)( #Z (n+1)*AffineMap(a,b))).(upper_bound A) -
((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a
,b))).(lower_bound A)
proof
assume
A1: a*(n+1) <> 0;
A2: [#]REAL=dom (AffineMap(a,b)) by FUNCT_2:def 1;
A3: for x being Element of REAL
st x in dom (((1/(a*(n+1))) (#)( #Z (n+1)*AffineMap(a,b)))`|REAL)
holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x = ( #Z n*AffineMap
(a,b)).x
proof
let x be Element of REAL;
assume x in dom (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL);
(((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x =(a*x+b) #Z n
by A1,Th12
.= (AffineMap(a,b).x) #Z n by FCONT_1:def 4
.= ( #Z n).(AffineMap(a,b).x) by TAYLOR_1:def 1
.=( #Z n*AffineMap(a,b)).x by A2,FUNCT_1:13;
hence thesis;
end;
A4: [#]REAL=dom ( #Z n*AffineMap(a,b)) by FUNCT_2:def 1;
for x st x in REAL holds AffineMap(a,b).x=a*x + b by FCONT_1:def 4;
then
A5: AffineMap(a,b) is_differentiable_on REAL by A2,FDIFF_1:23;
#Z n*AffineMap(a,b) is_differentiable_in x
proof
x in REAL by XREAL_0:def 1;
then AffineMap(a,b) is_differentiable_in x by A2,A5,FDIFF_1:9;
hence thesis by TAYLOR_1:3;
end;
then for x st x in REAL holds #Z n*AffineMap(a,b) is_differentiable_in x;
then #Z n*AffineMap(a,b) is_differentiable_on REAL by A4,FDIFF_1:9;
then
A6: ( #Z n*AffineMap(a,b))|REAL is continuous by FDIFF_1:25;
then ( #Z n*AffineMap(a,b))|A is continuous by FCONT_1:16;
then
A7: #Z n*AffineMap(a,b) is_integrable_on A by A4,INTEGRA5:11;
(1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)) is_differentiable_on REAL by A1
,Th12;
then dom (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL) = dom ( #Z n*
AffineMap(a,b)) by A4,FDIFF_1:def 7;
then
A8: (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL) = #Z n*AffineMap(a
,b) by A3,PARTFUN1:5;
( #Z n*AffineMap(a,b))|A is bounded by A4,A6,INTEGRA5:10;
hence thesis by A1,A7,A8,Th12,INTEGRA5:13;
end;
begin :: Addenda
reserve f, f1, f2, f3 for PartFunc of REAL, REAL;
:: f.x = (1/2)*x^2
theorem Th33:
Z c= dom ((1/2)(#)f) & f=#Z 2 implies (1/2)(#)f
is_differentiable_on Z & for x st x in Z holds (((1/2)(#)f)`|Z).x = x
proof
assume that
A1: Z c= dom ((1/2)(#)f) and
A2: f=#Z 2;
Z c= dom f & for x st x in Z holds f is_differentiable_in x by A1,A2,
TAYLOR_1:2,VALUED_1:def 5;
then
A3: f is_differentiable_on Z by FDIFF_1:9;
A4: for x st x in Z holds (f`|Z).x=2*x
proof
let x;
2 * (x #Z (2-1)) = 2 * x by PREPOWER:35;
then
A5: diff(f,x) = 2 * x by A2,TAYLOR_1:2;
assume x in Z;
hence thesis by A3,A5,FDIFF_1:def 7;
end;
for x st x in Z holds (((1/2)(#)f)`|Z).x=x
proof
let x;
assume
A6: x in Z;
then (((1/2)(#)f)`|Z).x=(1/2)*diff(f,x) by A1,A3,FDIFF_1:20
.=(1/2)*(f`|Z).x by A3,A6,FDIFF_1:def 7
.=(1/2)*(2*x) by A4,A6
.=x;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:20;
end;
:: f.x = x
theorem
A c= Z & f=#Z 2 & Z = dom ((1/2)(#)f) implies integral(id Z,A) = ((1/2
)(#)f).(upper_bound A)-((1/2)(#)f).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: f=#Z 2 & Z = dom ((1/2)(#)f);
A3: A c= dom id Z by A1;
then
A4: (id Z)|A is bounded by INTEGRA5:10;
A5: ((1/2)(#)f) is_differentiable_on Z by A2,Th33;
A6: for x being Element of REAL
st x in dom (((1/2)(#)f)`|Z) holds (((1/2)(#)f)`|Z).x = (id Z).x
proof
let x be Element of REAL;
assume x in dom (((1/2)(#)f)`|Z);
then
A7: x in Z by A5,FDIFF_1:def 7;
then (((1/2)(#)f)`|Z).x = x by A2,Th33
.= (id Z).x by A7,FUNCT_1:18;
hence thesis;
end;
dom (((1/2)(#)f)`|Z) = dom (id Z) by A5,FDIFF_1:def 7;
then
A8: (((1/2)(#)f)`|Z) = id Z by A6,PARTFUN1:5;
(id Z)|A is continuous;
then id Z is_integrable_on A by A3,INTEGRA5:11;
hence thesis by A1,A2,A4,A8,Th33,INTEGRA5:13;
end;
:: f.x = -1/x^2 :: INTEGRA9
theorem
not 0 in Z & A c= Z & (for x st x in Z holds x<>0 & f.x = -1/x^2) &
dom f = Z & f|A is continuous implies integral(f,A) =
((id Z)^).(upper_bound A)-((id Z)
^).(lower_bound A)
proof
set g = id Z;
assume that
A1: not 0 in Z and
A2: A c= Z and
A3: for x st x in Z holds x<>0 & f.x = -1/x^2 and
A4: dom f = Z and
A5: f|A is continuous;
A6: f is_integrable_on A by A2,A4,A5,INTEGRA5:11;
A7: g^ is_differentiable_on Z by A1,FDIFF_5:4;
A8: for x being Element of REAL st x in dom ((g^)`|Z) holds ((g^)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((g^)`|Z);
then
A9: x in Z by A7,FDIFF_1:def 7;
then ((g^)`|Z).x = -1/x^2 by A1,FDIFF_5:4
.= f.x by A3,A9;
hence thesis;
end;
dom ((g^)`|Z) = dom f by A4,A7,FDIFF_1:def 7;
then ((g^)`|Z) = f by A8,PARTFUN1:5;
hence thesis by A2,A4,A5,A6,A7,INTEGRA5:10,13;
end;
:: f.x = 2*x/(1+x^2)^2
theorem
A c= Z & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0 & f.x=2*x/(1+x
^2)^2) & dom (f1/(f2+f1))=Z & Z = dom f & f|A is continuous implies integral(f,
A) = (f1/(f2+f1)).(upper_bound A)-(f1/(f2+f1)).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: f1=#Z 2 and
A3: for x st x in Z holds f2.x=1 & x<>0 & f.x=2*x/(1+x^2)^2 and
A4: dom (f1/(f2+f1))=Z and
A5: Z = dom f and
A6: f|A is continuous;
A7: f is_integrable_on A by A1,A5,A6,INTEGRA5:11;
A8: for x st x in Z holds f2.x=1 & x<>0 by A3;
then
A9: (f1/(f2+f1)) is_differentiable_on Z by A2,A4,FDIFF_6:7;
A10: for x being Element of REAL
st x in dom ((f1/(f2+f1))`|Z) holds ((f1/(f2+f1))`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((f1/(f2+f1))`|Z);
then
A11: x in Z by A9,FDIFF_1:def 7;
then ((f1/(f2+f1))`|Z).x = 2*x/(1+x^2)^2 by A2,A4,A8,FDIFF_6:7
.= f.x by A3,A11;
hence thesis;
end;
dom ((f1/(f2+f1))`|Z) = dom f by A5,A9,FDIFF_1:def 7;
then ((f1/(f2+f1))`|Z) = f by A10,PARTFUN1:5;
hence thesis by A1,A5,A6,A7,A9,INTEGRA5:10,13;
end;
theorem Th37:
(Z c= dom (tan+sec) & for x st x in Z holds (1+sin.x)<>0 & (1-
sin.x)<>0) implies tan+sec is_differentiable_on Z & for x st x in Z holds ((tan
+sec)`|Z).x = 1/(1-sin.x)
proof
assume that
A1: Z c= dom (tan+sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
Z c= dom tan /\ dom (cos^) by A1,VALUED_1:def 1;
then
A3: Z c= dom tan by XBOOLE_1:18;
then
A4: for x st x in Z holds cos.x<>0 by FDIFF_8:1;
then
A5: cos^ is_differentiable_on Z by FDIFF_4:39;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A3,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds ((tan+sec)`|Z).x = 1/(1-sin.x)
proof
let x;
assume
A7: x in Z;
then
A8: cos.x<>0 by A3,FDIFF_8:1;
A9: 1+sin.x<>0 by A2,A7;
((tan+sec)`|Z).x = diff(tan,x) + diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:18
.=1/(cos.x)^2 + diff(cos^,x) by A8,FDIFF_7:46
.=1/(cos.x)^2 + ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7
.=1/(cos.x)^2 + sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39
.=(1+sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) by XCMPLX_1:62
.=(1+sin.x)/(1-(sin.x)^2) by SIN_COS:28
.=(1+sin.x)/((1+sin.x)*(1-sin.x))
.=(1+sin.x)/(1+sin.x)/(1-sin.x) by XCMPLX_1:78
.=1/(1-sin.x) by A9,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:18;
end;
:: f.x = 1/(1-sin.x)
theorem
A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/
(1-sin.x)) & dom (tan+sec)=Z & Z = dom f & f|A is continuous implies integral(f
,A) = (tan+sec).(upper_bound A)-(tan+sec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/(1-sin. x) and
A3: dom (tan+sec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
then
A8: (tan+sec) is_differentiable_on Z by A3,Th37;
A9: for x being Element of REAL
st x in dom ((tan+sec)`|Z) holds ((tan+sec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((tan+sec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((tan+sec)`|Z).x = 1/(1-sin.x) by A3,A7,Th37
.= f.x by A2,A10;
hence thesis;
end;
dom ((tan+sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((tan+sec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
theorem Th39:
(Z c= dom (tan-sec) & for x st x in Z holds (1+sin.x)<>0 & (1-
sin.x)<>0) implies tan-sec is_differentiable_on Z & for x st x in Z holds ((tan
-sec)`|Z).x = 1/(1+sin.x)
proof
assume that
A1: Z c= dom (tan-sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
Z c= dom tan /\ dom (cos^) by A1,VALUED_1:12;
then
A3: Z c= dom tan by XBOOLE_1:18;
then
A4: for x st x in Z holds cos.x<>0 by FDIFF_8:1;
then
A5: cos^ is_differentiable_on Z by FDIFF_4:39;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A3,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds ((tan-sec)`|Z).x = 1/(1+sin.x)
proof
let x;
assume
A7: x in Z;
then
A8: cos.x<>0 by A3,FDIFF_8:1;
A9: 1-sin.x<>0 by A2,A7;
((tan-sec)`|Z).x = diff(tan,x) - diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:19
.=1/(cos.x)^2 - diff(cos^,x) by A8,FDIFF_7:46
.=1/(cos.x)^2 - ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7
.=1/(cos.x)^2 - sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39
.=(1-sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) by XCMPLX_1:120
.=(1-sin.x)/(1-(sin.x)^2) by SIN_COS:28
.=(1-sin.x)/((1+sin.x)*(1-sin.x))
.=(1-sin.x)/(1-sin.x)/(1+sin.x) by XCMPLX_1:78
.=1/(1+sin.x) by A9,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:19;
end;
:: f.x = 1/(1+sin.x)
theorem
A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/
(1+sin.x)) & dom (tan-sec)=Z & Z = dom f & f|A is continuous implies integral(f
,A) = (tan-sec).(upper_bound A)-(tan-sec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/(1+sin. x) and
A3: dom (tan-sec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
then
A8: (tan-sec) is_differentiable_on Z by A3,Th39;
A9: for x being Element of REAL st x in dom ((tan-sec)`|Z)
holds ((tan-sec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((tan-sec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((tan-sec)`|Z).x = 1/(1+sin.x) by A3,A7,Th39
.= f.x by A2,A10;
hence thesis;
end;
dom ((tan-sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((tan-sec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
theorem Th41:
(Z c= dom (-cot+cosec) & for x st x in Z holds (1+cos.x)<>0 & (1
-cos.x)<>0) implies -cot+cosec is_differentiable_on Z & for x st x in Z holds (
(-cot+cosec)`|Z).x = 1/(1+cos.x)
proof
assume that
A1: Z c= dom (-cot+cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
Z c= dom (-cot) /\ dom (sin^) by A1,VALUED_1:def 1;
then
A3: Z c= dom (-cot) by XBOOLE_1:18;
then
A4: Z c= dom cot by VALUED_1:8;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A4,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
then
A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20;
A7: for x st x in Z holds sin.x<>0 by A4,FDIFF_8:2;
then
A8: sin^ is_differentiable_on Z by FDIFF_4:40;
for x st x in Z holds ((-cot+cosec)`|Z).x = 1/(1+cos.x)
proof
let x;
assume
A9: x in Z;
then
A10: sin.x<>0 by A4,FDIFF_8:2;
A11: 1-cos.x<>0 by A2,A9;
((-cot+cosec)`|Z).x = diff(-cot,x) + diff(sin^,x) by A1,A8,A6,A9,FDIFF_1:18
.=(((-1)(#)cot)`|Z).x + diff(sin^,x) by A6,A9,FDIFF_1:def 7
.=(-1)*diff(cot,x) + diff(sin^,x) by A3,A5,A9,FDIFF_1:20
.=(-1)*(-1/(sin.x)^2)+ diff(sin^,x) by A10,FDIFF_7:47
.=1/(sin.x)^2 + ((sin^)`|Z).x by A8,A9,FDIFF_1:def 7
.=1/(sin.x)^2 + (-cos.x/(sin.x)^2) by A7,A9,FDIFF_4:40
.=1/(sin.x)^2 - cos.x/(sin.x)^2
.=(1-cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2) by XCMPLX_1:120
.=(1-cos.x)/(1-(cos.x)^2) by SIN_COS:28
.=(1-cos.x)/((1-cos.x)*(1+cos.x))
.=(1-cos.x)/(1-cos.x)/(1+cos.x) by XCMPLX_1:78
.=1/(1+cos.x) by A11,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1,A8,A6,FDIFF_1:18;
end;
:: f.x = 1/(1+cos.x)
theorem
A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/
(1+cos.x)) & dom (-cot+cosec)=Z & Z = dom f & f|A is continuous implies
integral(f,A) = (-cot+cosec).(upper_bound A)-(-cot+cosec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/(1+cos. x) and
A3: dom (-cot+cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
then
A8: (-cot+cosec) is_differentiable_on Z by A3,Th41;
A9: for x being Element of REAL
st x in dom ((-cot+cosec)`|Z) holds ((-cot+cosec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((-cot+cosec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((-cot+cosec)`|Z).x = 1/(1+cos.x) by A3,A7,Th41
.= f.x by A2,A10;
hence thesis;
end;
dom ((-cot+cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((-cot+cosec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
theorem Th43:
(Z c= dom (-cot-cosec) & for x st x in Z holds (1+cos.x)<>0 & (1
-cos.x)<>0) implies -cot-cosec is_differentiable_on Z & for x st x in Z holds (
(-cot-cosec)`|Z).x = 1/(1-cos.x)
proof
assume that
A1: Z c= dom (-cot-cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
Z c= dom (-cot) /\ dom (sin^) by A1,VALUED_1:12;
then
A3: Z c= dom (-cot) by XBOOLE_1:18;
then
A4: Z c= dom cot by VALUED_1:8;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A4,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
then
A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20;
A7: for x st x in Z holds sin.x<>0 by A4,FDIFF_8:2;
then
A8: sin^ is_differentiable_on Z by FDIFF_4:40;
for x st x in Z holds ((-cot-cosec)`|Z).x = 1/(1-cos.x)
proof
let x;
assume
A9: x in Z;
then
A10: sin.x<>0 by A4,FDIFF_8:2;
A11: 1+cos.x<>0 by A2,A9;
((-cot-cosec)`|Z).x = diff(-cot,x) - diff(sin^,x) by A1,A8,A6,A9,FDIFF_1:19
.=(((-1)(#)cot)`|Z).x - diff(sin^,x) by A6,A9,FDIFF_1:def 7
.=(-1)*diff(cot,x) - diff(sin^,x) by A3,A5,A9,FDIFF_1:20
.=(-1)*(-1/(sin.x)^2)- diff(sin^,x) by A10,FDIFF_7:47
.=1/(sin.x)^2 - ((sin^)`|Z).x by A8,A9,FDIFF_1:def 7
.=1/(sin.x)^2 - (-cos.x/(sin.x)^2) by A7,A9,FDIFF_4:40
.=1/(sin.x)^2 + cos.x/(sin.x)^2
.=(1+cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2) by XCMPLX_1:62
.=(1+cos.x)/(1-(cos.x)^2) by SIN_COS:28
.=(1+cos.x)/((1+cos.x)*(1-cos.x))
.=(1+cos.x)/(1+cos.x)/(1-cos.x) by XCMPLX_1:78
.=1/(1-cos.x) by A11,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1,A8,A6,FDIFF_1:19;
end;
:: f.x = 1/(1-cos.x)
theorem
A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/
(1-cos.x)) & dom (-cot-cosec)=Z & Z = dom f & f|A is continuous implies
integral(f,A) = (-cot-cosec).(upper_bound A)-(-cot-cosec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/(1-cos. x) and
A3: dom (-cot-cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
then
A8: (-cot-cosec) is_differentiable_on Z by A3,Th43;
A9: for x being Element of REAL
st x in dom ((-cot-cosec)`|Z) holds ((-cot-cosec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((-cot-cosec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((-cot-cosec)`|Z).x = 1/(1-cos.x) by A3,A7,Th43
.= f.x by A2,A10;
hence thesis;
end;
dom ((-cot-cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((-cot-cosec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
:: f.x = 1/(1+x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=1/(1+x^2)) & Z =
dom f & f|A is continuous implies integral(f,A)
= arctan.(upper_bound A) - arctan.(lower_bound
A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=1/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: arctan is_differentiable_on Z by A2,SIN_COS9:81;
A7: for x being Element of REAL st x in dom ((arctan)`|Z)
holds ((arctan)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((arctan)`|Z);
then
A8: x in Z by A6,FDIFF_1:def 7;
then ((arctan)`|Z).x = 1/(1+x^2) by A2,SIN_COS9:81
.= f.x by A3,A8;
hence thesis;
end;
dom ((arctan)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
then
A9: ((arctan)`|Z) = f by A7,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:81;
end;
:: f.x = r/(1+x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=r/(1+x^2)) & Z =
dom f & f|A is continuous implies integral(f,A) = (r(#)arctan).(upper_bound A)
- (r(#)
arctan).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=r/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: r(#)arctan is_differentiable_on Z by A2,SIN_COS9:83;
A7: for x being Element of REAL
st x in dom ((r(#)arctan)`|Z) holds ((r(#)arctan)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((r(#)arctan)`|Z);
then
A8: x in Z by A6,FDIFF_1:def 7;
then ((r(#)arctan)`|Z).x = r/(1+x^2) by A2,SIN_COS9:83
.= f.x by A3,A8;
hence thesis;
end;
dom ((r(#)arctan)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
then
A9: ((r(#)arctan)`|Z) = f by A7,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:83;
end;
:: f.x = -1/(1+x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-1/(1+x^2)) & Z
= dom f & f|A is continuous implies integral(f,A) = arccot.(upper_bound A)
- arccot.(
lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=-1/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: arccot is_differentiable_on Z by A2,SIN_COS9:82;
A7: for x being Element of REAL
st x in dom ((arccot)`|Z) holds ((arccot)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((arccot)`|Z);
then
A8: x in Z by A6,FDIFF_1:def 7;
then ((arccot)`|Z).x = -1/(1+x^2) by A2,SIN_COS9:82
.= f.x by A3,A8;
hence thesis;
end;
dom ((arccot)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
then
A9: ((arccot)`|Z) = f by A7,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:82;
end;
:: f.x = -r/(1+x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-r/(1+x^2)) & Z
= dom f & f|A is continuous implies integral(f,A)
= (r(#)arccot).(upper_bound A) - (r
(#)arccot).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=-r/(1+x^2) and
A4: Z = dom f and
A5: f|A is continuous;
A6: r(#)arccot is_differentiable_on Z by A2,SIN_COS9:84;
A7: for x being Element of REAL
st x in dom ((r(#)arccot)`|Z) holds ((r(#)arccot)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((r(#)arccot)`|Z);
then
A8: x in Z by A6,FDIFF_1:def 7;
then ((r(#)arccot)`|Z).x = -r/(1+x^2) by A2,SIN_COS9:84
.= f.x by A3,A8;
hence thesis;
end;
dom ((r(#)arccot)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
then
A9: ((r(#)arccot)`|Z) = f by A7,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:84;
end;
:: f.x = x+cot.x-cosec.x
theorem Th49:
(Z c= dom ((id Z)+cot-cosec) & for x st x in Z holds (1+cos.x)<>
0 & (1-cos.x)<>0) implies (id Z)+cot-cosec is_differentiable_on Z & for x st x
in Z holds ((id Z+cot-cosec)`|Z).x = cos.x/(1+cos.x)
proof
assume that
A1: Z c= dom ((id Z)+cot-cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
A3: Z c= dom ((id Z)+cot) /\ dom cosec by A1,VALUED_1:12;
then
A4: Z c= dom (id Z+cot) by XBOOLE_1:18;
then
Z c= dom id Z /\ dom cot by VALUED_1:def 1;
then
A5: Z c= dom cot by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A7: Z c= dom id Z;
then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A5,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A9: cot is_differentiable_on Z by A5,FDIFF_1:9;
then
A10: id Z + cot is_differentiable_on Z by A4,A8,FDIFF_1:18;
A11: Z c= dom cosec by A3,XBOOLE_1:18;
then
A12: cosec is_differentiable_on Z by FDIFF_9:5;
A13: for x st x in Z holds (((id Z) + cot)`|Z).x = -(cos.x)^2/(sin.x)^2
proof
let x;
assume
A14: x in Z;
then
A15: sin.x<>0 by A5,FDIFF_8:2;
then
A16: (sin.x)^2 >0 by SQUARE_1:12;
((id Z + cot)`|Z).x = diff((id Z),x) + diff(cot,x) by A4,A9,A8,A14,
FDIFF_1:18
.=((id Z)`|Z).x + diff(cot,x) by A8,A14,FDIFF_1:def 7
.=1+diff(cot,x) by A7,A6,A14,FDIFF_1:23
.=1+(-1/(sin.x)^2) by A15,FDIFF_7:47
.=1-1/(sin.x)^2
.=(sin.x)^2/(sin.x)^2-1/(sin.x)^2 by A16,XCMPLX_1:60
.=((sin.x)^2-1)/(sin.x)^2 by XCMPLX_1:120
.=((sin.x)^2-((sin.x)^2+(cos.x)^2))/(sin.x)^2 by SIN_COS:28
.=(-(cos.x)^2)/(sin.x)^2
.=-(cos.x)^2/(sin.x)^2 by XCMPLX_1:187;
hence thesis;
end;
for x st x in Z holds ((id Z + cot-cosec)`|Z).x = cos.x/(1+cos.x)
proof
let x;
assume
A17: x in Z;
then
A18: 1-cos.x<>0 by A2;
((id Z + cot-cosec)`|Z).x=diff((id Z + cot),x) -diff(cosec,x) by A1,A12,A10
,A17,FDIFF_1:19
.=((id Z + cot)`|Z).x-diff(cosec,x) by A10,A17,FDIFF_1:def 7
.=-(cos.x)^2/(sin.x)^2-diff(cosec,x) by A13,A17
.=-(cos.x)^2/(sin.x)^2-((cosec)`|Z).x by A12,A17,FDIFF_1:def 7
.=-(cos.x)^2/(sin.x)^2-(-cos.x/(sin.x)^2) by A11,A17,FDIFF_9:5
.=cos.x/(sin.x)^2-(cos.x)^2/(sin.x)^2
.=(cos.x-(cos.x)*(cos.x))/(sin.x)^2 by XCMPLX_1:120
.=cos.x*(1-cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2)
.=cos.x*(1-cos.x)/(1-(cos.x)^2) by SIN_COS:28
.=cos.x*(1-cos.x)/((1-cos.x)*(1+cos.x))
.=cos.x*(1-cos.x)/(1-cos.x)/(1+cos.x) by XCMPLX_1:78
.=cos.x*((1-cos.x)/(1-cos.x))/(1+cos.x) by XCMPLX_1:74
.=cos.x*1/(1+cos.x) by A18,XCMPLX_1:60
.=cos.x/(1+cos.x);
hence thesis;
end;
hence thesis by A1,A12,A10,FDIFF_1:19;
end;
:: f.x = cos.x/(1+cos.x)
theorem
A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x =
cos.x/(1+cos.x)) & dom (id Z+cot-cosec)=Z & Z = dom f & f|A is continuous
implies integral(f,A) =
(id Z+cot-cosec).(upper_bound A)-(id Z+cot-cosec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/(1+
cos.x) and
A3: dom (id Z+cot-cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
then
A8: (id Z+cot-cosec) is_differentiable_on Z by A3,Th49;
A9: for x being Element of REAL
st x in dom ((id Z+cot-cosec)`|Z) holds ((id Z+cot-cosec)`|Z).x = f
.x
proof
let x be Element of REAL;
assume x in dom ((id Z+cot-cosec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((id Z+cot-cosec)`|Z).x = cos.x/(1+cos.x) by A3,A7,Th49
.= f.x by A2,A10;
hence thesis;
end;
dom ((id Z+cot-cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((id Z+cot-cosec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
:: f.x = x+cot.x+cosec.x
theorem Th51:
(Z c= dom ((id Z)+cot+cosec) & for x st x in Z holds (1+cos.x)<>
0 & (1-cos.x)<>0) implies (id Z)+cot+cosec is_differentiable_on Z & for x st x
in Z holds ((id Z+cot+cosec)`|Z).x = cos.x/(cos.x-1)
proof
assume that
A1: Z c= dom ((id Z)+cot+cosec) and
A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0;
A3: Z c= dom ((id Z)+cot) /\ dom cosec by A1,VALUED_1:def 1;
then
A4: Z c= dom (id Z+cot) by XBOOLE_1:18;
then
Z c= dom id Z /\ dom cot by VALUED_1:def 1;
then
A5: Z c= dom cot by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A7: Z c= dom id Z;
then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A5,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A9: cot is_differentiable_on Z by A5,FDIFF_1:9;
then
A10: id Z + cot is_differentiable_on Z by A4,A8,FDIFF_1:18;
A11: Z c= dom cosec by A3,XBOOLE_1:18;
then
A12: cosec is_differentiable_on Z by FDIFF_9:5;
A13: for x st x in Z holds (((id Z) + cot)`|Z).x = -(cos.x)^2/(sin.x)^2
proof
let x;
assume
A14: x in Z;
then
A15: sin.x<>0 by A5,FDIFF_8:2;
then
A16: (sin.x)^2 >0 by SQUARE_1:12;
((id Z + cot)`|Z).x = diff((id Z),x) + diff(cot,x) by A4,A9,A8,A14,
FDIFF_1:18
.=((id Z)`|Z).x + diff(cot,x) by A8,A14,FDIFF_1:def 7
.=1+diff(cot,x) by A7,A6,A14,FDIFF_1:23
.=1+(-1/(sin.x)^2) by A15,FDIFF_7:47
.=1-1/(sin.x)^2
.=(sin.x)^2/(sin.x)^2-1/(sin.x)^2 by A16,XCMPLX_1:60
.=((sin.x)^2-1)/(sin.x)^2 by XCMPLX_1:120
.=((sin.x)^2-((sin.x)^2+(cos.x)^2))/(sin.x)^2 by SIN_COS:28
.=(-(cos.x)^2)/(sin.x)^2
.=-(cos.x)^2/(sin.x)^2 by XCMPLX_1:187;
hence thesis;
end;
for x st x in Z holds ((id Z + cot+cosec)`|Z).x = cos.x/(cos.x-1)
proof
let x;
assume
A17: x in Z;
then
A18: 1+cos.x<>0 by A2;
((id Z + cot+cosec)`|Z).x=diff((id Z + cot),x) +diff(cosec,x) by A1,A12,A10
,A17,FDIFF_1:18
.=((id Z + cot)`|Z).x+diff(cosec,x) by A10,A17,FDIFF_1:def 7
.=-(cos.x)^2/(sin.x)^2+diff(cosec,x) by A13,A17
.=-(cos.x)^2/(sin.x)^2+((cosec)`|Z).x by A12,A17,FDIFF_1:def 7
.=-(cos.x)^2/(sin.x)^2+(-cos.x/(sin.x)^2) by A11,A17,FDIFF_9:5
.=-((cos.x)^2/(sin.x)^2+cos.x/(sin.x)^2)
.=-((cos.x)*(cos.x)+cos.x)/(sin.x)^2 by XCMPLX_1:62
.=-(cos.x)*(cos.x+1)/((sin.x)^2+(cos.x)^2-(cos.x)^2)
.=-(cos.x)*(cos.x+1)/(1-(cos.x)^2) by SIN_COS:28
.=-(cos.x)*(cos.x+1)/((1+cos.x)*(1-cos.x))
.=-(cos.x)*(cos.x+1)/(1+cos.x)/(1-cos.x) by XCMPLX_1:78
.=-(cos.x)*((1+cos.x)/(1+cos.x))/(1-cos.x) by XCMPLX_1:74
.=-(cos.x)*1/(1-cos.x) by A18,XCMPLX_1:60
.=(cos.x)/(-(1-cos.x)) by XCMPLX_1:188
.=(cos.x)/(cos.x-1);
hence thesis;
end;
hence thesis by A1,A12,A10,FDIFF_1:18;
end;
:: f.x = cos.x/(cos.x-1)
theorem
A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x =
cos.x/(cos.x-1)) & dom (id Z+cot+cosec)=Z & Z = dom f & f|A is continuous
implies integral(f,A) =
(id Z+cot+cosec).(upper_bound A)-(id Z+cot+cosec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/(
cos.x-1) and
A3: dom (id Z+cot+cosec)=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2;
then
A8: (id Z+cot+cosec) is_differentiable_on Z by A3,Th51;
A9: for x being Element of REAL
st x in dom ((id Z+cot+cosec)`|Z) holds ((id Z+cot+cosec)`|Z).x = f
.x
proof
let x be Element of REAL;
assume x in dom ((id Z+cot+cosec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((id Z+cot+cosec)`|Z).x = cos.x/(cos.x-1) by A3,A7,Th51
.= f.x by A2,A10;
hence thesis;
end;
dom ((id Z+cot+cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((id Z+cot+cosec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
:: f.x = x-tan.x+sec.x
theorem Th53:
(Z c= dom (id Z-tan+sec) & for x st x in Z holds (1+sin.x)<>0 &
(1-sin.x)<>0) implies (id Z)-tan+sec is_differentiable_on Z & for x st x in Z
holds ((id Z-tan+sec)`|Z).x = sin.x/(sin.x+1)
proof
assume that
A1: Z c= dom (id Z-tan+sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
A3: Z c= dom (id Z-tan) /\ dom sec by A1,VALUED_1:def 1;
then
A4: Z c= dom (id Z-tan) by XBOOLE_1:18;
then
A5: Z c= dom id Z /\ dom tan by VALUED_1:12;
A6: Z c= dom (id Z);
A7: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
A9: Z c= dom tan by A5,XBOOLE_1:18;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A9,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A10: tan is_differentiable_on Z by A9,FDIFF_1:9;
then
A11: id Z-tan is_differentiable_on Z by A4,A8,FDIFF_1:19;
A12: Z c= dom sec by A3,XBOOLE_1:18;
then
A13: sec is_differentiable_on Z by FDIFF_9:4;
A14: for x st x in Z holds ((id Z - tan)`|Z).x = -(sin.x)^2/(cos.x)^2
proof
let x;
assume
A15: x in Z;
then
A16: cos.x<>0 by A9,FDIFF_8:1;
then
A17: (cos.x)^2 >0 by SQUARE_1:12;
((id Z - tan)`|Z).x = diff(id Z,x) - diff(tan,x) by A4,A10,A8,A15,
FDIFF_1:19
.=((id Z)`|Z).x - diff(tan,x) by A8,A15,FDIFF_1:def 7
.=1-diff(tan,x) by A6,A7,A15,FDIFF_1:23
.=1-1/(cos.x)^2 by A16,FDIFF_7:46
.=1-((cos.x)^2+(sin.x)^2)/(cos.x)^2 by SIN_COS:28
.=1-((cos.x)^2/(cos.x)^2+(sin.x)^2/(cos.x)^2) by XCMPLX_1:62
.=1-(1+(sin.x)^2/(cos.x)^2) by A17,XCMPLX_1:60
.=-(sin.x)^2/(cos.x)^2;
hence thesis;
end;
for x st x in Z holds ((id Z-tan+sec)`|Z).x = sin.x/(sin.x+1)
proof
let x;
assume
A18: x in Z;
then
A19: 1-sin.x<>0 by A2;
((id Z-tan+sec)`|Z).x=diff((id Z-tan),x) +diff(sec,x) by A1,A13,A11,A18,
FDIFF_1:18
.=((id Z-tan)`|Z).x+diff(sec,x) by A11,A18,FDIFF_1:def 7
.=-(sin.x)^2/(cos.x)^2+diff(sec,x) by A14,A18
.=-(sin.x)^2/(cos.x)^2+((sec)`|Z).x by A13,A18,FDIFF_1:def 7
.=-(sin.x)^2/(cos.x)^2+sin.x/(cos.x)^2 by A12,A18,FDIFF_9:4
.=sin.x/(cos.x)^2-(sin.x)^2/(cos.x)^2
.=(sin.x-(sin.x)*(sin.x))/(cos.x)^2 by XCMPLX_1:120
.=(sin.x)*(1-sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2)
.=(sin.x)*(1-sin.x)/(1-(sin.x)^2) by SIN_COS:28
.=(sin.x)*(1-sin.x)/((1-sin.x)*(1+sin.x))
.=(sin.x)*(1-sin.x)/(1-sin.x)/(1+sin.x) by XCMPLX_1:78
.=(sin.x)*((1-sin.x)/(1-sin.x))/(1+sin.x) by XCMPLX_1:74
.=(sin.x)*1/(1+sin.x) by A19,XCMPLX_1:60
.=sin.x/(1+sin.x);
hence thesis;
end;
hence thesis by A1,A13,A11,FDIFF_1:18;
end;
:: f.x = sin.x/(1+sin.x)
theorem
A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x =
sin.x/(1+sin.x)) & Z c= dom (id Z-tan+sec) & Z = dom f & f|A is continuous
implies integral(f,A) =
(id Z-tan+sec).(upper_bound A)-(id Z-tan+sec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/(1+
sin.x) and
A3: Z c= dom (id Z-tan+sec) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
then
A8: (id Z-tan+sec) is_differentiable_on Z by A3,Th53;
A9: for x being Element of REAL
st x in dom ((id Z-tan+sec)`|Z) holds ((id Z-tan+sec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((id Z-tan+sec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((id Z-tan+sec)`|Z).x = sin.x/(1+sin.x) by A3,A7,Th53
.= f.x by A2,A10;
hence thesis;
end;
dom ((id Z-tan+sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((id Z-tan+sec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
:: f.x = x-tan.x-sec.x
theorem Th55:
(Z c= dom (id Z-tan-sec) & for x st x in Z holds (1+sin.x)<>0 &
(1-sin.x)<>0) implies id Z-tan-sec is_differentiable_on Z & for x st x in Z
holds ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1)
proof
assume that
A1: Z c= dom (id Z-tan-sec) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
A3: Z c= dom (id Z-tan) /\ dom sec by A1,VALUED_1:12;
then
A4: Z c= dom (id Z-tan) by XBOOLE_1:18;
then
Z c= dom id Z /\ dom tan by VALUED_1:12;
then
A5: Z c= dom tan by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A7: Z c= dom id Z;
then
A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A5,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A9: tan is_differentiable_on Z by A5,FDIFF_1:9;
then
A10: id Z-tan is_differentiable_on Z by A4,A8,FDIFF_1:19;
A11: Z c= dom sec by A3,XBOOLE_1:18;
then
A12: sec is_differentiable_on Z by FDIFF_9:4;
A13: for x st x in Z holds ((id Z-tan)`|Z).x = -(sin.x)^2/(cos.x)^2
proof
let x;
assume
A14: x in Z;
then
A15: cos.x<>0 by A5,FDIFF_8:1;
then
A16: (cos.x)^2 >0 by SQUARE_1:12;
((id Z - tan)`|Z).x = diff(id Z,x) - diff(tan,x) by A4,A9,A8,A14,FDIFF_1:19
.=((id Z)`|Z).x - diff(tan,x) by A8,A14,FDIFF_1:def 7
.=1-diff(tan,x) by A7,A6,A14,FDIFF_1:23
.=1-1/(cos.x)^2 by A15,FDIFF_7:46
.=1-((cos.x)^2+(sin.x)^2)/(cos.x)^2 by SIN_COS:28
.=1-((cos.x)^2/(cos.x)^2+(sin.x)^2/(cos.x)^2) by XCMPLX_1:62
.=1-(1+(sin.x)^2/(cos.x)^2) by A16,XCMPLX_1:60
.=-(sin.x)^2/(cos.x)^2;
hence thesis;
end;
for x st x in Z holds ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1)
proof
let x;
assume
A17: x in Z;
then
A18: 1+sin.x<>0 by A2;
((id Z-tan-sec)`|Z).x=diff((id Z-tan),x) -diff(sec,x) by A1,A12,A10,A17,
FDIFF_1:19
.=((id Z-tan)`|Z).x-diff(sec,x) by A10,A17,FDIFF_1:def 7
.=-(sin.x)^2/(cos.x)^2-diff(sec,x) by A13,A17
.=-(sin.x)^2/(cos.x)^2-((sec)`|Z).x by A12,A17,FDIFF_1:def 7
.=-(sin.x)^2/(cos.x)^2-sin.x/(cos.x)^2 by A11,A17,FDIFF_9:4
.=-(sin.x/(cos.x)^2+(sin.x)^2/(cos.x)^2)
.=-((sin.x+(sin.x)^2)/(cos.x)^2) by XCMPLX_1:62
.=-(sin.x)*(1+sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2)
.=-(sin.x)*(1+sin.x)/(1-(sin.x)^2) by SIN_COS:28
.=-(sin.x)*(1+sin.x)/((1+sin.x)*(1-sin.x))
.=-(sin.x)*(1+sin.x)/(1+sin.x)/(1-sin.x) by XCMPLX_1:78
.=-(sin.x)*((1+sin.x)/(1+sin.x))/(1-sin.x) by XCMPLX_1:74
.=-(sin.x)*1/(1-sin.x) by A18,XCMPLX_1:60
.=sin.x/(-(1-sin.x)) by XCMPLX_1:188
.=sin.x/(sin.x-1);
hence thesis;
end;
hence thesis by A1,A12,A10,FDIFF_1:19;
end;
:: f.x = sin.x/(sin.x-1)
theorem
A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x =
sin.x/(sin.x-1)) & Z c= dom (id Z-tan-sec) & Z = dom f & f|A is continuous
implies integral(f,A) =
(id Z-tan-sec).(upper_bound A)-(id Z-tan-sec).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/(
sin.x-1) and
A3: Z c= dom (id Z-tan-sec) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2;
then
A8: (id Z-tan-sec) is_differentiable_on Z by A3,Th55;
A9: for x being Element of REAL
st x in dom ((id Z-tan-sec)`|Z) holds ((id Z-tan-sec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((id Z-tan-sec)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1) by A3,A7,Th55
.= f.x by A2,A10;
hence thesis;
end;
dom ((id Z-tan-sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7;
then ((id Z-tan-sec)`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13;
end;
:: f.x = tan.x-x
theorem Th57:
Z c= dom (tan-id Z) implies tan-id Z is_differentiable_on Z &
for x st x in Z holds ((tan-id Z)`|Z).x=(tan.x)^2
proof
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
assume
A2: Z c= dom (tan-id Z);
then
Z c= dom tan /\ dom (id Z) by VALUED_1:12;
then
A3: Z c= dom tan by XBOOLE_1:18;
A4: Z c= dom (id Z);
then
A5: id Z is_differentiable_on Z by A1,FDIFF_1:23;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A3,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds ((tan-id Z)`|Z).x=(tan.x)^2
proof
let x;
assume
A7: x in Z;
then
A8: cos.x<>0 by A3,FDIFF_8:1;
then
A9: (cos.x)^2 >0 by SQUARE_1:12;
((tan-id Z)`|Z).x= diff(tan,x) - diff(id Z,x) by A2,A5,A6,A7,FDIFF_1:19
.=1/(cos.x)^2-diff(id Z,x) by A8,FDIFF_7:46
.=1/(cos.x)^2-((id Z)`|Z).x by A5,A7,FDIFF_1:def 7
.=1/(cos.x)^2-1 by A4,A1,A7,FDIFF_1:23
.=1/(cos.x)^2-(cos.x)^2/(cos.x)^2 by A9,XCMPLX_1:60
.=(1-(cos.x)^2)/(cos.x)^2 by XCMPLX_1:120
.=((sin.x)^2+(cos.x)^2-(cos.x)^2)/(cos.x)^2 by SIN_COS:28
.=(sin(x)/cos(x))*((sin.x)/(cos.x)) by XCMPLX_1:76
.=(tan.x)*tan(x) by A3,A7,FDIFF_8:1,SIN_COS9:15
.=(tan.x)^2 by A3,A7,FDIFF_8:1,SIN_COS9:15;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:19;
end;
:: f.x = (tan.x)^2
theorem
A c= Z & (for x st x in Z holds cos.x >0 & f.x = (tan.x)^2) & Z c= dom
(tan-id Z) & Z = dom f & f|A is continuous implies integral(f,A) = (tan-id Z).(
upper_bound A)-(tan-id Z).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds cos.x >0 & f.x = (tan.x)^2 and
A3: Z c= dom (tan-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: (tan-id Z) is_differentiable_on Z by A3,Th57;
A8: for x being Element of REAL
st x in dom ((tan-id Z)`|Z) holds ((tan-id Z)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((tan-id Z)`|Z);
then
A9: x in Z by A7,FDIFF_1:def 7;
then ((tan-id Z)`|Z).x = (tan.x)^2 by A3,Th57
.= f.x by A2,A9;
hence thesis;
end;
dom ((tan-id Z)`|Z) = dom f by A4,A7,FDIFF_1:def 7;
then ((tan-id Z)`|Z) = f by A8,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;
:: f.x = -cot.x-x
theorem Th59:
Z c= dom (-cot-id Z) implies -cot-id Z is_differentiable_on Z &
for x st x in Z holds ((-cot-id Z)`|Z).x = (cot.x)^2
proof
set f = -cot;
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
assume
A2: Z c= dom (-cot-id Z);
then
Z c= dom (-cot) /\ dom (id Z) by VALUED_1:12;
then
A3: Z c= dom (-cot) by XBOOLE_1:18;
then
A4: Z c= dom cot by VALUED_1:8;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A4,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
then
A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20;
A7: Z c= dom (id Z);
then
A8: id Z is_differentiable_on Z by A1,FDIFF_1:23;
for x st x in Z holds ((-cot-id Z)`|Z).x = (cot.x)^2
proof
let x;
assume
A9: x in Z;
then
A10: sin.x<>0 by A4,FDIFF_8:2;
then
A11: (sin.x)^2 >0 by SQUARE_1:12;
((f-id Z)`|Z).x=diff(f,x) - diff(id Z,x) by A2,A8,A6,A9,FDIFF_1:19
.=(((-1)(#)cot)`|Z).x-diff(id Z,x) by A6,A9,FDIFF_1:def 7
.=(-1)*diff(cot,x)-diff(id Z,x) by A3,A5,A9,FDIFF_1:20
.=(-1)*(-1/(sin.x)^2)-diff(id Z,x) by A10,FDIFF_7:47
.=1/(sin.x)^2-((id Z)`|Z).x by A8,A9,FDIFF_1:def 7
.=1/(sin.x)^2-1 by A7,A1,A9,FDIFF_1:23
.=1/(sin.x)^2-(sin.x)^2/(sin.x)^2 by A11,XCMPLX_1:60
.=(1-(sin.x)^2)/(sin.x)^2 by XCMPLX_1:120
.=((cos.x)^2+(sin.x)^2-(sin.x)^2)/(sin.x)^2 by SIN_COS:28
.=(cos(x)/sin(x))*((cos.x)/(sin.x)) by XCMPLX_1:76
.=(cot.x)*cot(x) by A4,A9,FDIFF_8:2,SIN_COS9:16
.=(cot.x)^2 by A4,A9,FDIFF_8:2,SIN_COS9:16;
hence thesis;
end;
hence thesis by A2,A8,A6,FDIFF_1:19;
end;
:: f.x = (cot.x)^2
theorem
A c= Z & (for x st x in Z holds sin.x >0 & f.x = (cot.x)^2) & Z c= dom
(-cot-id Z) & Z = dom f & f|A is continuous implies integral(f,A) = (-cot-id Z)
.(upper_bound A)-(-cot-id Z).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds sin.x >0 & f.x = (cot.x)^2 and
A3: Z c= dom (-cot-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: (-cot-id Z) is_differentiable_on Z by A3,Th59;
A8: for x being Element of REAL
st x in dom ((-cot-id Z)`|Z) holds ((-cot-id Z)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((-cot-id Z)`|Z);
then
A9: x in Z by A7,FDIFF_1:def 7;
then ((-cot-id Z)`|Z).x = (cot.x)^2 by A3,Th59
.= f.x by A2,A9;
hence thesis;
end;
dom ((-cot-id Z)`|Z) = dom f by A4,A7,FDIFF_1:def 7;
then ((-cot-id Z)`|Z) = f by A8,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;
:: f.x = 1/(cos.x)^2
theorem
A c= Z & (for x st x in Z holds f.x = 1/(cos.x)^2 & cos.x <> 0) & dom
tan=Z & Z = dom f & f|A is continuous implies
integral(f,A) = tan.(upper_bound A)-tan.(
lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = 1/(cos.x)^2 & cos.x <> 0 and
A3: dom tan=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: tan is_differentiable_on Z by A3,INTEGRA8:33;
A8: for x being Element of REAL st x in dom (tan`|Z) holds (tan`|Z).x = f.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 A3,INTEGRA8:33
.= f.x by A2,A9;
hence thesis;
end;
dom (tan`|Z) = dom f by A4,A7,FDIFF_1:def 7;
then (tan`|Z) = f by A8,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;
:: f.x = -1/(sin.x)^2
theorem
A c= Z & (for x st x in Z holds f.x = -1/(sin.x)^2 & sin.x <> 0) & dom
cot=Z & Z = dom f & f|A is continuous implies
integral(f,A) = cot.(upper_bound A)-cot.(
lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = -1/(sin.x)^2 & sin.x <> 0 and
A3: dom cot=Z and
A4: Z = dom f and
A5: f|A is continuous;
A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11;
A7: cot is_differentiable_on Z by A3,INTEGRA8:34;
A8: for x being Element of REAL st x in dom (cot`|Z) holds (cot`|Z).x = f.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 A3,INTEGRA8:34
.= f.x by A2,A9;
hence thesis;
end;
dom (cot`|Z) = dom f by A4,A7,FDIFF_1:def 7;
then (cot`|Z) = f by A8,PARTFUN1:5;
hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13;
end;
:: f.x = (sin.x-(cos.x)^2)/(cos.x)^2
theorem
A c= Z & (for x st x in Z holds f.x = (sin.x-(cos.x)^2)/(cos.x)^2) & Z
c= dom (sec-id Z) & Z = dom f & f|A is continuous implies integral(f,A) = (sec-
id Z).(upper_bound A)-(sec-id Z).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = (sin.x-(cos.x)^2)/(cos.x)^2 and
A3: Z c= dom (sec-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: (sec-id Z) is_differentiable_on Z by A3,FDIFF_9:22;
A7: for x being Element of REAL
st x in dom ((sec-id Z)`|Z) holds ((sec-id Z)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((sec-id Z)`|Z);
then
A8: x in Z by A6,FDIFF_1:def 7;
then ((sec-id Z)`|Z).x = (sin.x-(cos.x)^2)/(cos.x)^2 by A3,FDIFF_9:22
.= f.x by A2,A8;
hence thesis;
end;
dom ((sec-id Z)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
then
A9: ((sec-id Z)`|Z) = f by A7,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
hence thesis by A1,A3,A9,FDIFF_9:22,INTEGRA5:13;
end;
:: f.x = (cos.x-(sin.x)^2)/(sin.x)^2
theorem
A c= Z & (for x st x in Z holds f.x = (cos.x-(sin.x)^2)/(sin.x)^2) & Z
c= dom (-cosec-id Z) & Z = dom f & f|A is continuous implies integral(f,A) =(-
cosec-id Z).(upper_bound A)-(-cosec-id Z).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: for x st x in Z holds f.x = (cos.x-(sin.x)^2)/(sin.x)^2 and
A3: Z c= dom (-cosec-id Z) and
A4: Z = dom f and
A5: f|A is continuous;
A6: (-cosec-id Z) is_differentiable_on Z by A3,FDIFF_9:23;
A7: for x being Element of REAL
st x in dom ((-cosec-id Z)`|Z) holds ((-cosec-id Z)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((-cosec-id Z)`|Z);
then
A8: x in Z by A6,FDIFF_1:def 7;
then ((-cosec-id Z)`|Z).x = (cos.x-(sin.x)^2)/(sin.x)^2 by A3,FDIFF_9:23
.= f.x by A2,A8;
hence thesis;
end;
dom ((-cosec-id Z)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
then
A9: ((-cosec-id Z)`|Z) = f by A7,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
hence thesis by A1,A3,A9,FDIFF_9:23,INTEGRA5:13;
end;
:: f.x = cot(x)
theorem
A c= Z & (for x st x in Z holds sin.x >0) & Z c= dom (ln*sin) & Z =
dom cot & cot|A is continuous implies
integral(cot,A) = (ln*sin).(upper_bound A)-(ln*
sin).(lower_bound A)
proof
set f = cot;
assume that
A1: A c= Z and
A2: for x st x in Z holds sin.x >0 and
A3: Z c= dom (ln*sin) and
A4: Z = dom cot and
A5: f|A is continuous;
A6: (ln*sin) is_differentiable_on Z by A2,A3,FDIFF_4:43;
A7: for x being Element of REAL
st x in dom ((ln*sin)`|Z) holds ((ln*sin)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((ln*sin)`|Z);
then
A8: x in Z by A6,FDIFF_1:def 7;
then
A9: sin.x <> 0 by A2;
((ln*sin)`|Z).x = cot(x) by A2,A3,A8,FDIFF_4:43
.= f.x by A9,SIN_COS9:16;
hence thesis;
end;
dom ((ln*sin)`|Z) = dom f by A4,A6,FDIFF_1:def 7;
then
A10: ((ln*sin)`|Z) = f by A7,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11;
hence thesis by A1,A2,A3,A10,FDIFF_4:43,INTEGRA5:13;
end;
:: f.x = arcsin.x / sqrt(1-x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=arcsin.x/sqrt(1-
x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) & Z = dom f & f|A is continuous
implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arcsin))).(upper_bound A)
-((1/2)(#)(( #Z 2)
*(arcsin))).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=arcsin.x/sqrt(1-x^2) and
A4: Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) and
A5: Z = dom f and
A6: f|A is continuous;
A7: ((1/2)(#)(( #Z 2)*(arcsin))) is_differentiable_on Z by A2,A4,FDIFF_7:12;
A8: for x being Element of REAL
st x in dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) holds (((1/2)(#)(( #Z
2)*(arcsin)))`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z);
then
A9: x in Z by A7,FDIFF_1:def 7;
then
(((1/2)(#)(( #Z 2)*(arcsin)))`|Z).x = arcsin.x / sqrt(1-x^2) by A2,A4,
FDIFF_7:12
.= f.x by A3,A9;
hence thesis;
end;
dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) = dom f by A5,A7,FDIFF_1:def 7;
then
A10: (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) = f by A8,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A5,A6,INTEGRA5:10,11;
hence thesis by A1,A2,A4,A10,FDIFF_7:12,INTEGRA5:13;
end;
:: f.x = -arccos.x / sqrt(1-x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-arccos.x / sqrt
(1-x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) & Z = dom f & f|A is
continuous implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arccos))).(upper_bound A)
-((1/2)
(#)(( #Z 2)*(arccos))).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=-arccos.x / sqrt(1-x^2) and
A4: Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) and
A5: Z = dom f and
A6: f|A is continuous;
A7: ((1/2)(#)(( #Z 2)*(arccos))) is_differentiable_on Z by A2,A4,FDIFF_7:13;
A8: for x being Element of REAL
st x in dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z) holds (((1/2)(#)(( #Z
2)*(arccos)))`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z);
then
A9: x in Z by A7,FDIFF_1:def 7;
then (((1/2)(#)(( #Z 2)*(arccos)))`|Z).x = -arccos.x / sqrt(1-x^2) by A2,A4
,FDIFF_7:13
.= f.x by A3,A9;
hence thesis;
end;
dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z) = dom f by A5,A7,FDIFF_1:def 7;
then
A10: (((1/2)(#)(( #Z 2)*(arccos)))`|Z) = f by A8,PARTFUN1:5;
f is_integrable_on A & f|A is bounded by A1,A5,A6,INTEGRA5:10,11;
hence thesis by A1,A2,A4,A10,FDIFF_7:13,INTEGRA5:13;
end;
:: f.x = arcsin.x
theorem
A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=1 & f.x >0 & x<>0) & dom arcsin=Z & Z c= dom ((id Z)(#)(arcsin)+( #R (1/2)
)*f) implies integral(arcsin,A) =
((id Z)(#)(arcsin)+( #R (1/2))*f).(upper_bound A) -((
id Z)(#)(arcsin) + ( #R (1/2))*f).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ & f=f1-f2 &( f2=#Z 2 & for x st x in Z holds f1.x=1
& f.x >0 & x<>0 ) and
A3: dom arcsin=Z and
A4: Z c= dom ((id Z)(#)(arcsin)+( #R (1/2))*f);
A5: arcsin|A is bounded by A1,A3,INTEGRA5:10;
A6: ((id Z)(#)(arcsin)+( #R (1/2))*f) is_differentiable_on Z by A2,A4,
FDIFF_7:23;
A7: for x being Element of REAL
st x in dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) holds (((id Z)
(#)(arcsin)+( #R (1/2))*f)`|Z).x = arcsin.x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z);
then x in Z by A6,FDIFF_1:def 7;
hence thesis by A2,A4,FDIFF_7:23;
end;
dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) = dom arcsin by A3,A6,
FDIFF_1:def 7;
then (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) = arcsin by A7,PARTFUN1:5;
hence thesis by A1,A3,A5,A6,INTEGRA5:11,13;
end;
:: f.x = arcsin.(x/a)
theorem
A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0
& f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arcsin)*f3)=Z & Z c=
dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) & ((arcsin)*f3)|A is continuous
implies integral((arcsin)*f3,A) =
((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(upper_bound A
) -((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: f=f1-f2 & f2=#Z 2 and
A3: for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3
.x < 1 & x<>0 & a>0 and
A4: dom ((arcsin)*f3)=Z and
A5: Z c= dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) and
A6: ((arcsin)*f3)|A is continuous;
A7: (arcsin)*f3 is_integrable_on A by A1,A4,A6,INTEGRA5:11;
A8: ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) is_differentiable_on Z by A2,A3,A5,
FDIFF_7:28;
A9: for x being Element of REAL
st x in dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) holds (((id
Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = ((arcsin)*f3).x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then
(((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = arcsin.(x/a) by A2,A3,A5,
FDIFF_7:28
.= arcsin.(f3.x) by A3,A10
.= ((arcsin)*f3).x by A4,A10,FUNCT_1:12;
hence thesis;
end;
dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) = dom ((arcsin)*f3) by A4,A8,
FDIFF_1:def 7;
then (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) = (arcsin)*f3 by A9,
PARTFUN1:5;
hence thesis by A1,A4,A6,A7,A8,INTEGRA5:10,13;
end;
:: f.x = arccos.x
theorem
A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=1 & f.x >0 & x<>0) & dom arccos=Z & Z c= dom ((id Z)(#)(arccos)-( #R (1/2)
)*f) implies integral(arccos,A)
= ((id Z)(#)(arccos)-( #R (1/2))*f).(upper_bound A) -((
id Z)(#)(arccos)-( #R (1/2))*f).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ & f=f1-f2 &( f2=#Z 2 & for x st x in Z holds f1.x=1
& f.x >0 & x<>0 ) and
A3: dom arccos=Z and
A4: Z c= dom ((id Z)(#)(arccos)-( #R (1/2))*f);
A5: arccos|A is bounded by A1,A3,INTEGRA5:10;
A6: ((id Z)(#)(arccos)-( #R (1/2))*f) is_differentiable_on Z by A2,A4,
FDIFF_7:24;
A7: for x being Element of REAL
st x in dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) holds (((id Z)
(#)(arccos)-( #R (1/2))*f)`|Z).x = arccos.x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z);
then x in Z by A6,FDIFF_1:def 7;
hence thesis by A2,A4,FDIFF_7:24;
end;
dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) = dom arccos by A3,A6,
FDIFF_1:def 7;
then (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) = arccos by A7,PARTFUN1:5;
hence thesis by A1,A3,A5,A6,INTEGRA5:11,13;
end;
:: f.x = arccos.(x/a)
theorem
A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0
& f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arccos)*f3)=Z & Z = dom
((id Z)(#)((arccos)*f3)-( #R (1/2))*f) & ((arccos)*f3)|A is continuous implies
integral((arccos)*f3,A) =
((id Z)(#)((arccos)*f3)-( #R (1/2))*f).(upper_bound A) -((id
Z)(#)((arccos)*f3)-( #R (1/2))*f).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: f=f1-f2 & f2=#Z 2 and
A3: for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3
.x < 1 & x<>0 & a>0 and
A4: dom ((arccos)*f3)=Z and
A5: Z = dom ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) and
A6: ((arccos)*f3)|A is continuous;
A7: (arccos)*f3 is_integrable_on A by A1,A4,A6,INTEGRA5:11;
A8: ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) is_differentiable_on Z by A2,A3,A5,
FDIFF_7:29;
A9: for x being Element of REAL
st x in dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) holds (((id
Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = ((arccos)*f3).x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z);
then
A10: x in Z by A8,FDIFF_1:def 7;
then
(((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = arccos.(x/a) by A2,A3,A5,
FDIFF_7:29
.= arccos.(f3.x) by A3,A10
.= ((arccos)*f3).x by A4,A10,FUNCT_1:12;
hence thesis;
end;
dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) = dom ((arccos)*f3) by A4,A8,
FDIFF_1:def 7;
then (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) = (arccos)*f3 by A9,
PARTFUN1:5;
hence thesis by A1,A4,A6,A7,A8,INTEGRA5:10,13;
end;
:: f.x = arctan.x
theorem
A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1 ) &
Z = dom arctan & Z = dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) implies
integral(arctan,A) =
((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)
(#)(arctan)-(1/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: f2=#Z 2 & for x st x in Z holds f1.x=1 and
A4: Z = dom arctan and
A5: Z = dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)));
].-1,1 .[ c= [.-1,1 .] & A c= ].-1,1 .[ by A1,A2,XBOOLE_1:1,XXREAL_1:25;
then arctan|A is continuous by FCONT_1:16,SIN_COS9:53,XBOOLE_1:1;
then
A6: arctan is_integrable_on A & arctan|A is bounded by A1,A4,INTEGRA5:10,11;
A7: ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A2,A3,A5
,SIN_COS9:103;
A8: for x being Element of REAL
st x in dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) holds ((
(id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z).x = arctan.x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z);
then x in Z by A7,FDIFF_1:def 7;
hence thesis by A2,A3,A5,SIN_COS9:103;
end;
dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) = dom arctan by A4,A7,
FDIFF_1:def 7;
then (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) = arctan by A8,PARTFUN1:5;
hence thesis by A1,A2,A3,A5,A6,INTEGRA5:13,SIN_COS9:103;
end;
:: f.x = arccot.x
theorem
A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1) &
dom arccot=Z & Z = dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) implies
integral(arccot,A) =
((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)
(#)(arccot)+(1/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
assume that
A1: A c= Z and
A2: Z c= ]. -1,1 .[ and
A3: f2=#Z 2 & for x st x in Z holds f1.x=1 and
A4: dom arccot=Z and
A5: Z = dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)));
].-1,1 .[ c= [.-1,1 .] & A c= ].-1,1 .[ by A1,A2,XBOOLE_1:1,XXREAL_1:25;
then arccot|A is continuous by FCONT_1:16,SIN_COS9:54,XBOOLE_1:1;
then
A6: arccot is_integrable_on A & arccot|A is bounded by A1,A4,INTEGRA5:10,11;
A7: ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A2,A3,A5
,SIN_COS9:104;
A8: for x being Element of REAL
st x in dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) holds ((
(id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z).x = arccot.x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z);
then x in Z by A7,FDIFF_1:def 7;
hence thesis by A2,A3,A5,SIN_COS9:104;
end;
dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) = dom arccot by A4,A7,
FDIFF_1:def 7;
then (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) = arccot by A8,PARTFUN1:5;
hence thesis by A1,A2,A3,A5,A6,INTEGRA5:13,SIN_COS9:104;
end;