:: Integrability Formulas -- Part {I}
:: by Bo Li and Na Ma
::
:: Received November 7, 2009
:: Copyright (c) 2009-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 RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, INTEGRA1, FDIFF_1, XBOOLE_0,
SQUARE_1, ARYTM_3, ORDINAL2, RCOMP_1, PREPOWER, NEWTON, NUMBERS, REAL_1,
SUBSET_1, XXREAL_0, XXREAL_1, PARTFUN1, TAYLOR_1, SIN_COS6, SIN_COS9,
LIMFUNC1, TARSKI, VALUED_1, CARD_1, ORDINAL4, INTEGRA5, NAT_1, XXREAL_2,
SEQ_4, MEASURE5;
notations TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SIN_COS, SUBSET_1, ORDINAL1,
NUMBERS, VALUED_1, XCMPLX_0, NAT_1, XXREAL_0, XREAL_0, REAL_1, RELSET_1,
PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, MEASURE6, INTEGRA1,
FCONT_1, SQUARE_1, INTEGRA5, TAYLOR_1, FDIFF_1, SEQ_2, SEQ_4, SIN_COS6,
SIN_COS9, NEWTON, LIMFUNC1, PREPOWER;
constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, MEASURE6, BINOP_2,
SQUARE_1, PREPOWER, INTEGRA5, SEQ_4, XXREAL_3, XBOOLE_0, SEQ_2, LIMFUNC1,
NAT_1, POWER, RELSET_1, TARSKI, SIN_COS9, PARTFUN1, PARTFUN2, FUNCT_1,
RCOMP_1, RELAT_1, SIN_COS6, RFUNCT_1, VALUED_1, FDIFF_9, NEWTON,
INTEGRA1, COMSEQ_2;
registrations NAT_1, NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, ORDINAL1,
FUNCT_2, RCOMP_1, RELSET_1, XREAL_0, NEWTON, SQUARE_1, MEASURE5,
PREPOWER;
requirements NUMERALS, SUBSET, ARITHM, REAL;
definitions TARSKI;
equalities SIN_COS, VALUED_1, SQUARE_1, LIMFUNC1, XCMPLX_0;
expansions TARSKI;
theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, XCMPLX_1, RELAT_1, INTEGRA5,
SIN_COS, FDIFF_4, TAYLOR_1, VALUED_1, FCONT_1, SIN_COS6, XXREAL_1,
XBOOLE_1, PREPOWER, FDIFF_2, XREAL_1, NAT_1, FDIFF_5, FDIFF_7, FDIFF_8,
SIN_COS9, XBOOLE_0, XREAL_0;
begin
reserve a,b,x,r for Real;
reserve y for set;
reserve n for Element of NAT;
reserve A for non empty closed_interval Subset of REAL;
reserve f,g,f1,f2,g1,g2 for PartFunc of REAL,REAL;
reserve Z for open Subset of REAL;
theorem Th1:
Z c= dom ((f1+f2)^) & (for x st x in Z holds f1.x=1) & f2=#Z 2
implies (f1+f2)^ is_differentiable_on Z & for x st x in Z holds
(((f1+f2)^)`|Z).x = -2*x/(1+x |^2)^2
proof
assume
A1:Z c= dom ((f1+f2)^) & (for x st x in Z holds f1.x=1) & f2=#Z 2;
dom ((f1+f2)^) c= dom (f1+f2) by RFUNCT_1:1;
then A2:Z c= dom (f1+f2) by A1;
then A3:f1+f2 is_differentiable_on Z &
for x st x in Z holds ((f1+f2)`|Z).x = 2*x by A1,SIN_COS9:101;
A4:for x st x in Z holds (f1+f2).x<>0 by A1,RFUNCT_1:3;
then A5:(f1+f2)^ is_differentiable_on Z by A3,FDIFF_2:22;
for x st x in Z holds (((f1+f2)^)`|Z).x = -2*x/(1+x |^2)^2
proof
let x;
assume
A6: x in Z; then
A7: (f1+f2).x<>0 by A1,RFUNCT_1:3;
A8: f1+f2 is_differentiable_in x by A3,A6,FDIFF_1:9;
A9:f2.x=x #Z 2 by A1,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36;
A10:(f1+f2).x=f1.x+f2.x by A2,A6,VALUED_1:def 1
.=1+x |^2 by A1,A6,A9;
(((f1+f2)^)`|Z).x = diff((f1+f2)^,x) by A5,A6,FDIFF_1:def 7
.= - diff((f1+f2),x)/((f1+f2).x)^2 by A7,A8,FDIFF_2:15
.= -((f1+f2)`|Z).x/((f1+f2).x)^2 by A3,A6,FDIFF_1:def 7
.= -2*x/(1+x |^2)^2 by A1,A2,A6,A10,SIN_COS9:101;
hence thesis;
end;
hence thesis by A3,A4,FDIFF_2:22;
end;
::f.x=1/((1+x^2)*arccot.x)
theorem
A c= Z & f = ((g1+g2)^)/f2 & f2 = arccot & Z c= ]. -1,1 .[ & g2=#Z 2
& (for x st x in Z holds g1.x=1 & f2.x>0) & Z = dom f implies
integral(f,A)=(-ln*arccot).(upper_bound A)-(-ln*arccot).(lower_bound A)
proof
assume
A1:A c= Z & f = ((g1+g2)^)/f2 & f2 = arccot & Z c= ]. -1,1 .[ & g2=#Z 2
& (for x st x in Z holds g1.x=1 & f2.x>0) & Z = dom f;
then Z = dom ((g1+g2)^) /\ (dom f2 \ f2"{0}) by RFUNCT_1:def 1;
then A2: Z c= dom ((g1+g2)^) & Z c= dom f2 \ f2"{0} by XBOOLE_1:18;
dom ((g1+g2)^) c= dom (g1+g2) by RFUNCT_1:1;then
A3:Z c= dom (g1+g2) by A2;
for x st x in Z holds g1.x=1 by A1;
then A4: (g1+g2)^ is_differentiable_on Z by A1,A2,Th1;
A5: f2 is_differentiable_on Z by A1,SIN_COS9:82;
for x st x in Z holds f2.x<>0 by A1;
then f is_differentiable_on Z by A1,A4,A5,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;
then A6:f|A is continuous by A1,FCONT_1:16;
A7:Z c= dom (f2^) by A2,RFUNCT_1:def 2;
dom (f2^) c= dom f2 by RFUNCT_1:1;then
A8:Z c= dom f2 by A7;
A9:for x st x in Z holds f2.x>0 by A1;
rng (f2|Z) c= right_open_halfline(0)
proof
let x be object;
assume x in rng (f2|Z); then
consider y be object such that
A10: y in dom (f2|Z) & x = (f2|Z).y by FUNCT_1:def 3;
y in Z by A10; then
f2.y > 0 by A1; then
(f2|Z).y > 0 by A10,FUNCT_1:47;
hence thesis by A10,XXREAL_1:235;
end;
then f2.:Z c= dom ln by RELAT_1:115,TAYLOR_1:18;
then A11:Z c= dom (ln*arccot) by A1,A8,FUNCT_1:101;
A12:f is_integrable_on A & f|A is bounded by A1,A6,INTEGRA5:10,11;
A13:ln*arccot is_differentiable_on Z by A1,A11,A9,SIN_COS9:90;
Z c= dom (-ln*arccot) by A11,VALUED_1:8;
then A14:-ln*arccot is_differentiable_on Z by A13,FDIFF_1:20;
A15:for x st x in Z holds ((-ln*arccot)`|Z).x = 1/((1+x^2)*arccot.x)
proof
let x;
assume
A16:x in Z;then
A17:-1 < x & x < 1 by A1,XXREAL_1:4;
arccot is_differentiable_on Z by A1,SIN_COS9:82;then
A18:arccot is_differentiable_in x by A16,FDIFF_1:9;
A19:arccot.x >0 by A1,A16;
A20:ln*arccot is_differentiable_in x by A13,A16,FDIFF_1:9;
((-ln*arccot)`|Z).x=diff((-ln*arccot),x) by A14,A16,FDIFF_1:def 7
.=(-1)*diff(ln*arccot,x) by A20,FDIFF_1:15
.=(-1)*(diff(arccot,x)/arccot.x) by A18,A19,TAYLOR_1:20
.=(-1)*((-1/(1+x^2))/arccot.x) by A17,SIN_COS9:76
.= (1/(1+x^2))/arccot.x
.= 1/((1+x^2)*arccot.x) by XCMPLX_1:78;
hence thesis;
end;
A21:for x being Real st x in Z holds f.x=1/((1+x^2)*arccot.x)
proof
let x be Real;
assume
A22:x in Z;
then (((g1+g2)^)/f2).x =((g1+g2)^).x/f2.x by A1,RFUNCT_1:def 1
.=((g1+g2).x)"/f2.x by A2,A22,RFUNCT_1:def 2
.=(g1.x+g2.x)"/f2.x by A3,A22,VALUED_1:def 1
.=1/((g1.x+g2.x)*f2.x) by XCMPLX_1:221
.=1/((1+( #Z 2).x)*f2.x) by A1,A22
.=1/((1+(x #Z 2))*f2.x) by TAYLOR_1:def 1
.=1/((1+x^2)*arccot.x) by A1,FDIFF_7:1;
hence thesis by A1;
end;
A23:for x being Element of REAL
st x in dom ((-ln*arccot)`|Z) holds ((-ln*arccot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-ln*arccot)`|Z);then
A24:x in Z by A14,FDIFF_1:def 7;then
((-ln*arccot)`|Z).x=1/((1+x^2)*arccot.x) by A15
.=f.x by A21,A24;
hence thesis;
end;
dom ((-ln*arccot)`|Z)=dom f by A1,A14,FDIFF_1:def 7;
then ((-ln*arccot)`|Z)= f by A23,PARTFUN1:5;
hence thesis by A1,A12,A14,INTEGRA5:13;
end;
::f.x=exp_R.x/(1+(exp_R.x)^2)
theorem
A c= Z & (for x st x in Z holds exp_R.x < 1 & f1.x=1)
& Z c= dom (arctan*exp_R)
& Z = dom f & f=exp_R/(f1+(exp_R)^2)
implies integral(f,A)=(arctan*exp_R).(upper_bound A)
-(arctan*exp_R).(lower_bound A)
proof
assume
A1: A c= Z & (for x st x in Z holds exp_R.x < 1 & f1.x=1)
& Z c= dom (arctan*exp_R)
& Z = dom f & f=exp_R/(f1+(exp_R)^2);
then Z c= dom exp_R /\ (dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0})
by RFUNCT_1:def 1;
then Z c= dom exp_R & Z c= dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0}
by XBOOLE_1:18;
then A2:Z c= dom ((f1+(exp_R)^2)^) by RFUNCT_1:def 2;
dom ((f1+(exp_R)^2)^) c= dom (f1+(exp_R)^2) by RFUNCT_1:1;then
A3:Z c= dom (f1+(exp_R)^2) by A2;
then A4:Z c= dom f1 /\ dom ((exp_R)^2) by VALUED_1:def 1;
then A5:Z c= dom f1 & Z c= dom ((exp_R)^2) by XBOOLE_1:18;
A6:Z c= dom ((exp_R)(#)(exp_R)) by A4,XBOOLE_1:18;
A7:exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then A8:(exp_R)(#)(exp_R) is_differentiable_on Z by A6,FDIFF_1:21;
for x st x in Z holds f1.x=0*x+1 by A1;
then f1 is_differentiable_on Z by A5,FDIFF_1:23;
then A9:f1+(exp_R)^2 is_differentiable_on Z by A3,A8,FDIFF_1:18;
for x st x in Z holds (f1+(exp_R)^2).x<>0
proof
let x;
assume x in Z;then
x in dom exp_R /\ (dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0})
by A1,RFUNCT_1:def 1;then
x in dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0} by XBOOLE_0:def 4; then
x in dom ((f1+(exp_R)^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then f is_differentiable_on Z by A1,A7,A9,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;
then f|A is continuous by A1,FCONT_1:16;
then A10:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A11:for x st x in Z holds exp_R.x < 1 by A1;then
A12:arctan*exp_R is_differentiable_on Z by A1,SIN_COS9:115;
A13:for x st x in Z holds f.x=exp_R.x/(1+(exp_R.x)^2)
proof
let x;
assume
A14:x in Z;
then (exp_R/(f1+(exp_R)^2)).x=(exp_R.x)*((f1+(exp_R)^2).x)"
by A1,RFUNCT_1:def 1
.=(exp_R.x)*(f1.x+((exp_R)^2).x)"
by A14,A3,VALUED_1:def 1
.=(exp_R.x)*(f1.x+(exp_R.x)^2)"
by VALUED_1:11
.=exp_R.x/(1+(exp_R.x)^2) by A1,A14;
hence thesis by A1;
end;
A15:for x being Element of REAL
st x in dom ((arctan*exp_R)`|Z) holds ((arctan*exp_R)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((arctan*exp_R)`|Z);then
A16:x in Z by A12,FDIFF_1:def 7;then
((arctan*exp_R)`|Z).x=exp_R.x/(1+(exp_R.x)^2) by A1,A11,SIN_COS9:115
.=f.x by A16,A13;
hence thesis;
end;
dom ((arctan*exp_R)`|Z)=dom f by A1,A12,FDIFF_1:def 7;
then ((arctan*exp_R)`|Z)= f by A15,PARTFUN1:5;
hence thesis by A1,A10,A12,INTEGRA5:13;
end;
::f.x=-exp_R.x/(1+(exp_R.x)^2)
theorem
A c= Z & (for x st x in Z holds exp_R.x < 1 & f1.x=1)
& Z c= dom (arccot*exp_R) & Z = dom f & f=(-exp_R)/(f1+(exp_R)^2)
implies integral(f,A)=(arccot*exp_R).(upper_bound A)
-(arccot*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds exp_R.x < 1 & f1.x=1)
& Z c= dom (arccot*exp_R) & Z = dom f
& f=(-exp_R)/(f1+(exp_R)^2);
then Z c= dom (-exp_R) /\ (dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0})
by RFUNCT_1:def 1;
then A2:Z c= dom (-exp_R) & Z c= dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0}
by XBOOLE_1:18;
then A3:Z c= dom ((f1+(exp_R)^2)^) by RFUNCT_1:def 2;
dom ((f1+(exp_R)^2)^) c= dom (f1+(exp_R)^2) by RFUNCT_1:1;then
A4:Z c= dom (f1+(exp_R)^2) by A3;
then A5:Z c= dom f1 /\ dom ((exp_R)^2) by VALUED_1:def 1;
then A6:Z c= dom f1 & Z c= dom ((exp_R)^2) by XBOOLE_1:18;
A7:Z c= dom ((exp_R)(#)(exp_R)) by A5,XBOOLE_1:18;
A8:exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then A9:(-1)(#)(exp_R) is_differentiable_on Z by A2,FDIFF_1:20;
A10:(exp_R)(#)(exp_R) is_differentiable_on Z by A7,A8,FDIFF_1:21;
for x st x in Z holds f1.x=0*x+1 by A1;
then f1 is_differentiable_on Z by A6,FDIFF_1:23;
then A11:f1+(exp_R)^2 is_differentiable_on Z by A4,A10,FDIFF_1:18;
for x st x in Z holds (f1+(exp_R)^2).x<>0
proof
let x;
assume x in Z;then
x in dom (-exp_R) /\ (dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0})
by A1,RFUNCT_1:def 1;then
x in dom (f1+(exp_R)^2) \ (f1+(exp_R)^2)"{0} by XBOOLE_0:def 4; then
x in dom ((f1+(exp_R)^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then f is_differentiable_on Z by A1,A9,A11,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;
then f|A is continuous by A1,FCONT_1:16;
then A12:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A13:for x st x in Z holds exp_R.x < 1 by A1;then
A14:arccot*exp_R is_differentiable_on Z by A1,SIN_COS9:116;
A15:for x being Element of REAL st x in Z holds f.x=-exp_R.x/(1+(exp_R.x)^2)
proof
let x be Element of REAL;
assume
A16:x in Z;
then ((-exp_R)/(f1+(exp_R)^2)).x=((-exp_R).x)*((f1+(exp_R)^2).x)"
by A1,RFUNCT_1:def 1
.=(-exp_R.x)*((f1+(exp_R)^2).x)"
by RFUNCT_1:58
.=(-exp_R.x)*(f1.x+((exp_R)^2).x)"
by A16,A4,VALUED_1:def 1
.=(-exp_R.x)*(f1.x+(exp_R.x)^2)"
by VALUED_1:11
.=(-exp_R.x)/(1+(exp_R.x)^2) by A1,A16
.=-exp_R.x/(1+(exp_R.x)^2);
hence thesis by A1;
end;
A17:for x being Element of REAL
st x in dom ((arccot*exp_R)`|Z) holds ((arccot*exp_R)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((arccot*exp_R)`|Z);then
A18:x in Z by A14,FDIFF_1:def 7;
then
((arccot*exp_R)`|Z).x=-exp_R.x/(1+(exp_R.x)^2) by A1,A13,SIN_COS9:116
.=f.x by A18,A15;
hence thesis;
end;
dom ((arccot*exp_R)`|Z)=dom f by A1,A14,FDIFF_1:def 7;
then ((arccot*exp_R)`|Z)= f by A17,PARTFUN1:5;
hence thesis by A1,A12,A14,INTEGRA5:13;
end;
::f.x=exp_R.x*sin.x/cos.x+exp_R.x/(cos.x)^2
theorem
A c= Z & Z = dom f & f=exp_R(#)(sin/cos)+exp_R/cos^2 implies
integral(f,A)=(exp_R(#)tan).(upper_bound A)-(exp_R(#)tan).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom f & f=exp_R(#)(sin/cos)+exp_R/cos^2;
then Z = dom (exp_R(#)(sin/cos)) /\ dom (exp_R/cos^2) by VALUED_1:def 1;
then
A2:Z c= dom (exp_R(#)(sin/cos)) & Z c= dom (exp_R/cos^2) by XBOOLE_1:18;
A3:dom (exp_R(#)(sin/cos)) c= dom exp_R /\ dom (sin/cos) by VALUED_1:def 4;
dom (exp_R/cos^2) c= dom exp_R /\ (dom cos^2 \ (cos^2)"{0})
by RFUNCT_1:def 1;
then dom (exp_R(#)(sin/cos)) c= dom exp_R &
dom (exp_R(#)(sin/cos)) c= dom (sin/cos) &
dom (exp_R/cos^2) c= dom cos^2 \ (cos^2)"{0} by A3,XBOOLE_1:18; then
A4:Z c= dom exp_R & Z c= dom (sin/cos) & Z c= dom cos^2 \ (cos^2)"{0}
by A2;
A5:exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds sin/cos is_differentiable_in x
proof
let x;
assume x in Z;then
cos.x<>0 by A4,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then sin/cos is_differentiable_on Z by A4,FDIFF_1:9;
then A6:exp_R(#)(sin/cos) is_differentiable_on Z by A2,A5,FDIFF_1:21;
cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then A7:cos^2 is_differentiable_on Z by FDIFF_2:20;
x in Z implies (cos^2).x<>0
proof
assume x in Z;then
x in dom (exp_R/cos^2) by A2;
then x in dom exp_R /\ (dom cos^2 \ (cos^2)"{0}) by RFUNCT_1:def 1;
then x in dom cos^2 \ (cos^2)"{0} by XBOOLE_0:def 4;
then x in dom ((cos^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then exp_R/cos^2 is_differentiable_on Z by A5,A7,FDIFF_2:21;
then f|Z is continuous by A1,A6,FDIFF_1:18,25;then
f|A is continuous by A1,FCONT_1:16;
then A8:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A9:(exp_R(#)tan) is_differentiable_on Z by A2,FDIFF_8:30;
A10:for x st x in Z holds f.x=exp_R.x*sin.x/cos.x+exp_R.x/(cos.x)^2
proof
let x;
assume
A11:x in Z;
then (exp_R(#)(sin/cos)+exp_R/cos^2).x
=((exp_R(#)(sin/cos)).x)+(exp_R/cos^2).x by A1,VALUED_1:def 1
.=((exp_R.x)*((sin/cos).x))+(exp_R/cos^2).x by VALUED_1:5
.=((exp_R.x)*(sin.x*(cos.x)"))+(exp_R/cos^2).x by A4,A11,RFUNCT_1:def 1
.=(exp_R.x)*sin.x/cos.x+exp_R.x/(cos^2).x by A2,A11,RFUNCT_1:def 1
.=exp_R.x*sin.x/cos.x+exp_R.x/(cos.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A12:for x being Element of REAL
st x in dom((exp_R(#)tan)`|Z) holds ((exp_R(#)tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((exp_R(#)tan)`|Z);then
A13: x in Z by A9,FDIFF_1:def 7; then
((exp_R(#)tan)`|Z).x=exp_R.x*sin.x/cos.x+exp_R.x/(cos.x)^2 by A2,FDIFF_8:30
.=f.x by A13,A10;
hence thesis;
end;
dom((exp_R(#)tan)`|Z)=dom f by A1,A9,FDIFF_1:def 7;
then ((exp_R(#)tan)`|Z)= f by A12,PARTFUN1:5;
hence thesis by A1,A8,A2,FDIFF_8:30,INTEGRA5:13;
end;
::f.x=exp_R.x*cos.x/sin.x-exp_R.x/(sin.x)^2
theorem
A c= Z & Z = dom f & f=exp_R(#)(cos/sin)-exp_R/sin^2 implies
integral(f,A)=(exp_R(#)cot).(upper_bound A)-(exp_R(#)cot).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom f & f=exp_R(#)(cos/sin)-exp_R/sin^2;
then Z = dom (exp_R(#)(cos/sin)) /\ dom (exp_R/sin^2) by VALUED_1:12;
then
A2:Z c= dom (exp_R(#)(cos/sin)) & Z c= dom (exp_R/sin^2) by XBOOLE_1:18;
A3:dom (exp_R(#)(cos/sin)) c= dom exp_R /\ dom (cos/sin) by VALUED_1:def 4;
dom (exp_R/sin^2) c= dom exp_R /\ (dom sin^2 \ (sin^2)"{0})
by RFUNCT_1:def 1;
then dom (exp_R(#)(cos/sin)) c= dom exp_R &
dom (exp_R(#)(cos/sin)) c= dom (cos/sin) &
dom (exp_R/sin^2) c= dom sin^2 \ (sin^2)"{0} by A3,XBOOLE_1:18; then
A4:Z c= dom exp_R & Z c= dom (cos/sin) & Z c= dom sin^2 \ (sin^2)"{0}
by A2;
A5:exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds cos/sin 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 cos/sin is_differentiable_on Z by A4,FDIFF_1:9;
then A6:exp_R(#)(cos/sin) is_differentiable_on Z by A2,A5,FDIFF_1:21;
sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then A7:sin^2 is_differentiable_on Z by FDIFF_2:20;
x in Z implies (sin^2).x<>0
proof
assume x in Z;then
x in dom (exp_R/sin^2) by A2;
then x in dom exp_R /\ (dom sin^2 \ (sin^2)"{0}) by RFUNCT_1:def 1;
then x in dom sin^2 \ (sin^2)"{0} by XBOOLE_0:def 4;
then x in dom ((sin^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then exp_R/sin^2 is_differentiable_on Z by A5,A7,FDIFF_2:21;
then f|Z is continuous by A1,A6,FDIFF_1:19,25;then
f|A is continuous by A1,FCONT_1:16;
then A8:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A9:(exp_R(#)cot) is_differentiable_on Z by A2,FDIFF_8:31;
A10:for x st x in Z holds f.x=exp_R.x*cos.x/sin.x-exp_R.x/(sin.x)^2
proof
let x;
assume
A11:x in Z;
then (exp_R(#)(cos/sin)-exp_R/sin^2).x
=((exp_R(#)(cos/sin)).x)-(exp_R/sin^2).x by A1,VALUED_1:13
.=((exp_R.x)*((cos/sin).x))-(exp_R/sin^2).x by VALUED_1:5
.=((exp_R.x)*(cos.x*(sin.x)"))-(exp_R/sin^2).x
by A4,A11,RFUNCT_1:def 1
.=exp_R.x*cos.x/sin.x-exp_R.x/(sin^2).x by A2,A11,RFUNCT_1:def 1
.=exp_R.x*cos.x/sin.x-exp_R.x/(sin.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A12:for x being Element of REAL
st x in dom((exp_R(#)cot)`|Z) holds ((exp_R(#)cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((exp_R(#)cot)`|Z);then
A13: x in Z by A9,FDIFF_1:def 7; then
((exp_R(#)cot)`|Z).x=exp_R.x*cos.x/sin.x-exp_R.x/(sin.x)^2 by A2,FDIFF_8:31
.=f.x by A13,A10;
hence thesis;
end;
dom((exp_R(#)cot)`|Z)=dom f by A1,A9,FDIFF_1:def 7;
then ((exp_R(#)cot)`|Z)= f by A12,PARTFUN1:5;
hence thesis by A1,A8,A2,FDIFF_8:31,INTEGRA5:13;
end;
::f.x=exp_R.x*arctan.x+exp_R.x/(1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f
& f=exp_R(#)arctan+exp_R/(f1+#Z 2) implies
integral(f,A
)=(exp_R(#)arctan).(upper_bound A)-(exp_R(#)arctan).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f
& f=exp_R(#)arctan+exp_R/(f1+#Z 2);
then A2:Z = dom (exp_R(#)arctan) /\ dom (exp_R/(f1+#Z 2)) by VALUED_1:def 1;
A3:exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
A4:exp_R(#)arctan is_differentiable_on Z by A1,SIN_COS9:123;
A5:Z c= dom (exp_R/(f1+#Z 2)) by A2,XBOOLE_1:18;
then A6:Z c= dom (exp_R(#)((f1+#Z 2)^)) by RFUNCT_1:31;
then Z c= dom exp_R /\ dom ((f1+#Z 2)^) by VALUED_1:def 4;then
A7:Z c= dom ((f1+#Z 2)^) by XBOOLE_1:18;
dom ((f1+ #Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A8:Z c= dom (f1+#Z 2) by A7;
(f1+#Z 2)^ is_differentiable_on Z by A1,A7,Th1;
then exp_R(#)((f1+#Z 2)^) is_differentiable_on Z by A3,A6,FDIFF_1:21;
then exp_R/(f1+#Z 2) is_differentiable_on Z by RFUNCT_1:31;
then f|Z is continuous by A1,A4,FDIFF_1:18,25;then
f|A is continuous by A1,FCONT_1:16;
then A9:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A10:for x st x in Z holds f.x=exp_R.x*arctan.x+exp_R.x/(1+x^2)
proof
let x;
assume
A11:x in Z;
then (exp_R(#)arctan+exp_R/(f1+#Z 2)).x
=(exp_R(#)arctan).x+(exp_R/(f1+#Z 2)).x by A1,VALUED_1:def 1
.=exp_R.x*arctan.x+(exp_R/(f1+#Z 2)).x by VALUED_1:5
.=exp_R.x*arctan.x+exp_R.x/(f1+#Z 2).x by A5,A11,RFUNCT_1:def 1
.=exp_R.x*arctan.x+exp_R.x/(f1.x+(( #Z 2).x)) by A8,A11,VALUED_1:def 1
.=exp_R.x*arctan.x+exp_R.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1
.=exp_R.x*arctan.x+exp_R.x/(f1.x+x^2) by FDIFF_7:1
.=exp_R.x*arctan.x+exp_R.x/(1+x^2) by A1,A11;
hence thesis by A1;
end;
A12:for x being Element of REAL
st x in dom((exp_R(#)arctan)`|Z) holds ((exp_R(#)arctan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((exp_R(#)arctan)`|Z);then
A13:x in Z by A4,FDIFF_1:def 7;then
((exp_R(#)arctan)`|Z).x=exp_R.x*arctan.x+exp_R.x/(1+x^2) by A1,SIN_COS9:123
.=f.x by A13,A10;
hence thesis;
end;
dom((exp_R(#)arctan)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((exp_R(#)arctan)`|Z)= f by A12,PARTFUN1:5;
hence thesis by A1,A9,INTEGRA5:13,SIN_COS9:123;
end;
::f.x=exp_R.x*arccot.x-exp_R.x/(1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f
& f=exp_R(#)arccot-exp_R/(f1+#Z 2) implies
integral(f,A)
=(exp_R(#)arccot).(upper_bound A)-(exp_R(#)arccot).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f
& f=exp_R(#)arccot-exp_R/(f1+#Z 2);
then A2:Z = dom (exp_R(#)arccot) /\ dom (exp_R/(f1+#Z 2)) by VALUED_1:12;
A3:exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
A4:exp_R(#)arccot is_differentiable_on Z by A1,SIN_COS9:124;
A5:Z c= dom (exp_R/(f1+#Z 2)) by A2,XBOOLE_1:18;
then A6:Z c= dom (exp_R(#)((f1+#Z 2)^)) by RFUNCT_1:31;
then Z c= dom exp_R /\ dom ((f1+#Z 2)^) by VALUED_1:def 4;then
A7:Z c= dom ((f1+#Z 2)^) by XBOOLE_1:18;
dom ((f1+ #Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A8:Z c= dom (f1+#Z 2) by A7;
(f1+#Z 2)^ is_differentiable_on Z by A1,A7,Th1;
then exp_R(#)((f1+#Z 2)^) is_differentiable_on Z by A3,A6,FDIFF_1:21;
then exp_R/(f1+#Z 2) is_differentiable_on Z by RFUNCT_1:31;
then f|Z is continuous by A1,A4,FDIFF_1:19,25;then
f|A is continuous by A1,FCONT_1:16;
then A9:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A10:for x st x in Z holds f.x=exp_R.x*arccot.x-exp_R.x/(1+x^2)
proof
let x;
assume
A11:x in Z;
then (exp_R(#)arccot-exp_R/(f1+#Z 2)).x
=(exp_R(#)arccot).x-(exp_R/(f1+#Z 2)).x by A1,VALUED_1:13
.=exp_R.x*arccot.x-(exp_R/(f1+#Z 2)).x by VALUED_1:5
.=exp_R.x*arccot.x-exp_R.x/(f1+#Z 2).x by A5,A11,RFUNCT_1:def 1
.=exp_R.x*arccot.x-exp_R.x/(f1.x+(( #Z 2).x)) by A8,A11,VALUED_1:def 1
.=exp_R.x*arccot.x-exp_R.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1
.=exp_R.x*arccot.x-exp_R.x/(f1.x+x^2) by FDIFF_7:1
.=exp_R.x*arccot.x-exp_R.x/(1+x^2) by A1,A11;
hence thesis by A1;
end;
A12:for x being Element of REAL
st x in dom((exp_R(#)arccot)`|Z) holds ((exp_R(#)arccot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((exp_R(#)arccot)`|Z);then
A13:x in Z by A4,FDIFF_1:def 7;then
((exp_R(#)arccot)`|Z).x=exp_R.x*arccot.x-exp_R.x/(1+x^2) by A1,SIN_COS9:124
.=f.x by A13,A10;
hence thesis;
end;
dom((exp_R(#)arccot)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((exp_R(#)arccot)`|Z)= f by A12,PARTFUN1:5;
hence thesis by A1,A9,INTEGRA5:13,SIN_COS9:124;
end;
::f.x=exp_R.(sin.x) * cos.x
theorem
A c= Z & Z = dom f & f=(exp_R*sin)(#)cos implies
integral(f,A)=(exp_R*sin).(upper_bound A)-(exp_R*sin).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom f & f=(exp_R*sin)(#)cos;
then Z = dom (exp_R*sin) /\ dom cos by VALUED_1:def 4;
then A2:Z c= dom (exp_R*sin) by XBOOLE_1:18;
then A3:exp_R*sin is_differentiable_on Z by FDIFF_7:37;
cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then f|Z is continuous by A1,A3,FDIFF_1:21,25;then
f|A is continuous by A1,FCONT_1:16;
then A4:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A5:for x st x in Z holds f.x=exp_R.(sin.x) * cos.x
proof
let x;
assume
A6:x in Z;
then ((exp_R*sin)(#)cos).x=(exp_R*sin).x*cos.x by A1,VALUED_1:def 4
.=exp_R.(sin.x) * cos.x by A2,A6,FUNCT_1:12;
hence thesis by A1;
end;
A7:for x being Element of REAL
st x in dom((exp_R*sin)`|Z) holds ((exp_R*sin)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((exp_R*sin)`|Z);then
A8: x in Z by A3,FDIFF_1:def 7; then
((exp_R*sin)`|Z).x=exp_R.(sin.x) * cos.x by A2,FDIFF_7:37
.=f.x by A5,A8;
hence thesis;
end;
dom((exp_R*sin)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then((exp_R*sin)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,A4,FDIFF_7:37,INTEGRA5:13;
end;
::f.x=exp_R.(cos.x) * sin.x
theorem
A c= Z & Z = dom f & f=(exp_R*cos)(#)sin implies
integral(f,A)=(-exp_R*cos).(upper_bound A)-(-exp_R*cos).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom f & f=(exp_R*cos)(#)sin;
then Z = dom (exp_R*cos) /\ dom sin by VALUED_1:def 4;
then A2:Z c= dom (exp_R*cos) by XBOOLE_1:18;
then A3:exp_R*cos is_differentiable_on Z by FDIFF_7:36;
sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then f|Z is continuous by A1,A3,FDIFF_1:21,25;then
f|A is continuous by A1,FCONT_1:16;
then A4:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A5:Z c= dom (-exp_R*cos) by A2,VALUED_1:8;
then A6:(-1)(#)(exp_R*cos) is_differentiable_on Z by A3,FDIFF_1:20;
A7:for x st x in Z holds ((-exp_R*cos)`|Z).x = exp_R.(cos.x) * sin.x
proof
let x;
assume
A8:x in Z;
A9: cos is_differentiable_in x by SIN_COS:63;
A10: exp_R is_differentiable_in cos.x by SIN_COS:65;
A11: exp_R*cos is_differentiable_in x by A3,A8,FDIFF_1:9;
((-exp_R*cos)`|Z).x=diff(-exp_R*cos,x) by A6,A8,FDIFF_1:def 7
.=(-1)*diff(exp_R*cos,x) by A11,FDIFF_1:15
.=(-1)*(diff(exp_R,cos.x)*diff(cos,x)) by A9,A10,FDIFF_2:13
.=(-1)*(diff(exp_R,cos.x)*(-sin.x )) by SIN_COS:63
.=(-1)*(exp_R.(cos.x)*(-sin.x )) by SIN_COS:65
.=exp_R.(cos.x) * sin.x;
hence thesis;
end;
A12:for x st x in Z holds f.x=exp_R.(cos.x) * sin.x
proof
let x;
assume
A13:x in Z;
then ((exp_R*cos)(#)sin).x=(exp_R*cos).x*sin.x by A1,VALUED_1:def 4
.=exp_R.(cos.x) * sin.x by A2,A13,FUNCT_1:12;
hence thesis by A1;
end;
A14:for x being Element of REAL
st x in dom((-exp_R*cos)`|Z) holds ((-exp_R*cos)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((-exp_R*cos)`|Z);then
A15: x in Z by A6,FDIFF_1:def 7; then
((-exp_R*cos)`|Z).x=exp_R.(cos.x) * sin.x by A7
.=f.x by A15,A12;
hence thesis;
end;
dom((-exp_R*cos)`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((-exp_R*cos)`|Z)= f by A14,PARTFUN1:5;
hence thesis by A1,A4,A3,A5,FDIFF_1:20,INTEGRA5:13;
end;
::f.x=cos.(ln.x)/x
theorem
A c= Z & (for x st x in Z holds x>0)
& Z = dom f & f=(cos*ln)(#)((id Z)^) implies
integral(f,A)=(sin*ln).(upper_bound A)-(sin*ln).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds x>0) & Z = dom f & f=(cos*ln)(#)((id Z)^);
then A2:Z = dom ((cos*ln)/(id Z)) by RFUNCT_1:31;
Z = dom (cos*ln) /\ dom ((id Z)^) by A1,VALUED_1:def 4;
then A3:Z c= dom (cos*ln) by XBOOLE_1:18;
for y being object st y in Z holds y in dom (sin*ln)
proof
let y be object;
assume y in Z;then
y in dom ln & ln.y in dom sin by A3,FUNCT_1:11,SIN_COS:24;
hence thesis by FUNCT_1:11;
end;
then A4:Z c= dom (sin*ln);
A5:cos*ln is_differentiable_on Z by A3,A1,FDIFF_7:33;
not 0 in Z by A1;
then (id Z)^ is_differentiable_on Z by FDIFF_5:4;
then f|Z is continuous by A1,A5,FDIFF_1:21,25;then
f|A is continuous by A1,FCONT_1:16;
then A6:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A7:sin*ln is_differentiable_on Z by A4,A1,FDIFF_7:32;
A8:for x st x in Z holds f.x=cos.(ln.x)/x
proof
let x;
assume
A9:x in Z;
((cos*ln)(#)((id Z)^)).x=((cos*ln)/(id Z)).x by RFUNCT_1:31
.=(cos*ln).x*((id Z).x)" by A2,A9,RFUNCT_1:def 1
.=(cos*ln).x/x by A9,FUNCT_1:18
.=cos.(ln.x)/x by A3,A9,FUNCT_1:12;
hence thesis by A1;
end;
A10:for x being Element of REAL st x in dom((sin*ln)`|Z)
holds ((sin*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((sin*ln)`|Z);then
A11: x in Z by A7,FDIFF_1:def 7; then
((sin*ln)`|Z).x=cos.(ln.x)/x by A4,A1,FDIFF_7:32
.=f.x by A11,A8;
hence thesis;
end;
dom((sin*ln)`|Z)=dom f by A1,A7,FDIFF_1:def 7;
then ((sin*ln)`|Z)= f by A10,PARTFUN1:5;
hence thesis by A6,A4,A1,FDIFF_7:32,INTEGRA5:13;
end;
Lm1: right_open_halfline 0 = {g where g is Real: 0<g} by XXREAL_1:230;
::f.x=sin.(ln.x)/x
theorem
A c= Z & (for x st x in Z holds x>0)
& Z = dom f & f=(sin*ln)(#)((id Z)^) implies
integral(f,A)=(-cos*ln).(upper_bound A)-(-cos*ln).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds x>0)
& Z = dom f & f=(sin*ln)(#)((id Z)^); then
A2:Z = dom ((sin*ln)/(id Z)) by RFUNCT_1:31;
Z = dom (sin*ln) /\ dom ((id Z)^) by A1,VALUED_1:def 4;
then A3:Z c= dom (sin*ln) by XBOOLE_1:18;
for y being object st y in Z holds y in dom (cos*ln)
proof
let y be object;
assume y in Z;then
y in dom ln & ln.y in dom cos by A3,FUNCT_1:11,SIN_COS:24;
hence thesis by FUNCT_1:11;
end;
then A4:Z c= dom (cos*ln);
A5:sin*ln is_differentiable_on Z by A3,A1,FDIFF_7:32;
not 0 in Z by A1;
then (id Z)^ is_differentiable_on Z by FDIFF_5:4;
then f|Z is continuous by A1,A5,FDIFF_1:21,25;then
f|A is continuous by A1,FCONT_1:16;
then A6:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A7:cos*ln is_differentiable_on Z by A4,A1,FDIFF_7:33;
A8:Z c= dom (-cos*ln) by A4,VALUED_1:8;
then A9:(-1)(#)(cos*ln) is_differentiable_on Z by A7,FDIFF_1:20;
A10:for x st x in Z holds ((-cos*ln)`|Z).x =sin.(ln.x)/x
proof
let x;
assume
A11:x in Z;then
x>0 by A1;then
A12:x in right_open_halfline(0) by Lm1;
A13:ln is_differentiable_in x by A11,A1,TAYLOR_1:18;
A14:cos is_differentiable_in ln.x by SIN_COS:63;
A15:cos*ln is_differentiable_in x by A7,A11,FDIFF_1:9;
((-cos*ln)`|Z).x=diff(-cos*ln,x) by A9,A11,FDIFF_1:def 7
.=(-1)*(diff(cos*ln,x)) by A15,FDIFF_1:15
.=(-1)*(diff(cos,ln.x)*diff(ln,x)) by A13,A14,FDIFF_2:13
.=(-1)*((-sin.(ln.x))*diff(ln,x)) by SIN_COS:63
.=(-1)*((-sin.(ln.x))*(1/x)) by A12,TAYLOR_1:18
.=sin.(ln.x)/x;
hence thesis;
end;
A16:for x st x in Z holds f.x=sin.(ln.x)/x
proof
let x;
assume
A17: x in Z;
((sin*ln)(#)((id Z)^)).x=((sin*ln)/(id Z)).x by RFUNCT_1:31
.=(sin*ln).x*((id Z).x)" by A2,A17,RFUNCT_1:def 1
.=(sin*ln).x/x by A17,FUNCT_1:18
.=sin.(ln.x)/x by A3,A17,FUNCT_1:12;
hence thesis by A1;
end;
A18:for x being Element of REAL st x in dom((-cos*ln)`|Z)
holds ((-cos*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((-cos*ln)`|Z);then
A19:x in Z by A9,FDIFF_1:def 7; then
((-cos*ln)`|Z).x=sin.(ln.x)/x by A10
.=f.x by A19,A16;
hence thesis;
end;
dom((-cos*ln)`|Z)=dom f by A1,A9,FDIFF_1:def 7;
then ((-cos*ln)`|Z)= f by A18,PARTFUN1:5;
hence thesis by A1,A6,A7,A8,FDIFF_1:20,INTEGRA5:13;
end;
::f.x=exp_R.x * cos.(exp_R.x)
theorem
A c= Z & Z = dom f & f=exp_R(#)(cos*exp_R) implies
integral(f,A)=(sin*exp_R).(upper_bound A)-(sin*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom f & f=exp_R(#)(cos*exp_R);
then Z = dom exp_R /\ dom (cos*exp_R) by VALUED_1:def 4;
then A2:Z c= dom exp_R & Z c= dom (cos*exp_R) by XBOOLE_1:18;
for y being object st y in Z holds y in dom (sin*exp_R)
proof
let y be object;
assume y in Z;then
y in dom exp_R & exp_R.y in dom sin by A2,SIN_COS:24,XREAL_0:def 1;
hence thesis by FUNCT_1:11;
end;
then A3:Z c= dom (sin*exp_R);
A4:cos*exp_R is_differentiable_on Z by A2,FDIFF_7:35;
exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then f|Z is continuous by A1,A4,FDIFF_1:21,25;then
f|A is continuous by A1,FCONT_1:16;
then A5:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A6:sin*exp_R is_differentiable_on Z by A3,FDIFF_7:34;
A7:for x st x in Z holds f.x=exp_R.x * cos.(exp_R.x)
proof
let x;
assume
A8:x in Z;
then (exp_R(#)(cos*exp_R)).x=exp_R.x*(cos*exp_R).x by A1,VALUED_1:def 4
.=exp_R.x*cos.(exp_R.x) by A2,A8,FUNCT_1:12;
hence thesis by A1;
end;
A9:for x being Element of REAL st x in dom((sin*exp_R)`|Z)
holds ((sin*exp_R)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom((sin*exp_R)`|Z);then
A10: x in Z by A6,FDIFF_1:def 7; then
((sin*exp_R)`|Z).x=exp_R.x * cos.(exp_R.x) by A3,FDIFF_7:34
.=f.x by A10,A7;
hence thesis;
end;
dom((sin*exp_R)`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((sin*exp_R)`|Z)= f by A9,PARTFUN1:5;
hence thesis by A1,A5,A3,FDIFF_7:34,INTEGRA5:13;
end;
::f.x = exp_R.x * sin.(exp_R.x)
theorem
A c= Z & Z = dom f & f=exp_R(#)(sin*exp_R) implies
integral(f,A)=(-cos*exp_R).(upper_bound A)-(-cos*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom f & f=exp_R(#)(sin*exp_R);
then Z = dom exp_R /\ dom (sin*exp_R) by VALUED_1:def 4;
then A2:Z c= dom exp_R & Z c= dom (sin*exp_R) by XBOOLE_1:18;
for y being object st y in Z holds y in dom (cos*exp_R)
proof
let y be object;
assume y in Z;then
y in dom exp_R & exp_R.y in dom cos by A2,SIN_COS:24,XREAL_0:def 1;
hence thesis by FUNCT_1:11;
end;
then A3:Z c= dom (cos*exp_R);
A4:sin*exp_R is_differentiable_on Z by A2,FDIFF_7:34;
exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then f|Z is continuous by A1,A4,FDIFF_1:21,25;then
f|A is continuous by A1,FCONT_1:16;
then A5:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A6:cos*exp_R is_differentiable_on Z by A3,FDIFF_7:35;
A7:Z c= dom (-cos*exp_R) by A3,VALUED_1:8;
then A8:(-1)(#)(cos*exp_R) is_differentiable_on Z by A6,FDIFF_1:20;
A9:for x st x in Z holds ((-cos*exp_R)`|Z).x = exp_R.x * sin.(exp_R.x)
proof
let x;
assume
A10:x in Z;
A11: exp_R is_differentiable_in x by SIN_COS:65;
A12: cos is_differentiable_in exp_R.x by SIN_COS:63;
A13: cos*exp_R is_differentiable_in x by A6,A10,FDIFF_1:9;
((-cos*exp_R)`|Z).x=diff(-cos*exp_R,x) by A8,A10,FDIFF_1:def 7
.=(-1)*(diff(cos*exp_R,x)) by A13,FDIFF_1:15
.=(-1)*(diff(cos,exp_R.x)*diff(exp_R,x))
by A11,A12,FDIFF_2:13
.=(-1)*((-sin.(exp_R.x))*diff(exp_R,x)) by SIN_COS:63
.=(-1)*((-sin.(exp_R.x))*exp_R.x) by SIN_COS:65
.=exp_R.x*sin.(exp_R.x);
hence thesis;
end;
A14:for x st x in Z holds f.x=exp_R.x * sin.(exp_R.x)
proof
let x;
assume
A15:x in Z;
then (exp_R(#)(sin*exp_R)).x=exp_R.x*(sin*exp_R).x by A1,VALUED_1:def 4
.=exp_R.x*sin.(exp_R.x) by A2,A15,FUNCT_1:12;
hence thesis by A1;
end;
A16:for x being Element of REAL
st x in dom((-cos*exp_R)`|Z) holds ((-cos*exp_R)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom((-cos*exp_R)`|Z);then
A17:x in Z by A8,FDIFF_1:def 7; then
((-cos*exp_R)`|Z).x=exp_R.x * sin.(exp_R.x) by A9
.=f.x by A17,A14;
hence thesis;
end;
dom((-cos*exp_R)`|Z)=dom f by A1,A8,FDIFF_1:def 7;
then ((-cos*exp_R)`|Z)= f by A16,PARTFUN1:5;
hence thesis by A1,A5,A6,A7,FDIFF_1:20,INTEGRA5:13;
end;
::f.x=arctan.(x/r)
theorem
A c= Z & Z c= dom (ln*(f1+f2))
& r <> 0 & (for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1 & f1.x=1)
& f2=( #Z 2)*g & Z = dom f & f=arctan*g
implies
integral(f,A)=((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2))).(upper_bound A)
-((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (ln*(f1+f2))
& r <> 0 & (for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1 & f1.x=1)
& f2=( #Z 2)*g & Z = dom f & f=arctan*g;
Z c= dom id Z /\ dom f by A1;
then A2:Z c= dom ((id Z)(#)(arctan*g)) by A1,VALUED_1:def 4;
Z c= dom ((r/2)(#)(ln*(f1+f2))) by A1,VALUED_1:def 5;
then Z c= dom ((id Z)(#)(arctan*g)) /\ dom ((r/2)(#)(ln*(f1+f2)))
by A2,XBOOLE_1:19;
then A3:Z c= dom ((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2))) by VALUED_1:12;
for x st x in Z holds g.x=(1/r)*x+0
proof
let x;
assume x in Z;
then g.x=x/r by A1;
hence thesis;
end; then
for x st x in Z holds g.x=(1/r)*x+0 & g.x > -1 & g.x < 1 by A1;
then f is_differentiable_on Z by A1,SIN_COS9:87;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A4:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A5:(for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1)
& (for x st x in Z holds f1.x=1)
&(for x st x in Z holds g.x=x/r) by A1; then
A6:(id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2)) is_differentiable_on Z
by A1,A3,SIN_COS9:109;
A7:for x st x in Z holds f.x=arctan.(x/r)
proof
let x;
assume
A8:x in Z;
then (arctan*g).x=arctan.(g.x) by A1,FUNCT_1:12
.=arctan.(x/r) by A1,A8;
hence thesis by A1;
end;
A9:for x being Element of REAL
st x in dom(((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2)))`|Z) holds
(((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2)))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2)))`|Z);
then
A10:x in Z by A6,FDIFF_1:def 7;then
(((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2)))`|Z).x=arctan.(x/r)
by A1,A3,A5,SIN_COS9:109
.=f.x by A7,A10;
hence thesis;
end;
dom(((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2)))`|Z)=dom f
by A1,A6,FDIFF_1:def 7;
then (((id Z)(#)(arctan*g)-(r/2)(#)(ln*(f1+f2)))`|Z) = f by A9,PARTFUN1:5;
hence thesis by A1,A4,A6,INTEGRA5:13;
end;
::f.x=arccot.(x/r)
theorem
A c= Z & Z c= dom (ln*(f1+f2))
& r <> 0 & (for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1 & f1.x=1)
& f2=( #Z 2)*g & Z = dom f & f=arccot*g implies
integral(f,A)=((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2))).(upper_bound A)
-((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (ln*(f1+f2))
& r <> 0 & (for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1 & f1.x=1)
& f2=( #Z 2)*g & Z = dom f & f=(arccot)*g;
Z c= dom id Z /\ dom f by A1;
then A2:Z c= dom ((id Z)(#)((arccot)*g)) by A1,VALUED_1:def 4;
Z c= dom ((r/2)(#)(ln*(f1+f2))) by A1,VALUED_1:def 5;
then Z c= dom ((id Z)(#)((arccot)*g)) /\ dom ((r/2)(#)(ln*(f1+f2)))
by A2,XBOOLE_1:19;
then
A3:Z c= dom ((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2))) by VALUED_1:def 1;
A4:for x st x in Z holds g.x=x/r & g.x > -1 & g.x < 1 by A1;
for x st x in Z holds g.x=(1/r)*x+0
proof
let x;
assume x in Z;
then g.x=x/r by A1;
hence thesis;
end;
then
for x st x in Z holds g.x=(1/r)*x+0 & g.x > -1 & g.x < 1 by A1;
then f is_differentiable_on Z by A1,SIN_COS9:88;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A5:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A6:(for x st x in Z holds f1.x=1)
& (for x st x in Z holds g.x=x/r) by A1; then
A7:(id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2)) is_differentiable_on Z
by A1,A3,A4,SIN_COS9:110;
A8:for x st x in Z holds f.x=arccot.(x/r)
proof
let x;
assume
A9:x in Z;
then (arccot*g).x=arccot.(g.x) by A1,FUNCT_1:12
.=arccot.(x/r) by A1,A9;
hence thesis by A1;
end;
A10:for x being Element of REAL
st x in dom(((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2)))`|Z) holds
(((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2)))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2)))`|Z); then
A11:x in Z by A7,FDIFF_1:def 7;then
(((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2)))`|Z).x=arccot.(x/r)
by A1,A3,A4,A6,SIN_COS9:110
.=f.x by A8,A11;
hence thesis;
end;
dom(((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2)))`|Z)=dom f
by A1,A7,FDIFF_1:def 7;
then (((id Z)(#)((arccot)*g)+(r/2)(#)(ln*(f1+f2)))`|Z) = f by A10,PARTFUN1:5;
hence thesis by A1,A5,A7,INTEGRA5:13;
end;
::f.x=arctan.(x/r)+x/(r*(1+(x/r)^2))
theorem
A c= Z & f=arctan*f1+(id Z)/(r(#)(g+f1^2))
& (for x st x in Z holds g.x=1 & f1.x=x/r & f1.x > -1 & f1.x < 1)
& Z = dom f & f|A is continuous
implies integral(f,A)=((id Z)(#)(arctan*f1)).(upper_bound A)
-((id Z)(#)(arctan*f1)).(lower_bound A)
proof
assume
A1:A c= Z & f=arctan*f1+(id Z)/(r(#)(g+f1^2))
& (for x st x in Z holds g.x=1 & f1.x=x/r & f1.x > -1 & f1.x < 1)
& Z = dom f & f|A is continuous;
then
Z = dom (arctan*f1) /\ dom ((id Z)/(r(#)(g+f1^2))) by VALUED_1:def 1;
then
A2:Z c= dom (arctan*f1) & Z c= dom ((id Z)/(r(#)(g+f1^2))) by XBOOLE_1:18;
Z c= dom id Z /\ dom (arctan*f1) by A2,XBOOLE_1:19;
then A3:Z c= dom ((id Z)(#)(arctan*f1)) by VALUED_1:def 4;
Z c= dom (id Z) /\ (dom (r(#)(g+f1^2)) \ (r(#)(g+f1^2))"{0})
by A2,RFUNCT_1:def 1;
then Z c= dom (r(#)(g+f1^2)) \ (r(#)(g+f1^2))"{0} by XBOOLE_1:18;
then A4:Z c= dom ((r(#)(g+f1^2))^) by RFUNCT_1:def 2;
dom ((r(#)(g+f1^2))^) c= dom (r(#)(g+f1^2)) by RFUNCT_1:1; then
Z c= dom (r(#)(g+f1^2)) by A4;
then A5:Z c= dom (g+f1^2) by VALUED_1:def 5;
A6:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A7:for x st x in Z holds f1.x=x/r & f1.x > -1 & f1.x < 1 by A1; then
A8:(id Z)(#)(arctan*f1) is_differentiable_on Z by A3,SIN_COS9:105;
A9:for x st x in Z holds f.x=arctan.(x/r)+x/(r*(1+(x/r)^2))
proof
let x;
assume
A10:x in Z;
then (arctan*f1+(id Z)/(r(#)(g+f1^2))).x
=(arctan*f1).x+((id Z)/(r(#)(g+f1^2))).x by A1,VALUED_1:def 1
.=arctan.(f1.x)+((id Z)/(r(#)(g+f1^2))).x by A2,A10,FUNCT_1:12
.=arctan.(f1.x)+(id Z).x/(r(#)(g+f1^2)).x by A2,A10,RFUNCT_1:def 1
.=arctan.(f1.x)+x/(r(#)(g+f1^2)).x by A10,FUNCT_1:18
.=arctan.(f1.x)+x/(r*(g+f1^2).x) by VALUED_1:6
.=arctan.(f1.x)+x/(r*(g.x+(f1^2).x)) by A5,A10,VALUED_1:def 1
.=arctan.(f1.x)+x/(r*(g.x+((f1.x)^2))) by VALUED_1:11
.=arctan.(x/r)+x/(r*(g.x+(f1.x)^2)) by A1,A10
.=arctan.(x/r)+x/(r*(1+(f1.x)^2)) by A1,A10
.=arctan.(x/r)+x/(r*(1+(x/r)^2)) by A1,A10;
hence thesis by A1;
end;
A11:for x being Element of REAL st x in dom(((id Z)(#)(arctan*f1))`|Z) holds
(((id Z)(#)(arctan*f1))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)((arctan)*f1))`|Z);then
A12: x in Z by A8,FDIFF_1:def 7;then
(((id Z)(#)((arctan)*f1))`|Z).x=arctan.(x/r)+x/(r*(1+(x/r)^2))
by A3,A7,SIN_COS9:105
.=f.x by A9,A12;
hence thesis;
end;
dom(((id Z)(#)((arctan)*f1))`|Z) = dom f by A1,A8,FDIFF_1:def 7;
then (((id Z)(#)((arctan)*f1))`|Z) = f by A11,PARTFUN1:5;
hence thesis by A1,A6,A8,INTEGRA5:13;
end;
::f.x=arccot.(x/r)-x/(r*(1+(x/r)^2))
theorem
A c= Z & f=arccot*f1-(id Z)/(r(#)(g+f1^2))
& (for x st x in Z holds g.x=1 & f1.x=x/r & f1.x > -1 & f1.x < 1)
& Z = dom f & f|A is continuous
implies integral(f,A)=((id Z)(#)((arccot)*f1)).(upper_bound A)
-((id Z)(#)((arccot)*f1)).(lower_bound A)
proof
assume
A1:A c= Z & f=arccot*f1-(id Z)/(r(#)(g+f1^2))
& (for x st x in Z holds g.x=1 & f1.x=x/r & f1.x > -1 & f1.x < 1)
& Z = dom f & f|A is continuous;
then Z = dom (arccot*f1) /\ dom ((id Z)/(r(#)(g+f1^2))) by VALUED_1:12;
then
A2:Z c= dom (arccot*f1) & Z c= dom ((id Z)/(r(#)(g+f1^2))) by XBOOLE_1:18;
Z c= dom id Z /\ dom (arccot*f1) by A2,XBOOLE_1:19;
then A3:Z c= dom ((id Z)(#)(arccot*f1)) by VALUED_1:def 4;
Z c= dom (id Z) /\ (dom (r(#)(g+f1^2)) \ (r(#)(g+f1^2))"{0})
by A2,RFUNCT_1:def 1;
then Z c= dom (r(#)(g+f1^2)) \ (r(#)(g+f1^2))"{0} by XBOOLE_1:18;
then A4:Z c= dom ((r(#)(g+f1^2))^) by RFUNCT_1:def 2;
dom ((r(#)(g+f1^2))^) c= dom (r(#)(g+f1^2)) by RFUNCT_1:1; then
Z c= dom (r(#)(g+f1^2)) by A4;
then A5:Z c= dom (g+f1^2) by VALUED_1:def 5;
A6:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A7:for x st x in Z holds f1.x=x/r & f1.x > -1 & f1.x < 1 by A1; then
A8:(id Z)(#)((arccot)*f1) is_differentiable_on Z by A3,SIN_COS9:106;
A9:for x st x in Z holds f.x=arccot.(x/r)-x/(r*(1+(x/r)^2))
proof
let x;
assume
A10:x in Z;
then (arccot*f1-(id Z)/(r(#)(g+f1^2))).x
=(arccot*f1).x-((id Z)/(r(#)(g+f1^2))).x by A1,VALUED_1:13
.=arccot.(f1.x)-((id Z)/(r(#)(g+f1^2))).x by A2,A10,FUNCT_1:12
.=arccot.(f1.x)-(id Z).x/(r(#)(g+f1^2)).x by A2,A10,RFUNCT_1:def 1
.=arccot.(f1.x)-x/(r(#)(g+f1^2)).x by A10,FUNCT_1:18
.=arccot.(f1.x)-x/(r*(g+f1^2).x) by VALUED_1:6
.=arccot.(f1.x)-x/(r*(g.x+(f1^2).x)) by A5,A10,VALUED_1:def 1
.=arccot.(f1.x)-x/(r*(g.x+((f1.x)^2))) by VALUED_1:11
.=arccot.(x/r)-x/(r*(g.x+(f1.x)^2)) by A1,A10
.=arccot.(x/r)-x/(r*(1+(f1.x)^2)) by A1,A10
.=arccot.(x/r)-x/(r*(1+(x/r)^2)) by A1,A10;
hence thesis by A1;
end;
A11:for x being Element of REAL st x in dom(((id Z)(#)((arccot)*f1))`|Z) holds
(((id Z)(#)((arccot)*f1))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)((arccot)*f1))`|Z);then
A12: x in Z by A8,FDIFF_1:def 7;then
(((id Z)(#)((arccot)*f1))`|Z).x=arccot.(x/r)-x/(r*(1+(x/r)^2))
by A3,A7,SIN_COS9:106
.=f.x by A9,A12;
hence thesis;
end;
dom (((id Z)(#)((arccot)*f1))`|Z) = dom f by A1,A8,FDIFF_1:def 7;
then (((id Z)(#)((arccot)*f1))`|Z) = f by A11,PARTFUN1:5;
hence thesis by A1,A6,A8,INTEGRA5:13;
end;
::f.x=n*(arcsin.x) #Z (n-1) / sqrt(1-x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f1.x=1)
& Z = dom f & Z c= dom (( #Z n)*arcsin) & 1<n &
f=n(#)(( #Z (n-1))*arcsin)/(( #R (1/2))*(f1-#Z 2))
implies integral(f,A) = (( #Z n)*arcsin).(upper_bound A)
-(( #Z n)*arcsin).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f1.x=1)
& Z = dom f & Z c= dom (( #Z n)*arcsin) & 1<n &
f=n(#)(( #Z (n-1))*arcsin)/(( #R (1/2))*(f1-#Z 2));
then Z = dom (n(#)(( #Z (n-1))*(arcsin))) /\
(dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0})
by RFUNCT_1:def 1;
then A2:Z c= dom (n(#)(( #Z (n-1))*arcsin)) &
Z c= dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0}
by XBOOLE_1:18;
then A3:Z c= dom (( #Z (n-1))*arcsin) by VALUED_1:def 5;
A4:Z c= dom ((( #R (1/2))*(f1-#Z 2))^) by A2,RFUNCT_1:def 2;
dom ((( #R (1/2))*(f1-#Z 2))^) c= dom (( #R (1/2))*(f1-#Z 2))
by RFUNCT_1:1; then
A5:Z c= dom (( #R (1/2))*(f1-#Z 2)) by A4;
for x st x in Z holds ( #Z (n-1))*arcsin is_differentiable_in x
proof
let x;
assume x in Z; then
A6: arcsin is_differentiable_in x by A1,FDIFF_1:9,SIN_COS6:83;
consider m being Nat such that
A7: n = m + 1 by A1,NAT_1:6;
thus thesis by A6,A7,TAYLOR_1:3;
end;
then ( #Z (n-1))*arcsin is_differentiable_on Z by A3,FDIFF_1:9;
then A8:n(#)(( #Z (n-1))*arcsin) is_differentiable_on Z by A2,FDIFF_1:20;
set f2=#Z 2;
for x st x in Z holds (f1-#Z 2).x >0
proof
let x;
assume
A9:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A10:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f1-f2) by A5,FUNCT_1:11;
then (f1-f2).x = f1.x - f2.x by A9,VALUED_1:13
.=f1.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f1.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f1.x - (x*(x #Z 1)) by PREPOWER:35
.=f1.x - x*x by PREPOWER:35
.=1 - x*x by A1,A9;
hence thesis by A10;
end;
then for x st x in Z holds f1.x=1 & (f1-#Z 2).x >0 by A1;
then A11:(( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z by A5,FDIFF_7:22;
x in Z implies (( #R (1/2))*(f1-#Z 2)).x<>0 by A4,RFUNCT_1:3;
then f is_differentiable_on Z by A1,A8,A11,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A12:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A13:( #Z n)*arcsin is_differentiable_on Z by A1,FDIFF_7:10;
A14:for x st x in Z holds f.x=n*(arcsin.x) #Z (n-1) / sqrt(1-x^2)
proof
let x;
assume
A15:x in Z;
then
A16:x in dom (f1-#Z 2) & (f1-#Z 2).x in dom ( #R (1/2)) by A5,FUNCT_1:11;
then A17:(f1-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A15,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A18:0 < (1+x)*(1-x) by XREAL_1:129;
(n(#)(( #Z (n-1))*arcsin)/(( #R (1/2))*(f1-#Z 2))).x
=(n(#)(( #Z (n-1))*arcsin)).x/(( #R (1/2))*(f1-#Z 2)).x
by A1,A15,RFUNCT_1:def 1
.=n*(( #Z (n-1))*arcsin).x/(( #R (1/2))*(f1-#Z 2)).x by VALUED_1:6
.=n*(( #Z (n-1)).(arcsin.x))/(( #R (1/2))*(f1-#Z 2)).x
by A3,A15,FUNCT_1:12
.=n*(arcsin.x) #Z (n-1) / (( #R (1/2))*(f1-#Z 2)).x by TAYLOR_1:def 1
.=n*(arcsin.x) #Z (n-1) / (( #R (1/2)).((f1-#Z 2).x)) by A5,A15,FUNCT_1:12
.=n*(arcsin.x) #Z (n-1) / (((f1-#Z 2).x) #R (1/2)) by A17,TAYLOR_1:def 4
.=n*(arcsin.x) #Z (n-1) / ((f1.x-(( #Z 2).x)) #R (1/2))
by A16,VALUED_1:13
.=n*(arcsin.x) #Z (n-1) / ((f1.x-(x #Z 2)) #R (1/2)) by TAYLOR_1:def 1
.=n*(arcsin.x) #Z (n-1) / ((f1.x-x^2) #R (1/2)) by FDIFF_7:1
.=n*(arcsin.x) #Z (n-1) / ((1-x^2) #R (1/2)) by A1,A15
.=n*(arcsin.x) #Z (n-1) / sqrt(1-x^2) by A18,FDIFF_7:2;
hence thesis by A1;
end;
A19:for x being Element of REAL st x in dom ((( #Z n)*(arcsin))`|Z) holds
((( #Z n)*(arcsin))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((( #Z n)*(arcsin))`|Z);then
A20:x in Z by A13,FDIFF_1:def 7; then
((( #Z n)*(arcsin))`|Z).x=n*(arcsin.x) #Z (n-1) / sqrt(1-x^2)
by A1,FDIFF_7:10
.=f.x by A14,A20;
hence thesis;
end;
dom ((( #Z n)*(arcsin))`|Z)=dom f by A1,A13,FDIFF_1:def 7;
then ((( #Z n)*(arcsin))`|Z)= f by A19,PARTFUN1:5;
hence thesis by A1,A12,FDIFF_7:10,INTEGRA5:13;
end;
::f.x=n*(arccos.x) #Z (n-1) / sqrt(1-x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f1.x=1)
& Z c= dom (( #Z n)*(arccos)) & Z = dom f & 1<n &
f=n(#)(( #Z (n-1))*arccos)/(( #R (1/2))*(f1-#Z 2))
implies integral(f,A) = (-( #Z n)*(arccos)).(upper_bound A)
- (-( #Z n)*(arccos)).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f1.x=1)
& Z c= dom (( #Z n)*(arccos)) & Z = dom f & 1<n &
f=n(#)(( #Z (n-1))*arccos)/(( #R (1/2))*(f1-#Z 2));
then Z = dom (n(#)(( #Z (n-1))*(arccos))) /\
(dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0})
by RFUNCT_1:def 1;
then A2:Z c= dom (n(#)(( #Z (n-1))*(arccos))) &
Z c= dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0}
by XBOOLE_1:18;
then A3:Z c= dom (( #Z (n-1))*(arccos)) by VALUED_1:def 5;
A4:Z c= dom ((( #R (1/2))*(f1-#Z 2))^) by A2,RFUNCT_1:def 2;
dom ((( #R (1/2))*(f1-#Z 2))^) c= dom (( #R (1/2))*(f1-#Z 2))
by RFUNCT_1:1; then
A5:Z c= dom (( #R (1/2))*(f1-#Z 2)) by A4;
for x st x in Z holds ( #Z (n-1))*(arccos) is_differentiable_in x
proof
let x;
assume x in Z; then
A6: arccos is_differentiable_in x by A1,FDIFF_1:9,SIN_COS6:106;
consider m being Nat such that
A7: n = m + 1 by A1,NAT_1:6;
thus thesis by A6,A7,TAYLOR_1:3;
end;
then ( #Z (n-1))*(arccos) is_differentiable_on Z by A3,FDIFF_1:9;
then
A8:n(#)(( #Z (n-1))*(arccos)) is_differentiable_on Z by A2,FDIFF_1:20;
set f2=#Z 2;
for x st x in Z holds (f1-#Z 2).x >0
proof
let x;
assume
A9:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A10:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f1-f2) by A5,FUNCT_1:11;
then (f1-f2).x = f1.x - f2.x by A9,VALUED_1:13
.=f1.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f1.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f1.x - (x*(x #Z 1)) by PREPOWER:35
.=f1.x - x*x by PREPOWER:35
.=1 - x*x by A1,A9;
hence thesis by A10;
end;
then for x st x in Z holds f1.x=1 & (f1-#Z 2).x >0 by A1;
then A11:(( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z by A5,FDIFF_7:22;
x in Z implies (( #R (1/2))*(f1-#Z 2)).x<>0 by A4,RFUNCT_1:3;
then f is_differentiable_on Z by A1,A8,A11,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A12:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A13:( #Z n)*arccos is_differentiable_on Z by A1,FDIFF_7:11;
A14:Z c= dom (-( #Z n)*arccos) by A1,VALUED_1:8;
then
A15:(-1)(#)(( #Z n)*arccos) is_differentiable_on Z by A13,FDIFF_1:20;
A16:for x st x in Z holds f.x=n*(arccos.x) #Z (n-1) / sqrt(1-x^2)
proof
let x;
assume
A17:x in Z;
then
A18:x in dom (f1-#Z 2) & (f1-#Z 2).x in dom ( #R (1/2)) by A5,FUNCT_1:11;
then A19:(f1-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A17,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A20:0 < (1+x)*(1-x) by XREAL_1:129;
(n(#)(( #Z (n-1))*arccos)/(( #R (1/2))*(f1-#Z 2))).x
=(n(#)(( #Z (n-1))*arccos)).x/(( #R (1/2))*(f1-#Z 2)).x
by A1,A17,RFUNCT_1:def 1
.=n*(( #Z (n-1))*arccos).x/(( #R (1/2))*(f1-#Z 2)).x by VALUED_1:6
.=n*(( #Z (n-1)).(arccos.x))/(( #R (1/2))*(f1-#Z 2)).x
by A3,A17,FUNCT_1:12
.=n*(arccos.x) #Z (n-1) / (( #R (1/2))*(f1-#Z 2)).x by TAYLOR_1:def 1
.=n*(arccos.x) #Z (n-1) / (( #R (1/2)).((f1-#Z 2).x))
by A5,A17,FUNCT_1:12
.=n*(arccos.x) #Z (n-1) / (((f1-#Z 2).x) #R (1/2)) by A19,TAYLOR_1:def 4
.=n*(arccos.x) #Z (n-1) / ((f1.x-(( #Z 2).x)) #R (1/2))
by A18,VALUED_1:13
.=n*(arccos.x) #Z (n-1) / ((f1.x-(x #Z 2)) #R (1/2)) by TAYLOR_1:def 1
.=n*(arccos.x) #Z (n-1) / ((f1.x-x^2) #R (1/2)) by FDIFF_7:1
.=n*(arccos.x) #Z (n-1) / ((1-x^2) #R (1/2)) by A1,A17
.=n*(arccos.x) #Z (n-1) / sqrt(1-x^2) by A20,FDIFF_7:2;
hence thesis by A1;
end;
A21:for x st x in Z holds ((-( #Z n)*(arccos))`|Z).x
=n*(arccos.x) #Z (n-1) / sqrt(1-x^2)
proof
let x;
assume
A22:x in Z;then
A23:-1 < x & x < 1 by A1,XXREAL_1:4;
A24:arccos is_differentiable_in x by A1,A22,FDIFF_1:9,SIN_COS6:106;
A25:( #Z n)*(arccos) is_differentiable_in x by A13,A22,FDIFF_1:9;
((-( #Z n)*(arccos))`|Z).x=diff(-( #Z n)*(arccos),x) by A15,A22,FDIFF_1:def 7
.=(-1)*diff(( #Z n)*(arccos),x) by A25,FDIFF_1:15
.=(-1)*((n*((arccos.x) #Z (n-1)))
* diff(arccos,x)) by A24,TAYLOR_1:3
.=(-1)*((n*((arccos.x) #Z (n-1)))
*(-(1 / sqrt(1-x^2)))) by A23,SIN_COS6:106
.=n*(arccos.x) #Z (n-1) / sqrt(1-x^2);
hence thesis;
end;
A26:for x being Element of REAL st x in dom ((-( #Z n)*(arccos))`|Z) holds
((-( #Z n)*(arccos))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-( #Z n)*(arccos))`|Z);then
A27:x in Z by A15,FDIFF_1:def 7; then
((-( #Z n)*(arccos))`|Z).x=n*(arccos.x) #Z (n-1) / sqrt(1-x^2) by A21
.=f.x by A16,A27;
hence thesis;
end;
dom ((-( #Z n)*(arccos))`|Z)=dom f by A1,A15,FDIFF_1:def 7;
then ((-( #Z n)*(arccos))`|Z)= f by A26,PARTFUN1:5;
hence thesis by A1,A12,A13,A14,FDIFF_1:20,INTEGRA5:13;
end;
::f.x=arcsin.x+x/sqrt(1-x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1)
& Z c= ]. -1,1 .[ & Z = dom f & f=arcsin+(id Z)/(( #R (1/2))*(f1-#Z 2))
implies
integral(f,A)
=((id Z)(#)(arcsin)).(upper_bound A)-((id Z)(#)(arcsin)).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f
& f=arcsin+(id Z)/(( #R (1/2))*(f1-#Z 2));
then
Z = dom arcsin /\ dom ((id Z)/(( #R (1/2))*(f1-#Z 2))) by VALUED_1:def 1;
then A2:Z c= dom arcsin & Z c= dom ((id Z)/(( #R (1/2))*(f1-#Z 2)))
by XBOOLE_1:18;
A3:Z = dom id Z;
Z c= dom id Z /\ dom arcsin by A2,XBOOLE_1:19;
then A4:Z c= dom ((id Z)(#)(arcsin)) by VALUED_1:def 4;
A5:arcsin is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:83;
for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;then
A6:id Z is_differentiable_on Z by A3,FDIFF_1:23;
Z c= dom id Z /\ (dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0})
by A2,RFUNCT_1:def 1;
then Z c= dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0}
by XBOOLE_1:18;
then A7:Z c= dom ((( #R (1/2))*(f1-#Z 2))^) by RFUNCT_1:def 2;
dom ((( #R (1/2))*(f1-#Z 2))^) c= dom (( #R (1/2))*(f1-#Z 2))
by RFUNCT_1:1; then
A8:Z c= dom (( #R (1/2))*(f1-#Z 2)) by A7;
set f2=#Z 2;
for x st x in Z holds (f1-#Z 2).x >0
proof
let x;
assume
A9:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A10:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f1-f2) by A8,FUNCT_1:11;
then (f1-f2).x = f1.x - f2.x by A9,VALUED_1:13
.=f1.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f1.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f1.x - (x*(x #Z 1)) by PREPOWER:35
.=f1.x - x*x by PREPOWER:35
.=1 - x*x by A1,A9;
hence thesis by A10;
end;
then for x st x in Z holds f1.x=1 & (f1-#Z 2).x >0 by A1;
then A11:(( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z by A8,FDIFF_7:22;
x in Z implies (( #R (1/2))*(f1-#Z 2)).x<>0 by A7,RFUNCT_1:3;
then (id Z)/(( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z
by A6,A11,FDIFF_2:21;
then f|Z is continuous by A1,A5,FDIFF_1:18,25;then
f|A is continuous by A1,FCONT_1:16;
then A12:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A13:(id Z)(#)(arcsin) is_differentiable_on Z by A1,A4,FDIFF_7:16;
A14:for x st x in Z holds f.x=arcsin.x+x/sqrt(1-x^2)
proof
let x;
assume
A15:x in Z;
then
A16:x in dom (f1-#Z 2) & (f1-#Z 2).x in dom ( #R (1/2)) by A8,FUNCT_1:11;
then A17:(f1-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A15,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A18:0 < (1+x)*(1-x) by XREAL_1:129;
(arcsin+(id Z)/(( #R (1/2))*(f1-#Z 2))).x
=arcsin.x+((id Z)/(( #R (1/2))*(f1-#Z 2))).x by A1,A15,VALUED_1:def 1
.=arcsin.x+(id Z).x/(( #R (1/2))*(f1-#Z 2)).x by A2,A15,RFUNCT_1:def 1
.=arcsin.x+x/(( #R (1/2))*(f1-#Z 2)).x by A15,FUNCT_1:18
.=arcsin.x+x/(( #R (1/2)).((f1-#Z 2).x)) by A8,A15,FUNCT_1:12
.=arcsin.x+x/(((f1-#Z 2).x) #R (1/2)) by A17,TAYLOR_1:def 4
.=arcsin.x+x/((f1.x-(( #Z 2).x)) #R (1/2)) by A16,VALUED_1:13
.=arcsin.x+x/((f1.x-(x #Z 2)) #R (1/2)) by TAYLOR_1:def 1
.=arcsin.x+x/((f1.x-x^2) #R (1/2)) by FDIFF_7:1
.=arcsin.x+x/((1-x^2) #R (1/2)) by A1,A15
.=arcsin.x+x/sqrt(1-x^2) by A18,FDIFF_7:2;
hence thesis by A1;
end;
A19:for x being Element of REAL st x in dom (((id Z)(#)(arcsin))`|Z) holds
(((id Z)(#)(arcsin))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)(arcsin))`|Z);then
A20:x in Z by A13,FDIFF_1:def 7; then
(((id Z)(#)(arcsin))`|Z).x=arcsin.x+x/sqrt(1-x^2) by A1,A4,FDIFF_7:16
.=f.x by A14,A20;
hence thesis;
end;
dom(((id Z)(#)(arcsin))`|Z)=dom f by A1,A13,FDIFF_1:def 7;
then(((id Z)(#)(arcsin))`|Z)= f by A19,PARTFUN1:5;
hence thesis by A1,A12,A4,FDIFF_7:16,INTEGRA5:13;
end;
::f.x=arccos.x-x/sqrt(1-x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1)
& Z c= ]. -1,1 .[ & Z = dom f & f=arccos-(id Z)/(( #R (1/2))*(f1-#Z 2))
implies
integral(f,A)
=((id Z)(#)(arccos)).(upper_bound A)-((id Z)(#)(arccos)).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z = dom f
& f=arccos-(id Z)/(( #R (1/2))*(f1-#Z 2));
then
Z = dom arccos /\ dom ((id Z)/(( #R (1/2))*(f1-#Z 2))) by VALUED_1:12;
then A2:Z c= dom arccos & Z c= dom ((id Z)/(( #R (1/2))*(f1-#Z 2)))
by XBOOLE_1:18;
A3:Z = dom id Z;
Z c= dom id Z /\ dom arccos by A2,XBOOLE_1:19;
then A4:Z c= dom ((id Z)(#)(arccos)) by VALUED_1:def 4;
A5:arccos is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:106;
for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;then
A6:id Z is_differentiable_on Z by A3,FDIFF_1:23;
Z c= dom id Z /\ (dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0})
by A2,RFUNCT_1:def 1;
then Z c= dom (( #R (1/2))*(f1-#Z 2)) \ (( #R (1/2))*(f1-#Z 2))"{0}
by XBOOLE_1:18;
then A7:Z c= dom ((( #R (1/2))*(f1-#Z 2))^) by RFUNCT_1:def 2;
dom ((( #R (1/2))*(f1-#Z 2))^) c= dom (( #R (1/2))*(f1-#Z 2))
by RFUNCT_1:1; then
A8:Z c= dom (( #R (1/2))*(f1-#Z 2)) by A7;
set f2=#Z 2;
for x st x in Z holds (f1-#Z 2).x >0
proof
let x;
assume
A9:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A10:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f1-f2) by A8,FUNCT_1:11;
then (f1-f2).x = f1.x - f2.x by A9,VALUED_1:13
.=f1.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f1.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f1.x - (x*(x #Z 1)) by PREPOWER:35
.=f1.x - x*x by PREPOWER:35
.=1 - x*x by A1,A9;
hence thesis by A10;
end;
then for x st x in Z holds f1.x=1 & (f1-#Z 2).x >0 by A1;
then A11:(( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z by A8,FDIFF_7:22;
x in Z implies (( #R (1/2))*(f1-#Z 2)).x<>0 by A7,RFUNCT_1:3;
then (id Z)/(( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z
by A6,A11,FDIFF_2:21;
then f|Z is continuous by A1,A5,FDIFF_1:19,25;then
f|A is continuous by A1,FCONT_1:16;
then A12:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A13:(id Z)(#)(arccos) is_differentiable_on Z by A1,A4,FDIFF_7:17;
A14:for x st x in Z holds f.x=arccos.x-x/sqrt(1-x^2)
proof
let x;
assume
A15:x in Z;
then
A16:x in dom (f1-#Z 2) & (f1-#Z 2).x in dom ( #R (1/2)) by A8,FUNCT_1:11;
then A17:(f1-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A15,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A18:0 < (1+x)*(1-x) by XREAL_1:129;
(arccos-(id Z)/(( #R (1/2))*(f1-#Z 2))).x
=arccos.x-((id Z)/(( #R (1/2))*(f1-#Z 2))).x by A1,A15,VALUED_1:13
.=arccos.x-(id Z).x/(( #R (1/2))*(f1-#Z 2)).x by A2,A15,RFUNCT_1:def 1
.=arccos.x-x/(( #R (1/2))*(f1-#Z 2)).x by A15,FUNCT_1:18
.=arccos.x-x/(( #R (1/2)).((f1-#Z 2).x)) by A8,A15,FUNCT_1:12
.=arccos.x-x/(((f1-#Z 2).x) #R (1/2)) by A17,TAYLOR_1:def 4
.=arccos.x-x/((f1.x-(( #Z 2).x)) #R (1/2)) by A16,VALUED_1:13
.=arccos.x-x/((f1.x-(x #Z 2)) #R (1/2)) by TAYLOR_1:def 1
.=arccos.x-x/((f1.x-x^2) #R (1/2)) by FDIFF_7:1
.=arccos.x-x/((1-x^2) #R (1/2)) by A1,A15
.=arccos.x-x/sqrt(1-x^2) by A18,FDIFF_7:2;
hence thesis by A1;
end;
A19:for x being Element of REAL st x in dom (((id Z)(#)(arccos))`|Z) holds
(((id Z)(#)(arccos))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)(arccos))`|Z);then
A20:x in Z by A13,FDIFF_1:def 7; then
(((id Z)(#)(arccos))`|Z).x=arccos.x-x/sqrt(1-x^2) by A1,A4,FDIFF_7:17
.=f.x by A14,A20;
hence thesis;
end;
dom(((id Z)(#)(arccos))`|Z)=dom f by A1,A13,FDIFF_1:def 7;
then(((id Z)(#)(arccos))`|Z)= f by A19,PARTFUN1:5;
hence thesis by A1,A12,A4,FDIFF_7:17,INTEGRA5:13;
end;
::f.x=a*arcsin.x+(a*x+b)/sqrt(1-x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ &
(for x st x in Z holds f1.x=a*x+b & f2.x=1) & Z = dom f
& f=a(#)arcsin+f1/(( #R (1/2))*(f2-#Z 2)) implies
integral(f,A)=(f1(#)(arcsin)).(upper_bound A)-(f1(#)(arcsin)).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ &
(for x st x in Z holds f1.x=a*x+b & f2.x=1) & Z = dom f
& f=a(#)arcsin+f1/(( #R (1/2))*(f2-#Z 2));
then Z = dom (a(#)arcsin) /\ dom (f1/(( #R (1/2))*(f2-#Z 2)))
by VALUED_1:def 1;
then A2:Z c= dom (a(#)arcsin) & Z c= dom (f1/(( #R (1/2))*(f2-#Z 2)))
by XBOOLE_1:18;
then A3:Z c= dom arcsin by VALUED_1:def 5;
Z c= dom f1 /\ (dom (( #R (1/2))*(f2-#Z 2)) \ (( #R (1/2))*(f2-#Z 2))"{0})
by A2,RFUNCT_1:def 1;
then
A4:Z c= dom f1 & Z c= dom (( #R (1/2))*(f2-#Z 2)) \ (( #R (1/2))*(f2-#Z 2))"{0}
by XBOOLE_1:18;
then Z c= dom f1 /\ dom arcsin by A3,XBOOLE_1:19;
then A5:Z c= dom (f1(#)arcsin) by VALUED_1:def 4;
A6:Z c= dom ((( #R (1/2))*(f2-#Z 2))^) by A4,RFUNCT_1:def 2;
dom ((( #R (1/2))*(f2-#Z 2))^) c= dom (( #R (1/2))*(f2-#Z 2))
by RFUNCT_1:1; then
A7:Z c= dom (( #R (1/2))*(f2-#Z 2)) by A6;
A8:arcsin is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:83;
then A9:a(#)arcsin is_differentiable_on Z by A2,FDIFF_1:20;
A10:for x st x in Z holds f1.x = a*x+b by A1;
then A11:f1 is_differentiable_on Z by A4,FDIFF_1:23;
set f3=#Z 2;
for x st x in Z holds (f2-#Z 2).x >0
proof
let x;
assume
A12:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A13:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f2-f3) by A7,FUNCT_1:11;
then (f2-f3).x = f2.x - f3.x by A12,VALUED_1:13
.=f2.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f2.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f2.x - (x*(x #Z 1)) by PREPOWER:35
.=f2.x - x*x by PREPOWER:35
.=1 - x*x by A1,A12;
hence thesis by A13;
end;
then for x st x in Z holds f2.x=1 & (f2-#Z 2).x >0 by A1;
then A14:(( #R (1/2))*(f2-#Z 2)) is_differentiable_on Z by A7,FDIFF_7:22;
x in Z implies (( #R (1/2))*(f2-#Z 2)).x<>0 by A6,RFUNCT_1:3;
then f1/(( #R (1/2))*(f2-#Z 2)) is_differentiable_on Z
by A11,A14,FDIFF_2:21;
then f is_differentiable_on Z by A1,A9,FDIFF_1:18;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A15:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A16:f1(#)(arcsin) is_differentiable_on Z by A5,A8,A11,FDIFF_1:21;
A17:for x st x in Z holds f.x=a*arcsin.x+(a*x+b)/sqrt(1-x^2)
proof
let x;
assume
A18:x in Z;
then
A19:x in dom (f2-#Z 2) & (f2-#Z 2).x in dom ( #R (1/2)) by A7,FUNCT_1:11;
then A20:(f2-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A18,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A21:0 < (1+x)*(1-x) by XREAL_1:129;
(a(#)arcsin+f1/(( #R (1/2))*(f2-#Z 2))).x
=(a(#)arcsin).x+(f1/(( #R (1/2))*(f2-#Z 2))).x by A1,A18,VALUED_1:def 1
.=a*arcsin.x+(f1/(( #R (1/2))*(f2-#Z 2))).x by VALUED_1:6
.=a*arcsin.x+f1.x/(( #R (1/2))*(f2-#Z 2)).x by A2,A18,RFUNCT_1:def 1
.=a*arcsin.x+(a*x+b)/(( #R (1/2))*(f2-#Z 2)).x by A1,A18
.=a*arcsin.x+(a*x+b)/(( #R (1/2)).((f2-#Z 2).x)) by A7,A18,FUNCT_1:12
.=a*arcsin.x+(a*x+b)/(((f2-#Z 2).x) #R (1/2)) by A20,TAYLOR_1:def 4
.=a*arcsin.x+(a*x+b)/((f2.x-(( #Z 2).x)) #R (1/2)) by A19,VALUED_1:13
.=a*arcsin.x+(a*x+b)/((f2.x-(x #Z 2)) #R (1/2)) by TAYLOR_1:def 1
.=a*arcsin.x+(a*x+b)/((f2.x-x^2) #R (1/2)) by FDIFF_7:1
.=a*arcsin.x+(a*x+b)/((1-x^2) #R (1/2)) by A1,A18
.=a*arcsin.x+(a*x+b)/sqrt(1-x^2) by A21,FDIFF_7:2;
hence thesis by A1;
end;
A22:for x being Element of REAL
st x in dom ((f1(#)(arcsin))`|Z) holds ((f1(#)(arcsin))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((f1(#)(arcsin))`|Z);then
A23:x in Z by A16,FDIFF_1:def 7; then
((f1(#)(arcsin))`|Z).x=a*arcsin.x+(a*x+b)/sqrt(1-x^2)
by A1,A10,A5,FDIFF_7:18
.=f.x by A17,A23;
hence thesis;
end;
dom ((f1(#)(arcsin))`|Z)=dom f by A1,A16,FDIFF_1:def 7;
then ((f1(#)(arcsin))`|Z)= f by A22,PARTFUN1:5;
hence thesis by A1,A15,A16,INTEGRA5:13;
end;
::f.x=a*arccos.x-(a*x+b)/sqrt(1-x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ &
(for x st x in Z holds f1.x=a*x+b & f2.x=1) & Z = dom f &
f=a(#)arccos-f1/(( #R (1/2))*(f2-#Z 2)) implies
integral(f,A)=(f1(#)(arccos)).(upper_bound A)-(f1(#)(arccos)).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ &
(for x st x in Z holds f1.x=a*x+b & f2.x=1) & Z = dom f &
f=a(#)arccos-f1/(( #R (1/2))*(f2-#Z 2));
then
Z = dom (a(#)arccos) /\ dom (f1/(( #R (1/2))*(f2-#Z 2))) by VALUED_1:12;
then A2:Z c= dom (a(#)arccos) & Z c= dom (f1/(( #R (1/2))*(f2-#Z 2)))
by XBOOLE_1:18;
then A3:Z c= dom arccos by VALUED_1:def 5;
Z c= dom f1 /\ (dom (( #R (1/2))*(f2-#Z 2)) \ (( #R (1/2))*(f2-#Z 2))"{0})
by A2,RFUNCT_1:def 1;
then
A4:Z c= dom f1 & Z c= dom (( #R (1/2))*(f2-#Z 2)) \ (( #R (1/2))*(f2-#Z 2))"{0}
by XBOOLE_1:18;
then Z c= dom f1 /\ dom arccos by A3,XBOOLE_1:19;
then A5:Z c= dom (f1(#)arccos) by VALUED_1:def 4;
A6:Z c= dom ((( #R (1/2))*(f2-#Z 2))^) by A4,RFUNCT_1:def 2;
dom ((( #R (1/2))*(f2-#Z 2))^) c= dom (( #R (1/2))*(f2-#Z 2))
by RFUNCT_1:1; then
A7:Z c= dom (( #R (1/2))*(f2-#Z 2)) by A6;
A8:arccos is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:106;
then A9:a(#)arccos is_differentiable_on Z by A2,FDIFF_1:20;
A10:for x st x in Z holds f1.x = a*x+b by A1;
then A11:f1 is_differentiable_on Z by A4,FDIFF_1:23;
set f3=#Z 2;
for x st x in Z holds (f2-#Z 2).x >0
proof
let x;
assume
A12:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A13:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f2-f3) by A7,FUNCT_1:11;
then (f2-f3).x = f2.x - f3.x by A12,VALUED_1:13
.=f2.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f2.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f2.x - (x*(x #Z 1)) by PREPOWER:35
.=f2.x - x*x by PREPOWER:35
.=1 - x*x by A1,A12;
hence thesis by A13;
end;
then for x st x in Z holds f2.x=1 & (f2-#Z 2).x >0 by A1;
then A14:(( #R (1/2))*(f2-#Z 2)) is_differentiable_on Z by A7,FDIFF_7:22;
x in Z implies (( #R (1/2))*(f2-#Z 2)).x<>0 by A6,RFUNCT_1:3;
then f1/(( #R (1/2))*(f2-#Z 2)) is_differentiable_on Z
by A11,A14,FDIFF_2:21;
then f is_differentiable_on Z by A1,A9,FDIFF_1:19;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A15:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A16:f1(#)(arccos) is_differentiable_on Z by A5,A8,A11,FDIFF_1:21;
A17:for x st x in Z holds f.x=a*arccos.x-(a*x+b)/sqrt(1-x^2)
proof
let x;
assume
A18:x in Z;
then
A19:x in dom (f2-#Z 2) & (f2-#Z 2).x in dom ( #R (1/2)) by A7,FUNCT_1:11;
then A20:(f2-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A18,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A21:0 < (1+x)*(1-x) by XREAL_1:129;
(a(#)arccos-f1/(( #R (1/2))*(f2-#Z 2))).x
=(a(#)arccos).x-(f1/(( #R (1/2))*(f2-#Z 2))).x by A1,A18,VALUED_1:13
.=a*arccos.x-(f1/(( #R (1/2))*(f2-#Z 2))).x by VALUED_1:6
.=a*arccos.x-f1.x/(( #R (1/2))*(f2-#Z 2)).x by A2,A18,RFUNCT_1:def 1
.=a*arccos.x-(a*x+b)/(( #R (1/2))*(f2-#Z 2)).x by A1,A18
.=a*arccos.x-(a*x+b)/(( #R (1/2)).((f2-#Z 2).x)) by A7,A18,FUNCT_1:12
.=a*arccos.x-(a*x+b)/(((f2-#Z 2).x) #R (1/2)) by A20,TAYLOR_1:def 4
.=a*arccos.x-(a*x+b)/((f2.x-(( #Z 2).x)) #R (1/2)) by A19,VALUED_1:13
.=a*arccos.x-(a*x+b)/((f2.x-(x #Z 2)) #R (1/2)) by TAYLOR_1:def 1
.=a*arccos.x-(a*x+b)/((f2.x-x^2) #R (1/2)) by FDIFF_7:1
.=a*arccos.x-(a*x+b)/((1-x^2) #R (1/2)) by A1,A18
.=a*arccos.x-(a*x+b)/sqrt(1-x^2) by A21,FDIFF_7:2;
hence thesis by A1;
end;
A22:for x being Element of REAL
st x in dom ((f1(#)(arccos))`|Z) holds ((f1(#)(arccos))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((f1(#)(arccos))`|Z);then
A23:x in Z by A16,FDIFF_1:def 7; then
((f1(#)(arccos))`|Z).x=a*arccos.x-(a*x+b)/sqrt(1-x^2)
by A1,A10,A5,FDIFF_7:19
.=f.x by A17,A23;
hence thesis;
end;
dom ((f1(#)(arccos))`|Z)=dom f by A1,A16,FDIFF_1:def 7;
then ((f1(#)(arccos))`|Z)= f by A22,PARTFUN1:5;
hence thesis by A1,A15,A16,INTEGRA5:13;
end;
::f.x=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2))
theorem
A c= Z & (for x st x in Z holds g.x=1 & f1.x=x/a & f1.x>-1 & f1.x<1)
& Z = dom f & f|A is continuous
& f=arcsin*f1+(id Z)/(a(#)(( #R (1/2))*(g-f1^2))) implies
integral(f,A)=((id Z)(#)((arcsin)*f1)).(upper_bound A)
-((id Z)(#)((arcsin)*f1)).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds g.x=1 & f1.x=x/a & f1.x>-1 & f1.x<1)
& Z = dom f & f|A is continuous
& f=arcsin*f1+(id Z)/(a(#)(( #R (1/2))*(g-f1^2)));
then Z = dom (arcsin*f1) /\ dom ((id Z)/(a(#)(( #R (1/2))*(g-f1^2))))
by VALUED_1:def 1;
then A2:Z c= dom (arcsin*f1) & Z c= dom ((id Z)/(a(#)(( #R (1/2))*(g-f1^2))))
by XBOOLE_1:18;
Z c= dom id Z /\ dom (arcsin*f1) by A2,XBOOLE_1:19;
then A3:Z c= dom ((id Z)(#)((arcsin)*f1)) by VALUED_1:def 4;
Z c= dom (id Z) /\ (dom (a(#)(( #R (1/2))*(g-f1^2)))
\ (a(#)(( #R (1/2))*(g-f1^2)))"{0})
by A2,RFUNCT_1:def 1;then
Z c= dom (a(#)(( #R (1/2))*(g-f1^2))) \ (a(#)(( #R (1/2))*(g-f1^2)))"{0}
by XBOOLE_1:18;
then A4:Z c= dom ((a(#)(( #R (1/2))*(g-f1^2)))^) by RFUNCT_1:def 2;
dom ((a(#)(( #R (1/2))*(g-f1^2)))^) c= dom (a(#)(( #R (1/2))*(g-f1^2)))
by RFUNCT_1:1; then
Z c= dom (a(#)(( #R (1/2))*(g-f1^2))) by A4;
then A5:Z c= dom (( #R (1/2))*(g-f1^2)) by VALUED_1:def 5;
A6:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A7:for x st x in Z holds f1.x=x/a & f1.x>-1 & f1.x<1 by A1;then
A8:(id Z)(#)((arcsin)*f1) is_differentiable_on Z by A3,FDIFF_7:25;
A9:for x st x in Z holds f.x=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2))
proof
let x;
assume
A10:x in Z;
then
A11:x in dom (g-f1^2) & (g-f1^2).x in dom ( #R (1/2)) by A5,FUNCT_1:11;
then A12:(g-f1^2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < f1.x & f1.x < 1 by A1,A10; then
0 < 1+f1.x & 0 < 1-f1.x by XREAL_1:50,148; then
A13:0 < (1+f1.x)*(1-f1.x) by XREAL_1:129;
A14: f1.x=x/a by A1,A10;
(arcsin*f1+(id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x
=(arcsin*f1).x+((id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x
by A1,A10,VALUED_1:def 1
.=arcsin.(f1.x)+((id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x
by A2,A10,FUNCT_1:12
.=arcsin.(x/a)+((id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x by A1,A10
.=arcsin.(x/a)+(id Z).x/(a(#)(( #R (1/2))*(g-f1^2))).x
by A2,A10,RFUNCT_1:def 1
.=arcsin.(x/a)+x/(a(#)(( #R (1/2))*(g-f1^2))).x by A10,FUNCT_1:18
.=arcsin.(x/a)+x/(a*(( #R (1/2))*(g-f1^2)).x) by VALUED_1:6
.=arcsin.(x/a)+x/(a*(( #R (1/2)).((g-f1^2).x))) by A5,A10,FUNCT_1:12
.=arcsin.(x/a)+x/(a*(((g-f1^2).x) #R (1/2))) by A12,TAYLOR_1:def 4
.=arcsin.(x/a)+x/(a*((g.x-((f1^2).x)) #R (1/2))) by A11,VALUED_1:13
.=arcsin.(x/a)+x/(a*((g.x-((f1.x)^2)) #R (1/2))) by VALUED_1:11
.=arcsin.(x/a)+x/(a*((1-(f1.x)^2) #R (1/2))) by A1,A10
.=arcsin.(x/a)+x/(a*((1-(x/a)^2) #R (1/2))) by A1,A10
.=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2)) by A14,A13,FDIFF_7:2;
hence thesis by A1;
end;
A15:for x being Element of REAL st x in dom (((id Z)(#)((arcsin)*f1))`|Z) holds
(((id Z)(#)((arcsin)*f1))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)((arcsin)*f1))`|Z);then
A16:x in Z by A8,FDIFF_1:def 7; then
(((id Z)(#)((arcsin)*f1))`|Z).x=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2))
by A3,A7,FDIFF_7:25
.=f.x by A9,A16;
hence thesis;
end;
dom (((id Z)(#)((arcsin)*f1))`|Z)=dom f by A1,A8,FDIFF_1:def 7;
then (((id Z)(#)((arcsin)*f1))`|Z)= f by A15,PARTFUN1:5;
hence thesis by A1,A6,A8,INTEGRA5:13;
end;
::f.x=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2))
theorem
A c= Z & (for x st x in Z holds g.x=1 & f1.x=x/a & f1.x>-1 & f1.x<1)
& Z = dom f & f|A is continuous
& f=arccos*f1-(id Z)/(a(#)(( #R (1/2))*(g-f1^2))) implies
integral(f,A)=((id Z)(#)(arccos*f1)).(upper_bound A)
-((id Z)(#)(arccos*f1)).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds g.x=1 & f1.x=x/a & f1.x>-1 & f1.x<1)
& Z = dom f & f|A is continuous
& f=arccos*f1-(id Z)/(a(#)(( #R (1/2))*(g-f1^2)));
then Z = dom (arccos*f1) /\ dom ((id Z)/(a(#)(( #R (1/2))*(g-f1^2))))
by VALUED_1:12;
then A2:Z c= dom (arccos*f1) & Z c= dom ((id Z)/(a(#)(( #R (1/2))*(g-f1^2))))
by XBOOLE_1:18;
Z c= dom id Z /\ dom (arccos*f1) by A2,XBOOLE_1:19;
then A3:Z c= dom ((id Z)(#)((arccos)*f1)) by VALUED_1:def 4;
Z c= dom (id Z) /\ (dom (a(#)(( #R (1/2))*(g-f1^2)))
\ (a(#)(( #R (1/2))*(g-f1^2)))"{0})
by A2,RFUNCT_1:def 1;then
Z c= dom (a(#)(( #R (1/2))*(g-f1^2))) \ (a(#)(( #R (1/2))*(g-f1^2)))"{0}
by XBOOLE_1:18;
then A4:Z c= dom ((a(#)(( #R (1/2))*(g-f1^2)))^) by RFUNCT_1:def 2;
dom ((a(#)(( #R (1/2))*(g-f1^2)))^) c= dom (a(#)(( #R (1/2))*(g-f1^2)))
by RFUNCT_1:1; then
Z c= dom (a(#)(( #R (1/2))*(g-f1^2))) by A4;
then A5:Z c= dom (( #R (1/2))*(g-f1^2)) by VALUED_1:def 5;
A6:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A7:for x st x in Z holds f1.x=x/a & f1.x>-1 & f1.x<1 by A1;then
A8:(id Z)(#)((arccos)*f1) is_differentiable_on Z by A3,FDIFF_7:26;
A9:for x st x in Z holds f.x=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2))
proof
let x;
assume
A10:x in Z;
then
A11:x in dom (g-f1^2) & (g-f1^2).x in dom ( #R (1/2)) by A5,FUNCT_1:11;
then A12:(g-f1^2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < f1.x & f1.x < 1 by A1,A10; then
0 < 1+f1.x & 0 < 1-f1.x by XREAL_1:50,148; then
A13:0 < (1+f1.x)*(1-f1.x) by XREAL_1:129;
A14:f1.x=x/a by A1,A10;
(arccos*f1-(id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x
=(arccos*f1).x-((id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x
by A1,A10,VALUED_1:13
.=arccos.(f1.x)-((id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x
by A2,A10,FUNCT_1:12
.=arccos.(x/a)-((id Z)/(a(#)(( #R (1/2))*(g-f1^2)))).x by A1,A10
.=arccos.(x/a)-(id Z).x/(a(#)(( #R (1/2))*(g-f1^2))).x
by A2,A10,RFUNCT_1:def 1
.=arccos.(x/a)-x/(a(#)(( #R (1/2))*(g-f1^2))).x by A10,FUNCT_1:18
.=arccos.(x/a)-x/(a*(( #R (1/2))*(g-f1^2)).x) by VALUED_1:6
.=arccos.(x/a)-x/(a*(( #R (1/2)).((g-f1^2).x))) by A5,A10,FUNCT_1:12
.=arccos.(x/a)-x/(a*(((g-f1^2).x) #R (1/2))) by A12,TAYLOR_1:def 4
.=arccos.(x/a)-x/(a*((g.x-((f1^2).x)) #R (1/2))) by A11,VALUED_1:13
.=arccos.(x/a)-x/(a*((g.x-((f1.x)^2)) #R (1/2))) by VALUED_1:11
.=arccos.(x/a)-x/(a*((1-(f1.x)^2) #R (1/2))) by A1,A10
.=arccos.(x/a)-x/(a*((1-(x/a)^2) #R (1/2))) by A1,A10
.=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) by A14,A13,FDIFF_7:2;
hence thesis by A1;
end;
A15:for x being Element of REAL st x in dom (((id Z)(#)((arccos)*f1))`|Z) holds
(((id Z)(#)((arccos)*f1))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((id Z)(#)((arccos)*f1))`|Z);then
A16:x in Z by A8,FDIFF_1:def 7; then
(((id Z)(#)((arccos)*f1))`|Z).x=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2))
by A3,A7,FDIFF_7:26
.=f.x by A9,A16;
hence thesis;
end;
dom (((id Z)(#)((arccos)*f1))`|Z)=dom f by A1,A8,FDIFF_1:def 7;
then (((id Z)(#)((arccos)*f1))`|Z)= f by A15,PARTFUN1:5;
hence thesis by A1,A6,A8,INTEGRA5:13;
end;
::f.x = n*(sin.x) #Z (n-1)/(cos.x) #Z (n+1)
theorem
A c= Z & f=(n(#)(( #Z (n-1))*sin))/(( #Z (n+1))*cos) &
1<=n & Z c= dom (( #Z n)*tan) & Z = dom f
implies
integral(f,A)=(( #Z n)*tan).(upper_bound A)-(( #Z n)*tan).(lower_bound A)
proof
assume
A1:A c= Z & f=n(#)(( #Z (n-1))*sin)/(( #Z (n+1))*cos)
& 1<=n & Z c= dom (( #Z n)*tan) & Z = dom f;
then Z = dom (n(#)(( #Z (n-1))*sin)) /\
(dom (( #Z (n+1))*cos) \ (( #Z (n+1))*cos)"{0})
by RFUNCT_1:def 1;
then A2:Z c= dom (n(#)(( #Z (n-1))*sin)) &
Z c= dom (( #Z (n+1))*cos) \ (( #Z (n+1))*cos)"{0} by XBOOLE_1:18;
then A3:Z c= dom ((( #Z (n+1))*cos)^) by RFUNCT_1:def 2;
dom ((( #Z (n+1))*cos)^) c= dom (( #Z (n+1))*cos) by RFUNCT_1:1;then
A4:Z c= dom (( #Z (n+1))*cos) by A3;
A5: x in Z implies (( #Z (n+1))*cos).x <> 0
proof
assume x in Z;
then x in dom (n(#)(( #Z (n-1))*sin)) /\
(dom (( #Z (n+1))*cos) \ (( #Z (n+1))*cos)"{0})
by A1,RFUNCT_1:def 1;
then x in dom (( #Z (n+1))*cos) \ (( #Z (n+1))*cos)"{0}
by XBOOLE_0:def 4; then
x in dom ((( #Z (n+1))*cos)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
A6:Z c= dom (( #Z (n-1))*sin) by A2,VALUED_1:def 5;
A7:#Z (n-1)*sin is_differentiable_in x
proof
consider m being Nat such that
A8: n = m + 1 by A1,NAT_1:6;
sin is_differentiable_in x by SIN_COS:64;
hence thesis by A8,TAYLOR_1:3;
end;
#Z (n-1)*sin is_differentiable_on Z
proof
for x st x in Z holds #Z (n-1)*sin is_differentiable_in x by A7;
hence thesis by A6,FDIFF_1:9;
end;
then A9:(n(#)(( #Z (n-1))*sin)) is_differentiable_on Z by A2,FDIFF_1:20;
A10: #Z (n+1)*cos is_differentiable_in x
proof
cos is_differentiable_in x by SIN_COS:63;
hence thesis by TAYLOR_1:3;
end;
(( #Z (n+1))*cos) is_differentiable_on Z
proof
for x st x in Z holds ( #Z (n+1))*cos is_differentiable_in x by A10;
hence thesis by A4,FDIFF_1:9;
end;
then f|Z is continuous by A1,A5,A9,FDIFF_1:25,FDIFF_2:21;
then f|A is continuous by A1,FCONT_1:16;
then A11:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A12:(( #Z n)*tan) is_differentiable_on Z by A1,FDIFF_8:20;
A13:for x st x in Z holds f.x = n*(sin.x) #Z (n-1)/(cos.x) #Z (n+1)
proof
let x;
assume
A14:x in Z;
then ((n(#)(( #Z (n-1))*sin))/(( #Z (n+1))*cos)).x
=(n(#)(( #Z (n-1))*sin)).x/(( #Z (n+1))*cos).x by A1,RFUNCT_1:def 1
.=n*(( #Z (n-1))*sin).x/(( #Z (n+1))*cos).x by VALUED_1:6
.=n*(( #Z (n-1)).(sin.x))/(( #Z (n+1))*cos).x by A6,A14,FUNCT_1:12
.=n*(sin.x) #Z (n-1)/(( #Z (n+1))*cos).x by TAYLOR_1:def 1
.=n*(sin.x) #Z (n-1)/(( #Z (n+1)).(cos.x)) by A4,A14,FUNCT_1:12
.=n*(sin.x) #Z (n-1)/(cos.x) #Z (n+1) by TAYLOR_1:def 1;
hence thesis by A1;
end;
A15:for x being Element of REAL
st x in dom ((( #Z n)*tan)`|Z) holds ((( #Z n)*tan)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((( #Z n)*tan)`|Z);then
A16: x in Z by A12,FDIFF_1:def 7; then
((( #Z n)*tan)`|Z).x = n*(sin.x) #Z (n-1)/(cos.x) #Z (n+1) by A1,FDIFF_8:20
.=f.x by A13,A16;
hence thesis;
end;
dom ((( #Z n)*tan)`|Z) = dom f by A1,A12,FDIFF_1:def 7;
then ((( #Z n)*tan)`|Z)=f by A15,PARTFUN1:5;
hence thesis by A1,A11,FDIFF_8:20,INTEGRA5:13;
end;
::f.x=n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1)
theorem
A c= Z & f=(n(#)(( #Z (n-1))*cos))/(( #Z (n+1))*sin)
& 1<=n & Z c= dom (( #Z n)*cot) & Z = dom f
implies
integral(f,A)=(-( #Z n)*cot).(upper_bound A)-(-( #Z n)*cot).(lower_bound A)
proof
assume
A1:A c= Z & f=(n(#)(( #Z (n-1))*cos))/(( #Z (n+1))*sin)
& 1<=n & Z c= dom (( #Z n)*cot) & Z = dom f;
then Z = dom (n(#)(( #Z (n-1))*cos)) /\
(dom (( #Z (n+1))*sin) \ (( #Z (n+1))*sin)"{0})
by RFUNCT_1:def 1;
then A2:Z c= dom (n(#)(( #Z (n-1))*cos)) &
Z c= dom (( #Z (n+1))*sin) \ (( #Z (n+1))*sin)"{0} by XBOOLE_1:18;
then A3:Z c= dom ((( #Z (n+1))*sin)^) by RFUNCT_1:def 2;
dom ((( #Z (n+1))*sin)^) c= dom (( #Z (n+1))*sin) by RFUNCT_1:1;then
A4:Z c= dom (( #Z (n+1))*sin) by A3;
A5: x in Z implies (( #Z (n+1))*sin).x <> 0
proof
assume x in Z;
then x in dom (n(#)(( #Z (n-1))*cos)) /\
(dom (( #Z (n+1))*sin) \ (( #Z (n+1))*sin)"{0})
by A1,RFUNCT_1:def 1;
then x in dom (( #Z (n+1))*sin) \ (( #Z (n+1))*sin)"{0}
by XBOOLE_0:def 4; then
x in dom ((( #Z (n+1))*sin)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
A6:Z c= dom (( #Z (n-1))*cos) by A2,VALUED_1:def 5;
A7:#Z (n-1)*cos is_differentiable_in x
proof
consider m being Nat such that
A8: n = m + 1 by A1,NAT_1:6;
cos is_differentiable_in x by SIN_COS:63;
hence thesis by A8,TAYLOR_1:3;
end;
#Z (n-1)*cos is_differentiable_on Z
proof
for x st x in Z holds #Z (n-1)*cos is_differentiable_in x by A7;
hence thesis by A6,FDIFF_1:9;
end;
then A9:(n(#)(( #Z (n-1))*cos)) is_differentiable_on Z by A2,FDIFF_1:20;
A10: #Z (n+1)*sin is_differentiable_in x
proof
sin is_differentiable_in x by SIN_COS:64;
hence thesis by TAYLOR_1:3;
end;
(( #Z (n+1))*sin) is_differentiable_on Z
proof
for x st x in Z holds ( #Z (n+1))*sin is_differentiable_in x by A10;
hence thesis by A4,FDIFF_1:9;
end;
then f|Z is continuous by A1,A5,A9,FDIFF_1:25,FDIFF_2:21;
then f|A is continuous by A1,FCONT_1:16;
then A11:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A12:( #Z n)*cot is_differentiable_on Z by A1,FDIFF_8:21;
A13:dom (( #Z n)*cot) c= dom cot by RELAT_1:25;
A14:Z c= dom (-( #Z n)*cot) by A1,VALUED_1:8;
then A15:(-1)(#)(( #Z n)*cot) is_differentiable_on Z by A12,FDIFF_1:20;
A16:for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom (cos/sin) by A1,FUNCT_1:11;
hence thesis by FDIFF_8:2;
end;
A17:for x st x in Z holds ((-( #Z n)*cot)`|Z).x
=n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1)
proof
let x;
assume
A18:x in Z;then
A19: sin.x<>0 by A16; then
A20: cot is_differentiable_in x by FDIFF_7:47;
consider m being Nat such that
A21: n = m + 1 by A1,NAT_1:6;
set m = n-1;
A22:( #Z n)*cot is_differentiable_in x by A12,A18,FDIFF_1:9;
((-( #Z n)*cot)`|Z).x=diff(-( #Z n)*cot,x) by A15,A18,FDIFF_1:def 7
.=(-1)*diff(( #Z n)*cot,x) by A22,FDIFF_1:15
.=(-1)*(n*(cot.x) #Z (n-1) * diff(cot,x))
by A20,TAYLOR_1:3
.=(-1)*(n*(cot.x) #Z (n-1) *(-1/(sin.x)^2))
by A19,FDIFF_7:47
.=(-1)*(-(n*(cot.x) #Z (n-1))/(sin.x)^2)
.=(-1)*(-n*((cos.x) #Z m/(sin.x) #Z m)/(sin.x)^2)
by A1,A13,A18,A21,FDIFF_8:3,XBOOLE_1:1
.=(-1)*(-n*(cos.x) #Z (n-1)/(sin.x) #Z (n-1)/(sin.x)^2)
.=(-1)*(-n*(cos.x) #Z (n-1)/((sin.x) #Z (n-1)*(sin.x)^2))
by XCMPLX_1:78
.=(-1)*(-n*((cos.x) #Z (n-1))/((sin.x) #Z (n-1)*(sin.x) #Z 2))
by FDIFF_7:1
.=(-1)*(-n*((cos.x) #Z (n-1))/((sin.x) #Z (n-1+2)))
by A16,A18,PREPOWER:44
.=n*((cos.x) #Z (n-1))/(sin.x) #Z (n+1);
hence thesis;
end;
A23:for x st x in Z holds f.x = n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1)
proof
let x;
assume
A24:x in Z;
then ((n(#)(( #Z (n-1))*cos))/(( #Z (n+1))*sin)).x
=(n(#)(( #Z (n-1))*cos)).x/(( #Z (n+1))*sin).x by A1,RFUNCT_1:def 1
.=n*(( #Z (n-1))*cos).x/(( #Z (n+1))*sin).x by VALUED_1:6
.=n*(( #Z (n-1)).(cos.x))/(( #Z (n+1))*sin).x by A6,A24,FUNCT_1:12
.=n*(cos.x) #Z (n-1)/(( #Z (n+1))*sin).x by TAYLOR_1:def 1
.=n*(cos.x) #Z (n-1)/(( #Z (n+1)).(sin.x)) by A4,A24,FUNCT_1:12
.=n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1) by TAYLOR_1:def 1;
hence thesis by A1;
end;
A25:for x being Element of REAL
st x in dom ((-( #Z n)*cot)`|Z) holds ((-( #Z n)*cot)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((-( #Z n)*cot)`|Z);then
A26:x in Z by A15,FDIFF_1:def 7; then
((-( #Z n)*cot)`|Z).x = n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1) by A17
.=f.x by A23,A26;
hence thesis;
end;
dom ((-( #Z n)*cot)`|Z) = dom f by A1,A15,FDIFF_1:def 7;
then ((-( #Z n)*cot)`|Z)=f by A25,PARTFUN1:5;
hence thesis by A1,A11,A12,A14,FDIFF_1:20,INTEGRA5:13;
end;
::f.x=(sin.(a*x))^2/(cos.(a*x))^2
theorem
A c= Z & Z c= dom (tan*f1) & f=(sin*f1)^2/(cos*f1)^2
& (for x st x in Z holds f1.x=a*x & a<>0) & Z = dom f
implies
integral(f,A)=((1/a)(#)(tan*f1)-id Z).(upper_bound A)
-((1/a)(#)(tan*f1)-id Z).(lower_bound A)
proof
assume
A1: A c= Z & Z c= dom (tan*f1) & f=(sin*f1)^2/(cos*f1)^2
& (for x st x in Z holds f1.x=a*x & a<>0) & Z = dom f;
then A2:Z c= dom ((1/a)(#)(tan*f1)) by VALUED_1:def 5;
Z c= dom ((1/a)(#)(tan*f1)) /\ dom id Z by A2,XBOOLE_1:19;
then A3:Z c= dom ((1/a)(#)(tan*f1)-id Z) by VALUED_1:12;
A4:for x st x in Z holds f1.x=a*x+0 by A1;
Z = dom ((sin*f1)^2) /\ (dom ((cos*f1)^2) \ ((cos*f1)^2)"{0})
by A1,RFUNCT_1:def 1;
then A5:Z c= dom ((sin*f1)^2) & Z c= dom ((cos*f1)^2) \ ((cos*f1)^2)"{0}
by XBOOLE_1:18;
then A6:Z c= dom (sin*f1) by VALUED_1:11;
A7:Z c= dom (((cos*f1)^2)^) by A5,RFUNCT_1:def 2;
dom (((cos*f1)^2)^) c= dom ((cos*f1)^2) by RFUNCT_1:1;then
Z c= dom ((cos*f1)^2) by A7;
then A8:Z c= dom (cos*f1) by VALUED_1:11;
A9:sin*f1 is_differentiable_on Z by A6,A4,FDIFF_4:37;
A10:cos*f1 is_differentiable_on Z by A4,A8,FDIFF_4:38;
A11:(sin*f1)^2 is_differentiable_on Z by A9,FDIFF_2:20;
A12:(cos*f1)^2 is_differentiable_on Z by A10,FDIFF_2:20;
x in Z implies ((cos*f1)^2).x<>0
proof
assume x in Z;
then x in dom ((sin*f1)^2) /\ (dom ((cos*f1)^2) \ ((cos*f1)^2)"{0})
by A1,RFUNCT_1:def 1;
then x in dom ((cos*f1)^2) \ ((cos*f1)^2)"{0} by XBOOLE_0:def 4;
then x in dom (((cos*f1)^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then f is_differentiable_on Z by A1,A11,A12,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A13:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A14:((1/a)(#)(tan*f1)-id Z) is_differentiable_on Z by A1,A3,FDIFF_8:26;
A15:for x st x in Z holds f.x = (sin.(a*x))^2/(cos.(a*x))^2
proof
let x;
assume
A16:x in Z;
then ((sin*f1)^2/(cos*f1)^2).x
=((sin*f1)^2).x/((cos*f1)^2).x by A1,RFUNCT_1:def 1
.=((sin*f1).x)^2/((cos*f1)^2).x by VALUED_1:11
.=((sin*f1).x)^2/((cos*f1).x)^2 by VALUED_1:11
.=(sin.(f1.x))^2/((cos*f1).x)^2 by A6,A16,FUNCT_1:12
.=(sin.(f1.x))^2/(cos.(f1.x))^2 by A8,A16,FUNCT_1:12
.=(sin.(a*x))^2/(cos.(f1.x))^2 by A16,A1
.=(sin.(a*x))^2/(cos.(a*x))^2 by A16,A1;
hence thesis by A1;
end;
A17:for x being Element of REAL st x in dom(((1/a)(#)(tan*f1)-id Z)`|Z) holds
(((1/a)(#)(tan*f1)-id Z)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((1/a)(#)(tan*f1)-id Z)`|Z);then
A18: x in Z by A14,FDIFF_1:def 7; then
(((1/a)(#)(tan*f1)-id Z)`|Z).x
=(sin.(a*x))^2/(cos.(a*x))^2 by A1,A3,FDIFF_8:26
.=f.x by A15,A18;
hence thesis;
end;
dom (((1/a)(#)(tan*f1)-id Z)`|Z)=dom f by A1,A14,FDIFF_1:def 7;
then (((1/a)(#)(tan*f1)-id Z)`|Z)=f by A17,PARTFUN1:5;
hence thesis by A1,A13,A14,INTEGRA5:13;
end;
::f.x=(cos.(a*x))^2/(sin.(a*x))^2
theorem
A c= Z & Z c= dom (cot*f1) & f=(cos*f1)^2/(sin*f1)^2 &
(for x st x in Z holds f1.x=a*x & a<>0) & Z = dom f
implies
integral(f,A)=((-1/a)(#)(cot*f1)-id Z).(upper_bound A)
-((-1/a)(#)(cot*f1)-id Z).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (cot*f1) & f=(cos*f1)^2/(sin*f1)^2 &
(for x st x in Z holds f1.x=a*x & a<>0) & Z = dom f;
then A2:Z c= dom ((-1/a)(#)(cot*f1)) by VALUED_1:def 5;
Z c= dom ((-1/a)(#)(cot*f1)) /\ dom id Z by A2,XBOOLE_1:19;
then A3:Z c= dom ((-1/a)(#)(cot*f1)-id Z) by VALUED_1:12;
A4:for x st x in Z holds f1.x=a*x+0 by A1;
Z = dom ((cos*f1)^2) /\ (dom ((sin*f1)^2) \ ((sin*f1)^2)"{0})
by A1,RFUNCT_1:def 1;
then A5:Z c= dom ((cos*f1)^2) & Z c= dom ((sin*f1)^2) \ ((sin*f1)^2)"{0}
by XBOOLE_1:18;
then A6:Z c= dom (cos*f1) by VALUED_1:11;
A7:Z c= dom (((sin*f1)^2)^) by A5,RFUNCT_1:def 2;
dom (((sin*f1)^2)^) c= dom ((sin*f1)^2) by RFUNCT_1:1;then
Z c= dom ((sin*f1)^2) by A7;
then A8:Z c= dom (sin*f1) by VALUED_1:11;
then A9:sin*f1 is_differentiable_on Z by A4,FDIFF_4:37;
A10:cos*f1 is_differentiable_on Z by A4,A6,FDIFF_4:38;
A11:(sin*f1)^2 is_differentiable_on Z by A9,FDIFF_2:20;
A12:(cos*f1)^2 is_differentiable_on Z by A10,FDIFF_2:20;
x in Z implies ((sin*f1)^2).x<>0
proof
assume x in Z;
then x in dom ((cos*f1)^2) /\ (dom ((sin*f1)^2) \ ((sin*f1)^2)"{0})
by A1,RFUNCT_1:def 1;
then x in dom ((sin*f1)^2) \ ((sin*f1)^2)"{0} by XBOOLE_0:def 4;
then x in dom (((sin*f1)^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then f is_differentiable_on Z by A1,A11,A12,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A13:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A14:((-1/a)(#)(cot*f1)-id Z) is_differentiable_on Z by A1,A3,FDIFF_8:27;
A15:for x st x in Z holds f.x =(cos.(a*x))^2/(sin.(a*x))^2
proof
let x;
assume
A16:x in Z;
then ((cos*f1)^2/(sin*f1)^2).x
=((cos*f1)^2).x/((sin*f1)^2).x by A1,RFUNCT_1:def 1
.=((cos*f1).x)^2/((sin*f1)^2).x by VALUED_1:11
.=((cos*f1).x)^2/((sin*f1).x)^2 by VALUED_1:11
.=(cos.(f1.x))^2/((sin*f1).x)^2 by A6,A16,FUNCT_1:12
.=(cos.(f1.x))^2/(sin.(f1.x))^2 by A8,A16,FUNCT_1:12
.=(cos.(a*x))^2/(sin.(f1.x))^2 by A16,A1
.=(cos.(a*x))^2/(sin.(a*x))^2 by A16,A1;
hence thesis by A1;
end;
A17:for x being Element of REAL st x in dom(((-1/a)(#)(cot*f1)-id Z)`|Z) holds
(((-1/a)(#)(cot*f1)-id Z)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((-1/a)(#)(cot*f1)-id Z)`|Z);then
A18: x in Z by A14,FDIFF_1:def 7; then
(((-1/a)(#)(cot*f1)-id Z)`|Z).x
=(cos.(a*x))^2/(sin.(a*x))^2 by A1,A3,FDIFF_8:27
.=f.x by A15,A18;
hence thesis;
end;
dom (((-1/a)(#)(cot*f1)-id Z)`|Z)=dom f by A1,A14,FDIFF_1:def 7;
then (((-1/a)(#)(cot*f1)-id Z)`|Z)=f by A17,PARTFUN1:5;
hence thesis by A1,A13,A14,INTEGRA5:13;
end;
::f.x=a*sin.x/cos.x+(a*x+b)/(cos.x)^2
theorem
A c= Z & (for x st x in Z holds f1.x=a*x+b) & Z = dom f &
f=a(#)(sin/cos)+f1/cos^2 implies
integral(f,A)=(f1(#)tan).(upper_bound A)-(f1(#)tan).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=a*x+b) & Z = dom f &
f=a(#)(sin/cos)+f1/cos^2;
then A2:Z = dom (a(#)(sin/cos)) /\ dom (f1/cos^2) by VALUED_1:def 1;
then A3:Z c= dom (a(#)(sin/cos)) by XBOOLE_1:18;
then A4:Z c= dom (sin/cos) by VALUED_1:def 5;
A5:Z c= dom (f1/cos^2) by A2,XBOOLE_1:18;
dom (f1/cos^2) = dom f1 /\ (dom cos^2 \ (cos^2)"{0}) by RFUNCT_1:def 1;
then A6:Z c= dom f1 by A5,XBOOLE_1:18;
then Z c= dom f1 /\ dom tan by A4,XBOOLE_1:19;
then A7:Z c= dom (f1(#)tan) by VALUED_1:def 4;
for x st x in Z holds sin/cos is_differentiable_in x
proof
let x;
assume x in Z;then
cos.x<>0 by A4,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then sin/cos is_differentiable_on Z by A4,FDIFF_1:9;
then A8:a(#)(sin/cos) is_differentiable_on Z by A3,FDIFF_1:20;
A9:f1 is_differentiable_on Z by A1,A6,FDIFF_1:23;
cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then A10:cos^2 is_differentiable_on Z by FDIFF_2:20;
x in Z implies (cos^2).x<>0
proof
assume x in Z;then
x in dom (f1/cos^2) by A5;
then x in dom f1 /\ (dom cos^2 \ (cos^2)"{0}) by RFUNCT_1:def 1;
then x in dom cos^2 \ (cos^2)"{0} by XBOOLE_0:def 4;
then x in dom ((cos^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then f1/cos^2 is_differentiable_on Z by A9,A10,FDIFF_2:21; then
f|Z is continuous by A1,A8,FDIFF_1:18,25;then
f|A is continuous by A1,FCONT_1:16;
then A11:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A12:(f1(#)tan) is_differentiable_on Z by A1,A7,FDIFF_8:28;
A13:for x st x in Z holds f.x=a*sin.x/cos.x+(a*x+b)/(cos.x)^2
proof
let x;
assume
A14:x in Z;
then (a(#)(sin/cos)+f1/cos^2).x
=(a(#)(sin/cos)).x+(f1/cos^2).x by A1,VALUED_1:def 1
.=a*(sin/cos).x+(f1/cos^2).x by VALUED_1:6
.=a*(sin.x/cos.x)+(f1/cos^2).x by A14,A4,RFUNCT_1:def 1
.=a*sin.x/cos.x+f1.x/(cos^2).x by A14,A5,RFUNCT_1:def 1
.=a*sin.x/cos.x+f1.x/(cos.x)^2 by VALUED_1:11
.=a*sin.x/cos.x+(a*x+b)/(cos.x)^2 by A1,A14;
hence thesis by A1;
end;
A15:for x being Element of REAL st x in dom((f1(#)tan)`|Z)
holds ((f1(#)tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((f1(#)tan)`|Z);then
A16: x in Z by A12,FDIFF_1:def 7; then
((f1(#)tan)`|Z).x=a*sin.x/cos.x+(a*x+b)/(cos.x)^2 by A1,A7,FDIFF_8:28
.=f.x by A13,A16;
hence thesis;
end;
dom((f1(#)tan)`|Z)=dom f by A1,A12,FDIFF_1:def 7;
then ((f1(#)tan)`|Z)=f by A15,PARTFUN1:5;
hence thesis by A1,A11,A7,FDIFF_8:28,INTEGRA5:13;
end;
::f.x=a*cos.x/sin.x-(a*x+b)/(sin.x)^2
theorem
A c= Z & (for x st x in Z holds f1.x=a*x+b) & Z = dom f &
f=a(#)(cos/sin)-f1/sin^2 implies
integral(f,A)=(f1(#)cot).(upper_bound A)-(f1(#)cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=a*x+b) & Z = dom f &
f=a(#)(cos/sin)-f1/sin^2;
then A2:Z = dom (a(#)(cos/sin)) /\ dom (-f1/sin^2) by VALUED_1:def 1;
then A3:Z c= dom (a(#)(cos/sin)) by XBOOLE_1:18;
then A4:Z c= dom (cos/sin) by VALUED_1:def 5;
Z c= dom (-f1/sin^2) by A2,XBOOLE_1:18;
then A5:Z c= dom (f1/sin^2) by VALUED_1:8;
dom (f1/sin^2) = dom f1 /\ (dom sin^2 \ (sin^2)"{0}) by RFUNCT_1:def 1;then
A6:Z c= dom f1 by A5,XBOOLE_1:18;
then Z c= dom f1 /\ dom cot by A4,XBOOLE_1:19;
then A7:Z c= dom (f1(#)cot) by VALUED_1:def 4;
for x st x in Z holds cos/sin 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 cos/sin is_differentiable_on Z by A4,FDIFF_1:9;
then A8:a(#)(cos/sin) is_differentiable_on Z by A3,FDIFF_1:20;
A9:f1 is_differentiable_on Z by A1,A6,FDIFF_1:23;
sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then A10:sin^2 is_differentiable_on Z by FDIFF_2:20;
x in Z implies (sin^2).x<>0
proof
assume x in Z;then
x in dom (f1/sin^2) by A5;
then x in dom f1 /\ (dom sin^2 \ (sin^2)"{0}) by RFUNCT_1:def 1;
then x in dom sin^2 \ (sin^2)"{0} by XBOOLE_0:def 4;
then x in dom ((sin^2)^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then f1/sin^2 is_differentiable_on Z by A9,A10,FDIFF_2:21; then
f|Z is continuous by A1,A8,FDIFF_1:19,25;then
f|A is continuous by A1,FCONT_1:16;
then A11:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A12:(f1(#)cot) is_differentiable_on Z by A1,A7,FDIFF_8:29;
A13:for x st x in Z holds f.x=a*cos.x/sin.x-(a*x+b)/(sin.x)^2
proof
let x;
assume
A14:x in Z;
then (a(#)(cos/sin)-f1/sin^2).x
=(a(#)(cos/sin)).x-(f1/sin^2).x by A1,VALUED_1:13
.=a*(cos/sin).x-(f1/sin^2).x by VALUED_1:6
.=a*(cos.x/sin.x)-(f1/sin^2).x by A14,A4,RFUNCT_1:def 1
.=a*cos.x/sin.x-f1.x/(sin^2).x by A14,A5,RFUNCT_1:def 1
.=a*cos.x/sin.x-f1.x/(sin.x)^2 by VALUED_1:11
.=a*cos.x/sin.x-(a*x+b)/(sin.x)^2 by A1,A14;
hence thesis by A1;
end;
A15:for x being Element of REAL st x in dom((f1(#)cot)`|Z)
holds ((f1(#)cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((f1(#)cot)`|Z);then
A16: x in Z by A12,FDIFF_1:def 7; then
((f1(#)cot)`|Z).x=a*cos.x/sin.x-(a*x+b)/(sin.x)^2 by A1,A7,FDIFF_8:29
.=f.x by A13,A16;
hence thesis;
end;
dom((f1(#)cot)`|Z)=dom f by A1,A12,FDIFF_1:def 7;
then ((f1(#)cot)`|Z) = f by A15,PARTFUN1:5;
hence thesis by A1,A11,A7,FDIFF_8:29,INTEGRA5:13;
end;
::f.x=(sin.x)^2/(cos.x)^2
theorem
A c= Z & (for x st x in Z holds f.x=(sin.x)^2/(cos.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
A1:A c= Z & (for x st x in Z holds f.x=(sin.x)^2/(cos.x)^2)
& Z c= dom (tan-id Z) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan-id Z is_differentiable_on Z by A1,FDIFF_8:24;
A4: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
A5:x in Z by A3,FDIFF_1:def 7;then
((tan-id Z)`|Z).x=(sin.x)^2/(cos.x)^2 by A1,FDIFF_8:24
.=f.x by A1,A5;
hence thesis;
end;
dom ((tan-id Z)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan-id Z)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:24,INTEGRA5:13;
end;
::f.x=(cos.x)^2/(sin.x)^2
theorem
A c= Z & (for x st x in Z holds f.x=(cos.x)^2/(sin.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
A1:A c= Z & (for x st x in Z holds f.x=(cos.x)^2/(sin.x)^2)
& Z c= dom (-cot-id Z) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cot-id Z is_differentiable_on Z by A1,FDIFF_8:25;
A4: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
A5:x in Z by A3,FDIFF_1:def 7;then
((-cot-id Z)`|Z).x=(cos.x)^2/(sin.x)^2 by A1,FDIFF_8:25
.=f.x by A1,A5;
hence thesis;
end;
dom ((-cot-id Z)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cot-id Z)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:25,INTEGRA5:13;
end;
::f.x=1/(x*(1+(ln.x)^2))
theorem
A c= Z & (for x st x in Z holds f.x=1/(x*(1+(ln.x)^2))
& ln.x > -1 & ln.x < 1) & Z c= dom (arctan*ln) & Z = dom f
& f|A is continuous implies integral(f,A)=(arctan*ln).(upper_bound A)
-(arctan*ln).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=1/(x*(1+(ln.x)^2))
& ln.x > -1 & ln.x < 1) & Z c= dom (arctan*ln) & Z = dom f
& f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:for x st x in Z holds ln.x > -1 & ln.x < 1 by A1;then
A4:arctan*ln is_differentiable_on Z by A1,SIN_COS9:117;
A5:for x being Element of REAL st x in dom ((arctan*ln)`|Z)
holds ((arctan*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((arctan*ln)`|Z);then
A6:x in Z by A4,FDIFF_1:def 7;then
((arctan*ln)`|Z).x=1/(x*(1+(ln.x)^2)) by A1,A3,SIN_COS9:117
.=f.x by A1,A6;
hence thesis;
end;
dom ((arctan*ln)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((arctan*ln)`|Z)= f by A5,PARTFUN1:5;
hence thesis by A1,A2,A4,INTEGRA5:13;
end;
::f.x=-1/(x*(1+(ln.x)^2))
theorem
A c= Z & (for x st x in Z holds f.x=-1/(x*(1+(ln.x)^2))
& ln.x > -1 & ln.x < 1) & Z c= dom (arccot*ln) & Z = dom f
& f|A is continuous implies integral(f,A)=(arccot*ln).(upper_bound A)
-(arccot*ln).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=-1/(x*(1+(ln.x)^2))
& ln.x > -1 & ln.x < 1) & Z c= dom (arccot*ln) & Z = dom f
& f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:for x st x in Z holds ln.x > -1 & ln.x < 1 by A1;then
A4:arccot*ln is_differentiable_on Z by A1,SIN_COS9:118;
A5:for x being Element of REAL st x in dom ((arccot*ln)`|Z)
holds ((arccot*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((arccot*ln)`|Z);then
A6:x in Z by A4,FDIFF_1:def 7;then
((arccot*ln)`|Z).x=-1/(x*(1+(ln.x)^2)) by A1,A3,SIN_COS9:118
.=f.x by A1,A6;
hence thesis;
end;
dom ((arccot*ln)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((arccot*ln)`|Z)= f by A5,PARTFUN1:5;
hence thesis by A1,A2,A4,INTEGRA5:13;
end;
::f.x=a / sqrt(1-(a*x+b)^2)
theorem
A c= Z & (for x st x in Z holds f.x=a / sqrt(1-(a*x+b)^2)
& f1.x=a*x+b & f1.x>-1 & f1.x<1) & Z c= dom ((arcsin)*f1)
& Z = dom f & f|A is continuous implies
integral(f,A)=((arcsin)*f1).(upper_bound A)-((arcsin)*f1).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=a / sqrt(1-(a*x+b)^2)
& f1.x=a*x+b & f1.x>-1 & f1.x<1) & Z c= dom ((arcsin)*f1)
& Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:for x st x in Z holds f1.x=a*x+b & f1.x>-1 & f1.x<1 by A1;
then A4:(arcsin)*f1 is_differentiable_on Z by A1,FDIFF_7:14;
A5:for x being Element of REAL
st x in dom (((arcsin)*f1)`|Z) holds (((arcsin)*f1)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((arcsin)*f1)`|Z);then
A6:x in Z by A4,FDIFF_1:def 7; then
(((arcsin)*f1)`|Z).x=a / sqrt(1-(a*x+b)^2) by A1,A3,FDIFF_7:14
.=f.x by A1,A6;
hence thesis;
end;
dom(((arcsin)*f1)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then (((arcsin)*f1)`|Z)= f by A5,PARTFUN1:5;
hence thesis by A1,A2,A4,INTEGRA5:13;
end;
theorem
A c= Z & (for x st x in Z holds f.x=a / sqrt(1-(a*x+b)^2)
& f1.x=a*x+b & f1.x>-1 & f1.x<1) & Z c= dom ((arccos)*f1)
& Z = dom f & f|A is continuous implies
integral(f,A)=(-(arccos)*f1).(upper_bound A)-(-(arccos)*f1).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=a / sqrt(1-(a*x+b)^2)
& f1.x=a*x+b & f1.x>-1 & f1.x<1) & Z c= dom ((arccos)*f1)
& Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:for x st x in Z holds f1.x=a*x+b by A1;
A4:for x st x in Z holds f1.x=a*x+b & f1.x>-1 & f1.x<1 by A1;
A5:Z c= dom (-(arccos)*f1) by A1,VALUED_1:8;
A6:(arccos)*f1 is_differentiable_on Z by A1,A4,FDIFF_7:15;
then A7:(-1)(#)((arccos)*f1) is_differentiable_on Z by A5,FDIFF_1:20;
for y being object st y in Z holds y in dom f1 by A1,FUNCT_1:11; then
A8: Z c= dom f1; then
A9: f1 is_differentiable_on Z & for x st x in Z holds (f1`|Z).x = a
by A3,FDIFF_1:23;
A10:for x st x in Z holds ((-(arccos)*f1)`|Z).x=a / sqrt(1-(a*x+b)^2)
proof
let x;
assume
A11:x in Z;then
A12:f1 is_differentiable_in x by A9,FDIFF_1:9;
A13:f1.x > -1 & f1.x < 1 by A1,A11;
A14:(arccos)*f1 is_differentiable_in x by A6,A11,FDIFF_1:9;
((-(arccos)*f1)`|Z).x=diff(-(arccos)*f1,x) by A7,A11,FDIFF_1:def 7
.=(-1)*diff((arccos)*f1,x) by A14,FDIFF_1:15
.=(-1)*(-diff(f1,x)/sqrt(1-(f1.x)^2)) by A12,A13,FDIFF_7:7
.=(-1)*(-(f1`|Z).x/sqrt(1-(f1.x)^2))
by A9,A11,FDIFF_1:def 7
.=(-1)*(-a/sqrt(1-(f1.x)^2)) by A3,A8,A11,FDIFF_1:23
.=a / sqrt(1-(a*x+b)^2) by A1,A11;
hence thesis;
end;
A15:for x being Element of REAL
st x in dom ((-(arccos)*f1)`|Z) holds ((-(arccos)*f1)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((-(arccos)*f1)`|Z);then
A16:x in Z by A7,FDIFF_1:def 7; then
((-(arccos)*f1)`|Z).x=a / sqrt(1-(a*x+b)^2) by A10
.=f.x by A1,A16;
hence thesis;
end;
dom((-(arccos)*f1)`|Z)=dom f by A1,A7,FDIFF_1:def 7;
then ((-(arccos)*f1)`|Z)= f by A15,PARTFUN1:5;
hence thesis by A1,A2,A7,INTEGRA5:13;
end;
::f.x=x*(1-x #Z 2) #R (-1/2)
theorem
A c= Z & f1=g-f2 & f2=#Z 2 & (for x st x in Z holds f.x=x*(1-x #Z 2) #R (-1/2)
& g.x=1 & f1.x >0) & Z c= dom (( #R (1/2))*f1)
& Z = dom f & f|A is continuous implies
integral(f,A)=(-( #R (1/2))*f1).(upper_bound A)
-(-( #R (1/2))*f1).(lower_bound A)
proof
assume
A1:A c= Z & f1=g-f2 & f2=#Z 2
& (for x st x in Z holds f.x=x*(1-x #Z 2) #R (-1/2)
& g.x=1 & f1.x >0) & Z c= dom (( #R (1/2))*f1)
& Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:for x st x in Z holds g.x=1 & f1.x >0 by A1;
A4:Z c= dom (-( #R (1/2))*f1) by A1,VALUED_1:8;
for y being object st y in Z holds y in dom f1 by A1,FUNCT_1:11;
then A5:Z c= dom ((g+(-1)(#)f2)) by A1;
A6:(( #R (1/2))*f1) is_differentiable_on Z by A1,A3,FDIFF_7:22;
then A7:(-1)(#)(( #R (1/2))*f1) is_differentiable_on Z by A4,FDIFF_1:20;
A8:f2=#Z 2 & for x st x in Z holds g.x=1+0*x by A1;
then A9:f1 is_differentiable_on Z &
for x st x in Z holds (f1`|Z).x =0+2*(-1)*x by A1,A5,FDIFF_4:12;
A10:for x st x in Z holds ((-( #R (1/2))*f1)`|Z).x =x*(1-x #Z 2) #R (-1/2)
proof
let x;
assume
A11:x in Z;then
A12:x in dom (g-f2) by A1,FUNCT_1:11;
A13:f1 is_differentiable_in x by A9,A11,FDIFF_1:9;
A14:(g-f2).x=g.x - f2.x by A12,VALUED_1:13
.=1 -(f2.x) by A1,A11
.=1 -(x #Z 2) by A1,TAYLOR_1:def 1; then
A15:f1.x = 1-x #Z 2 & f1.x >0 by A1,A11;
A16:( #R (1/2))*f1 is_differentiable_in x by A6,A11,FDIFF_1:9;
((-( #R (1/2))*f1)`|Z).x=diff((-( #R (1/2))*f1),x) by A7,A11,FDIFF_1:def 7
.=(-1)*diff((( #R (1/2))*f1),x) by A16,FDIFF_1:15
.=(-1)*((1/2)*((f1.x) #R (1/2-1)) * diff(f1,x))
by A13,A15,TAYLOR_1:22
.=(-1)*((1/2)*((f1.x) #R (1/2-1))*(f1`|Z).x) by A9,A11,FDIFF_1:def 7
.=(-1)*((1/2)*((f1.x) #R (1/2-1))*(0+2*(-1)*x))
by A1,A5,A8,A11,FDIFF_4:12
.=x*(1-x #Z 2) #R (-1/2) by A1,A14;
hence thesis;
end;
A17:for x being Element of REAL
st x in dom ((-( #R (1/2))*f1)`|Z) holds ((-( #R (1/2))*f1)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-( #R (1/2))*f1)`|Z);then
A18:x in Z by A7,FDIFF_1:def 7; then
((-( #R (1/2))*f1)`|Z).x=x*(1-x #Z 2) #R (-1/2) by A10
.=f.x by A1,A18;
hence thesis;
end;
dom((-( #R (1/2))*f1)`|Z)=dom f by A1,A7,FDIFF_1:def 7;
then((-( #R (1/2))*f1)`|Z) = f by A17,PARTFUN1:5;
hence thesis by A1,A2,A7,INTEGRA5:13;
end;
::f.x=x*(a^2-x #Z 2) #R (-1/2)
theorem
A c= Z & g=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f.x=x*((a^2-x #Z 2) #R (-1/2)) & f1.x=a^2 & g.x >0)
& Z c= dom (( #R (1/2))*g) & Z = dom f & f|A is continuous implies
integral(f,A)
=(-( #R (1/2))*g).(upper_bound A)-(-( #R (1/2))*g).(lower_bound A)
proof
assume
A1:A c= Z & g=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f.x=x*((a^2-x #Z 2) #R (-1/2)) & f1.x=a^2 & g.x >0)
& Z c= dom (( #R (1/2))*g) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:for x st x in Z holds f1.x=a^2 & g.x >0 by A1;
A4:Z c= dom (-( #R (1/2))*g) by A1,VALUED_1:8;
for y being object st y in Z holds y in dom g by A1,FUNCT_1:11;
then A5:Z c= dom ((f1+(-1)(#)f2)) by A1;
A6:(( #R (1/2))*g) is_differentiable_on Z by A1,A3,FDIFF_7:27;
then A7:(-1)(#)(( #R (1/2))*g) is_differentiable_on Z by A4,FDIFF_1:20;
A8:f2=#Z 2 & for x st x in Z holds f1.x=a^2+0*x by A1;
then A9:g is_differentiable_on Z &
for x st x in Z holds (g`|Z).x =0+2*(-1)*x by A1,A5,FDIFF_4:12;
A10:for x st x in Z holds ((-( #R (1/2))*g)`|Z).x = x*(a^2-x #Z 2) #R (-1/2)
proof
let x;
assume
A11:x in Z;then
A12:x in dom (f1-f2) by A1,FUNCT_1:11;
A13:g is_differentiable_in x by A9,A11,FDIFF_1:9;
A14:(f1-f2).x=f1.x - f2.x by A12,VALUED_1:13
.=a^2 -(f2.x) by A1,A11
.=a^2 -(x #Z 2) by A1,TAYLOR_1:def 1; then
A15:g.x = a^2-x #Z 2 & g.x >0 by A1,A11;
A16:( #R (1/2))*g is_differentiable_in x by A6,A11,FDIFF_1:9;
((-( #R (1/2))*g)`|Z).x = diff(-( #R (1/2))*g,x) by A7,A11,FDIFF_1:def 7
.=(-1)*diff(( #R (1/2))*g,x) by A16,FDIFF_1:15
.=(-1)*((1/2)*((g.x) #R (1/2-1)) * diff(g,x))
by A13,A15,TAYLOR_1:22
.=(-1)*((1/2)*((g.x) #R (1/2-1))*(g`|Z).x)
by A9,A11,FDIFF_1:def 7
.=(-1)*((1/2)*((g.x) #R (1/2-1))*(0+2*(-1)*x))
by A1,A5,A8,A11,FDIFF_4:12
.=x*(a^2-x #Z 2) #R (-1/2) by A1,A14;
hence thesis;
end;
A17:for x being Element of REAL
st x in dom ((-( #R (1/2))*g)`|Z) holds ((-( #R (1/2))*g)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-( #R (1/2))*g)`|Z);then
A18:x in Z by A7,FDIFF_1:def 7;then
((-( #R (1/2))*g)`|Z).x=x*(a^2-x #Z 2) #R (-1/2) by A10
.=f.x by A1,A18;
hence thesis;
end;
dom ((-( #R (1/2))*g)`|Z)=dom f by A1,A7,FDIFF_1:def 7;
then((-( #R (1/2))*g)`|Z)= f by A17,PARTFUN1:5;
hence thesis by A1,A2,A7,INTEGRA5:13;
end;
::f.x=cos.x/((sin.x) #Z (n+1))
theorem
A c= Z & n>0 & (for x st x in Z holds f.x=cos.x/((sin.x) #Z (n+1))
& sin.x<>0) & Z c= dom (( #Z n)*(sin^)) & Z =dom f
& f|A is continuous implies
integral(f,A)=((-1/n)(#)(( #Z n)*(sin^))).(upper_bound A)
-((-1/n)(#)(( #Z n)*(sin^))).(lower_bound A)
proof
assume
A1:A c= Z & n>0 & (for x st x in Z holds f.x=cos.x/((sin.x) #Z (n+1))
& sin.x<>0) & Z c= dom (( #Z n)*(sin^)) & Z =dom f
& f|A is continuous;
then A2:Z c= dom ((-1/n)(#)(( #Z n)*(sin^))) by VALUED_1:def 5;
A3:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A4:for x st x in Z holds sin.x<>0 by A1;then
A5:(-1/n)(#)(( #Z n)*(sin^)) is_differentiable_on Z by A1,A2,FDIFF_7:30;
A6:for x being Element of REAL st x in dom (((-1/n)(#)(( #Z n)*(sin^)))`|Z)
holds
(((-1/n)(#)(( #Z n)*(sin^)))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((-1/n)(#)(( #Z n)*(sin^)))`|Z);then
A7:x in Z by A5,FDIFF_1:def 7;then
(((-1/n)(#)(( #Z n)*(sin^)))`|Z).x=cos.x/((sin.x) #Z (n+1))
by A1,A2,A4,FDIFF_7:30
.=f.x by A1,A7;
hence thesis;
end;
dom (((-1/n)(#)(( #Z n)*(sin^)))`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then(((-1/n)(#)(( #Z n)*(sin^)))`|Z)= f by A6,PARTFUN1:5;
hence thesis by A1,A3,A5,INTEGRA5:13;
end;
::f.x=sin.x/((cos.x) #Z (n+1))
theorem
A c= Z & n>0 & (for x st x in Z holds f.x=sin.x/((cos.x) #Z (n+1))
& cos.x<>0) & Z c= dom (( #Z n)*(cos^)) & Z =dom f
& f|A is continuous implies
integral(f,A)=((1/n)(#)(( #Z n)*(cos^))).(upper_bound A)
-((1/n)(#)(( #Z n)*(cos^))).(lower_bound A)
proof
assume
A1:A c= Z & n>0 & (for x st x in Z holds f.x=sin.x/((cos.x) #Z (n+1))
& cos.x<>0) & Z c= dom (( #Z n)*(cos^)) & Z =dom f
& f|A is continuous;
then A2:Z c= dom ((1/n)(#)(( #Z n)*(cos^))) by VALUED_1:def 5;
A3:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A4:for x st x in Z holds cos.x<>0 by A1;then
A5:(1/n)(#)(( #Z n)*(cos^)) is_differentiable_on Z by A1,A2,FDIFF_7:31;
A6:for x being Element of REAL st x in dom (((1/n)(#)(( #Z n)*(cos^)))`|Z)
holds
(((1/n)(#)(( #Z n)*(cos^)))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((1/n)(#)(( #Z n)*(cos^)))`|Z);then
A7:x in Z by A5,FDIFF_1:def 7;then
(((1/n)(#)(( #Z n)*(cos^)))`|Z).x=sin.x/((cos.x) #Z (n+1))
by A1,A2,A4,FDIFF_7:31
.=f.x by A1,A7;
hence thesis;
end;
dom (((1/n)(#)(( #Z n)*(cos^)))`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then(((1/n)(#)(( #Z n)*(cos^)))`|Z)= f by A6,PARTFUN1:5;
hence thesis by A1,A3,A5,INTEGRA5:13;
end;
::f.x=1/((1+x^2)*arccot.x)
theorem
A c= Z & f = ((g1+g2)^)/f2 & f2 = arccot & Z c= ]. -1,1 .[ & g2=#Z 2
& (for x st x in Z holds f.x=1/((1+x^2)*arccot.x) & g1.x=1 & f2.x>0) &
Z = dom f implies
integral(f,A)=(-ln*arccot).(upper_bound A)-(-ln*arccot).(lower_bound A)
proof
assume
A1:A c= Z & f = ((g1+g2)^)/f2 & f2 = arccot & Z c= ]. -1,1 .[ & g2=#Z 2
& (for x st x in Z holds f.x=1/((1+x^2)*arccot.x) & g1.x=1
& f2.x>0) & Z = dom f;
then Z = dom ((g1+g2)^) /\ (dom f2 \ f2"{0}) by RFUNCT_1:def 1;
then A2: Z c= dom ((g1+g2)^) & Z c= dom f2 \ f2"{0} by XBOOLE_1:18;
for x st x in Z holds g1.x=1 by A1;
then A3: (g1+g2)^ is_differentiable_on Z by A1,A2,Th1;
A4: f2 is_differentiable_on Z by A1,SIN_COS9:82;
for x st x in Z holds f2.x<>0 by A1;
then f is_differentiable_on Z by A1,A3,A4,FDIFF_2:21;
then f|Z is continuous by FDIFF_1:25;
then A5:f|A is continuous by A1,FCONT_1:16;
A6:Z c= dom (f2^) by A2,RFUNCT_1:def 2;
dom (f2^) c= dom f2 by RFUNCT_1:1;then
A7:Z c= dom f2 by A6;
A8:for x st x in Z holds f2.x>0 by A1;
rng (f2|Z) c= right_open_halfline(0)
proof
let x be object;
assume x in rng (f2|Z); then
consider y be object such that
A9: y in dom (f2|Z) & x = (f2|Z).y by FUNCT_1:def 3;
y in Z by A9; then
f2.y > 0 by A1; then
(f2|Z).y > 0 by A9,FUNCT_1:47;
hence thesis by A9,XXREAL_1:235;
end;
then f2.:Z c= dom ln by RELAT_1:115,TAYLOR_1:18;
then A10:Z c= dom (ln*arccot) by A1,A7,FUNCT_1:101;
A11:f is_integrable_on A & f|A is bounded by A1,A5,INTEGRA5:10,11;
A12:ln*arccot is_differentiable_on Z by A1,A10,A8,SIN_COS9:90;
Z c= dom (-ln*arccot) by A10,VALUED_1:8;
then A13:-ln*arccot is_differentiable_on Z by A12,FDIFF_1:20;
A14:for x st x in Z holds ((-ln*arccot)`|Z).x = 1/((1+x^2)*arccot.x)
proof
let x;
assume
A15:x in Z;then
A16:-1 < x & x < 1 by A1,XXREAL_1:4;
arccot is_differentiable_on Z by A1,SIN_COS9:82;then
A17:arccot is_differentiable_in x by A15,FDIFF_1:9;
A18:arccot.x >0 by A1,A15;
A19:ln*arccot is_differentiable_in x by A12,A15,FDIFF_1:9;
((-ln*arccot)`|Z).x=diff((-ln*arccot),x) by A13,A15,FDIFF_1:def 7
.=(-1)*diff(ln*arccot,x) by A19,FDIFF_1:15
.=(-1)*(diff(arccot,x)/arccot.x) by A17,A18,TAYLOR_1:20
.=(-1)*((-1/(1+x^2))/arccot.x) by A16,SIN_COS9:76
.= (1/(1+x^2))/arccot.x
.= 1/((1+x^2)*arccot.x) by XCMPLX_1:78;
hence thesis;
end;
A20:for x being Element of REAL
st x in dom ((-ln*(arccot))`|Z) holds ((-ln*(arccot))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-ln*arccot)`|Z);then
A21:x in Z by A13,FDIFF_1:def 7;then
((-ln*(arccot))`|Z).x=1/((1+x^2)*arccot.x) by A14
.=f.x by A1,A21;
hence thesis;
end;
dom ((-ln*arccot)`|Z)=dom f by A1,A13,FDIFF_1:def 7;
then ((-ln*arccot)`|Z)= f by A20,PARTFUN1:5;
hence thesis by A1,A11,A13,INTEGRA5:13;
end;
::f.x=1 / (sqrt(1-x^2)*arcsin.x)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds
arcsin.x>0 & f1.x=1) & Z c= dom (ln*(arcsin)) & Z = dom f
& f=((( #R (1/2))*(f1-#Z 2))(#)arcsin)^ implies
integral(f,A)=(ln*(arcsin)).(upper_bound A)-(ln*(arcsin)).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds
arcsin.x>0 & f1.x=1) & Z c= dom (ln*(arcsin)) & Z = dom f
& f=((( #R (1/2))*(f1-#Z 2))(#)arcsin)^;
set g=((( #R (1/2))*(f1-#Z 2))(#)arcsin);
A2:Z c= dom g by A1,RFUNCT_1:1;
dom g = dom (( #R (1/2))*(f1-#Z 2)) /\ dom arcsin by VALUED_1:def 4;
then
A3:Z c= dom (( #R (1/2))*(f1-#Z 2)) & Z c= dom arcsin by A2,XBOOLE_1:18;
A4:arcsin is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:83;
set f2=#Z 2;
for x st x in Z holds (f1-#Z 2).x >0
proof
let x;
assume
A5:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A6:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f1-f2) by A3,FUNCT_1:11;
then (f1-f2).x = f1.x - f2.x by A5,VALUED_1:13
.=f1.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f1.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f1.x - (x*(x #Z 1)) by PREPOWER:35
.=f1.x - x*x by PREPOWER:35
.=1 - x*x by A1,A5;
hence thesis by A6;
end;
then for x st x in Z holds f1.x=1 & (f1-#Z 2).x >0 by A1;
then (( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z by A3,FDIFF_7:22;
then A7:g is_differentiable_on Z by A2,A4,FDIFF_1:21;
for x st x in Z holds g.x<>0 by A1,RFUNCT_1:3;
then f is_differentiable_on Z by A1,A7,FDIFF_2:22;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A8:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A9:for x st x in Z holds arcsin.x>0 by A1;
then A10:ln*arcsin is_differentiable_on Z by A1,FDIFF_7:8;
A11:for x st x in Z holds f.x=1 / (sqrt(1-x^2)*arcsin.x)
proof
let x;
assume
A12:x in Z;
then
A13:x in dom (f1-#Z 2) & (f1-#Z 2).x in dom ( #R (1/2)) by A3,FUNCT_1:11;
then A14:(f1-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A12,XXREAL_1:4;
then 0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A15:0 < (1+x)*(1-x) by XREAL_1:129;
(((( #R (1/2))*(f1-#Z 2))(#)arcsin)^).x
=1/(((( #R (1/2))*(f1-#Z 2))(#)arcsin).x) by A1,A12,RFUNCT_1:def 2
.=1/((( #R (1/2))*(f1-#Z 2)).x*arcsin.x) by VALUED_1:5
.=1/(( #R (1/2)).((f1-#Z 2).x)*arcsin.x) by A3,A12,FUNCT_1:12
.=1/((((f1-#Z 2).x) #R (1/2))*arcsin.x) by A14,TAYLOR_1:def 4
.=1/(((f1.x-(( #Z 2).x)) #R (1/2))*arcsin.x) by A13,VALUED_1:13
.=1/(((f1.x-(x #Z 2)) #R (1/2))*arcsin.x) by TAYLOR_1:def 1
.=1/(((f1.x-x^2) #R (1/2))*arcsin.x) by FDIFF_7:1
.=1/(((1-x^2) #R (1/2))*arcsin.x) by A1,A12
.=1/(sqrt(1-x^2)*arcsin.x) by A15,FDIFF_7:2;
hence thesis by A1;
end;
A16:for x being Element of REAL
st x in dom (ln*(arcsin)`|Z) holds (ln*(arcsin)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (ln*(arcsin)`|Z);then
A17: x in Z by A10,FDIFF_1:def 7; then
(ln*(arcsin)`|Z).x=1 / (sqrt(1-x^2)*arcsin.x) by A1,A9,FDIFF_7:8
.=f.x by A11,A17;
hence thesis;
end;
dom (ln*(arcsin)`|Z)=dom f by A1,A10,FDIFF_1:def 7;
then (ln*(arcsin)`|Z)= f by A16,PARTFUN1:5;
hence thesis by A1,A8,A10,INTEGRA5:13;
end;
::f.x=1 / (sqrt(1-x^2)*arccos.x)
theorem
A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f1.x=1
& arccos.x>0) & Z c= dom (ln*arccos) & Z = dom f &
f=((( #R (1/2))*(f1-#Z 2))(#)arccos)^ implies
integral(f,A)=(-ln*arccos).(upper_bound A)-(-ln*arccos).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds
f1.x=1 & arccos.x>0) & Z c= dom (ln*arccos) & Z = dom f &
f=((( #R (1/2))*(f1-#Z 2))(#)arccos)^;
set g=((( #R (1/2))*(f1-#Z 2))(#)arccos);
A2:Z c= dom g by A1,RFUNCT_1:1;
dom g = dom (( #R (1/2))*(f1-#Z 2)) /\ dom arccos by VALUED_1:def 4;
then
A3:Z c= dom (( #R (1/2))*(f1-#Z 2)) & Z c= dom arccos by A2,XBOOLE_1:18;
A4:arccos is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:106;
set f2=#Z 2;
for x st x in Z holds (f1-#Z 2).x >0
proof
let x;
assume
A5:x in Z; then
-1 < x & x < 1 by A1,XXREAL_1:4; then
0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A6:0 < (1+x)*(1-x) by XREAL_1:129;
for x st x in Z holds x in dom (f1-f2) by A3,FUNCT_1:11;
then (f1-f2).x = f1.x - f2.x by A5,VALUED_1:13
.=f1.x - (x #Z (1+1)) by TAYLOR_1:def 1
.=f1.x - ((x #Z 1)*(x #Z 1)) by TAYLOR_1:1
.=f1.x - (x*(x #Z 1)) by PREPOWER:35
.=f1.x - x*x by PREPOWER:35
.=1 - x*x by A1,A5;
hence thesis by A6;
end;
then for x st x in Z holds f1.x=1 & (f1-#Z 2).x >0 by A1;
then (( #R (1/2))*(f1-#Z 2)) is_differentiable_on Z by A3,FDIFF_7:22;
then A7:g is_differentiable_on Z by A2,A4,FDIFF_1:21;
for x st x in Z holds g.x<>0 by A1,RFUNCT_1:3;
then f is_differentiable_on Z by A1,A7,FDIFF_2:22;
then f|Z is continuous by FDIFF_1:25;then
f|A is continuous by A1,FCONT_1:16;
then A8:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
for x st x in Z holds arccos.x>0 by A1;
then A9:ln*arccos is_differentiable_on Z by A1,FDIFF_7:9;
Z c= dom (-ln*arccos) by A1,VALUED_1:8;
then A10:(-1)(#)(ln*arccos) is_differentiable_on Z by A9,FDIFF_1:20;
A11:for x st x in Z holds ((-ln*arccos)`|Z).x = 1 / (sqrt(1-x^2)*arccos.x)
proof
let x;
assume
A12:x in Z;then
A13:-1 < x & x < 1 by A1,XXREAL_1:4;
A14:arccos is_differentiable_in x by A1,A12,FDIFF_1:9,SIN_COS6:106;
A15:arccos.x >0 by A1,A12;
A16:ln*arccos is_differentiable_in x by A9,A12,FDIFF_1:9;
((-ln*arccos)`|Z).x=diff(-ln*(arccos),x) by A10,A12,FDIFF_1:def 7
.=(-1)*diff(ln*arccos,x) by A16,FDIFF_1:15
.=(-1)*(diff(arccos,x)/arccos.x) by A14,A15,TAYLOR_1:20
.=(-1)*((-1 / sqrt(1-x^2))/arccos.x) by A13,SIN_COS6:106
.=(-1)*(-(1 / sqrt(1-x^2))/arccos.x)
.=1 / (sqrt(1-x^2)*arccos.x) by XCMPLX_1:78;
hence thesis;
end;
A17:for x st x in Z holds f.x=1 / (sqrt(1-x^2)*arccos.x)
proof
let x;
assume
A18:x in Z;
then
A19:x in dom (f1-#Z 2) & (f1-#Z 2).x in dom ( #R (1/2)) by A3,FUNCT_1:11;
then A20:(f1-#Z 2).x in right_open_halfline(0) by TAYLOR_1:def 4;
-1 < x & x < 1 by A1,A18,XXREAL_1:4;
then 0 < 1+x & 0 < 1-x by XREAL_1:50,148; then
A21:0 < (1+x)*(1-x) by XREAL_1:129;
(((( #R (1/2))*(f1-#Z 2))(#)arccos)^).x
=1/(((( #R (1/2))*(f1-#Z 2))(#)arccos).x) by A1,A18,RFUNCT_1:def 2
.=1/((( #R (1/2))*(f1-#Z 2)).x*arccos.x) by VALUED_1:5
.=1/(( #R (1/2)).((f1-#Z 2).x)*arccos.x) by A3,A18,FUNCT_1:12
.=1/((((f1-#Z 2).x) #R (1/2))*arccos.x) by A20,TAYLOR_1:def 4
.=1/(((f1.x-(( #Z 2).x)) #R (1/2))*arccos.x) by A19,VALUED_1:13
.=1/(((f1.x-(x #Z 2)) #R (1/2))*arccos.x) by TAYLOR_1:def 1
.=1/(((f1.x-x^2) #R (1/2))*arccos.x) by FDIFF_7:1
.=1/(((1-x^2) #R (1/2))*arccos.x) by A1,A18
.=1/(sqrt(1-x^2)*arccos.x) by A21,FDIFF_7:2;
hence thesis by A1;
end;
A22:for x being Element of REAL
st x in dom ((-ln*arccos)`|Z) holds ((-ln*arccos)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-ln*arccos)`|Z);then
A23: x in Z by A10,FDIFF_1:def 7; then
((-ln*arccos)`|Z).x=1 / (sqrt(1-x^2)*arccos.x) by A11
.=f.x by A17,A23;
hence thesis;
end;
dom ((-ln*arccos)`|Z)=dom f by A1,A10,FDIFF_1:def 7;
then ((-ln*arccos)`|Z)= f by A22,PARTFUN1:5;
hence thesis by A1,A8,A10,INTEGRA5:13;
end;