:: Integrability Formulas -- Part {II}
:: by Bo Li , Na Ma and Xiquan Liang
::
:: Received February 4, 2010
:: Copyright (c) 2010-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, LIMFUNC1, PARTFUN1,
TAYLOR_1, SIN_COS9, SUBSET_1, TARSKI, NUMBERS, REAL_1, CARD_1, INTEGRA5,
XXREAL_2, ORDINAL4, VALUED_1, XXREAL_1, XXREAL_0, SEQ_4, MEASURE5;
notations TARSKI, XBOOLE_0, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1,
XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1,
PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5,
PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, SIN_COS4, SIN_COS9, LIMFUNC1, SEQ_4;
constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER,
INTEGRA5, SEQ_4, SIN_COS9, PARTFUN2, RFUNCT_1, SIN_COS4, LIMFUNC1,
RELSET_1, INTEGRA1, COMSEQ_2, COMPLEX1, BINOP_2;
registrations NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, RCOMP_1, RELSET_1,
MEASURE5, XREAL_0, SQUARE_1, PREPOWER;
requirements NUMERALS, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities SIN_COS, VALUED_1, SQUARE_1, SIN_COS4, LIMFUNC1, XCMPLX_0;
expansions TARSKI;
theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, XCMPLX_1, INTEGRA5, SIN_COS,
TAYLOR_1, VALUED_1, XREAL_0, XBOOLE_0, XXREAL_1, XBOOLE_1, FDIFF_5,
FDIFF_7, FDIFF_8, SIN_COS9, PREPOWER, TARSKI, RELAT_1, FDIFF_2;
begin
reserve a,x for Real;
reserve n for Element of NAT;
reserve A for non empty closed_interval Subset of REAL;
reserve f,h,f1,f2 for PartFunc of REAL,REAL;
reserve Z for open Subset of REAL;
Lm1:
0 in Z implies (id Z)"{0} = {0}
proof
assume A1: 0 in Z;
thus (id Z)"{0} c= {0}
proof
let x be object; assume
A2: x in (id Z)"{0};
then x in dom id Z by FUNCT_1:def 7; then
A3: x in Z;
(id Z).x in {0} by A2,FUNCT_1:def 7;
hence thesis by A3,FUNCT_1:18;
end;
let x be object; assume x in {0}; then
A4: x = 0 by TARSKI:def 1; then
(id Z).x = 0 by A1,FUNCT_1:18; then
A5: (id Z).x in {0} by TARSKI:def 1;
x in dom id Z by A1,A4;
hence thesis by A5,FUNCT_1:def 7;
end;
Lm2: right_open_halfline 0 = {g where g is Real: 0<g} by XXREAL_1:230;
:: f.x = 1/(sin.x*cos.x)
theorem
A c= Z & f=(sin(#)cos)^ & Z c= dom (ln*tan) & Z = dom f & f|A is continuous
implies integral(f,A)=(ln*tan).(upper_bound A)-(ln*tan).(lower_bound A)
proof
assume
A1: A c= Z & f=(sin(#)cos)^
& Z c= dom (ln*tan) & Z = dom f & f|A is continuous;then
A2: f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3: (ln*tan) is_differentiable_on Z by A1,FDIFF_8:18;
A4:for x st x in Z holds f.x=1/(sin.x*cos.x)
proof
let x;
assume x in Z;
then ((sin(#)cos)^).x =1/((sin(#)cos).x) by A1,RFUNCT_1:def 2
.=1/(sin.x*cos.x) by VALUED_1:5;
hence thesis by A1;
end;
A5: for x being Element of REAL
st x in dom ((ln*tan)`|Z) holds ((ln*tan)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((ln*tan)`|Z);then
A6: x in Z by A3,FDIFF_1:def 7; then
((ln*tan)`|Z).x = 1/(sin.x*cos.x) by A1,FDIFF_8:18
.=f.x by A4,A6;
hence thesis;
end;
dom ((ln*tan)`|Z) = dom f by A1,A3,FDIFF_1:def 7;then
((ln*tan)`|Z)=f by A5,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:18,INTEGRA5:13;
end;
:: f.x = -1/(sin.x*cos.x)
theorem
A c= Z & f=-(sin(#)cos)^ & Z c= dom (ln*cot) & Z = dom f & f|A is continuous
implies integral(f,A)=(ln*cot).(upper_bound A)-(ln*cot).(lower_bound A)
proof
assume
A1:A c= Z & f=-(sin(#)cos)^
& Z c= dom (ln*cot) & Z = dom f & f|A is continuous;then
A2: f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3: (ln*cot) is_differentiable_on Z by A1,FDIFF_8:19;
A4:Z = dom ((sin(#)cos)^) by A1,VALUED_1:8;
A5:for x st x in Z holds f.x=-1/(sin.x*cos.x)
proof
let x;
assume
A6:x in Z;
(-(sin(#)cos)^).x=-(((sin(#)cos)^).x) by VALUED_1:8
.=-1/((sin(#)cos).x) by A4,A6,RFUNCT_1:def 2
.=-1/(sin.x*cos.x) by VALUED_1:5;
hence thesis by A1;
end;
A7: for x being Element of REAL
st x in dom ((ln*cot)`|Z) holds ((ln*cot)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((ln*cot)`|Z);then
A8: x in Z by A3,FDIFF_1:def 7; then
((ln*cot)`|Z).x = -1/(sin.x*cos.x) by A1,FDIFF_8:19
.=f.x by A5,A8;
hence thesis;
end;
dom ((ln*cot)`|Z) = dom f by A1,A3,FDIFF_1:def 7;then
((ln*cot)`|Z)=f by A7,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:19,INTEGRA5:13;
end;
::f.x=2 * exp_R.x * sin.x
theorem
A c= Z & f=2(#)(exp_R(#)sin)
& Z c= dom (exp_R(#)(sin-cos)) & Z = dom f & f|A is continuous implies
integral(f,A)=(exp_R(#)(sin-cos)).(upper_bound A)-
(exp_R(#)(sin-cos)).(lower_bound A)
proof
assume
A1:A c= Z & f=2(#)(exp_R(#)sin)
& Z c= dom (exp_R(#)(sin-cos)) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)(sin-cos) is_differentiable_on Z by A1,FDIFF_7:40;
A4:for x st x in Z holds f.x=2 * exp_R.x * sin.x
proof
let x;
assume x in Z;
(2(#)(exp_R(#)sin)).x=2*(exp_R(#)sin).x by VALUED_1:6
.=2*(exp_R.x * sin.x) by VALUED_1:5;
hence thesis by A1;
end;
A5:for x being Element of REAL
st x in dom ((exp_R(#)(sin-cos))`|Z) holds
((exp_R(#)(sin-cos))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((exp_R(#)(sin-cos))`|Z);then
A6:x in Z by A3,FDIFF_1:def 7;then
((exp_R(#)(sin-cos))`|Z).x=2 * exp_R.x * sin.x by A1,FDIFF_7:40
.=f.x by A4,A6;
hence thesis;
end;
dom ((exp_R(#)(sin-cos))`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((exp_R(#)(sin-cos))`|Z)= f by A5,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_7:40,INTEGRA5:13;
end;
::f.x=2 * exp_R.x * cos.x
theorem
A c= Z & f=2(#)(exp_R(#)cos)
& Z c= dom (exp_R(#)(sin+cos)) & Z = dom f & f|A is continuous implies
integral(f,A)=(exp_R(#)(sin+cos)).(upper_bound A)-
(exp_R(#)(sin+cos)).(lower_bound A)
proof
assume
A1:A c= Z & f=2(#)(exp_R(#)cos)
& Z c= dom (exp_R(#)(sin+cos)) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)(sin+cos) is_differentiable_on Z by A1,FDIFF_7:41;
A4:for x st x in Z holds f.x=2 * exp_R.x * cos.x
proof
let x;
assume x in Z;
(2(#)(exp_R(#)cos)).x=2*(exp_R(#)cos).x by VALUED_1:6
.=2*(exp_R.x * cos.x) by VALUED_1:5;
hence thesis by A1;
end;
A5:for x being Element of REAL
st x in dom ((exp_R(#)(sin+cos))`|Z) holds
((exp_R(#)(sin+cos))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((exp_R(#)(sin+cos))`|Z);then
A6:x in Z by A3,FDIFF_1:def 7;then
((exp_R(#)(sin+cos))`|Z).x=2 * exp_R.x * cos.x by A1,FDIFF_7:41
.=f.x by A6,A4;
hence thesis;
end;
dom ((exp_R(#)(sin+cos))`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((exp_R(#)(sin+cos))`|Z)= f by A5,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_7:41,INTEGRA5:13;
end;
::f.x=cos.x-sin.x
theorem
A c= Z & Z = dom (cos-sin) & (cos-sin)|A is continuous implies
integral(cos-sin,A)=(sin+cos).(upper_bound A)-(sin+cos).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom (cos-sin) & (cos-sin)|A is continuous;then
A2:cos-sin is_integrable_on A & (cos-sin)|A is bounded by INTEGRA5:10,11;
Z = dom cos /\ dom sin by A1,VALUED_1:12;then
A3:Z c= dom (sin+cos) by VALUED_1:def 1;
then A4:sin+cos is_differentiable_on Z by FDIFF_7:38;
A5:for x being Element of REAL
st x in dom ((sin+cos)`|Z) holds ((sin+cos)`|Z).x=(cos-sin).x
proof
let x be Element of REAL;
assume x in dom((sin+cos)`|Z);then
A6:x in Z by A4,FDIFF_1:def 7;
then ((sin+cos)`|Z).x=cos.x-sin.x by A3,FDIFF_7:38
.=(cos-sin).x by A1,A6,VALUED_1:13;
hence thesis;
end;
dom((sin+cos)`|Z)=dom (cos-sin) by A1,A4,FDIFF_1:def 7;
then((sin+cos)`|Z)=(cos-sin) by A5,PARTFUN1:5;
hence thesis by A1,A2,A3,FDIFF_7:38,INTEGRA5:13;
end;
::f.x=cos.x+sin.x
theorem
A c= Z & Z = dom (cos+sin) & (cos+sin)|A is continuous implies
integral(cos+sin,A)=(sin-cos).(upper_bound A)-(sin-cos).(lower_bound A)
proof
assume
A1:A c= Z & Z = dom (cos+sin) & (cos+sin)|A is continuous;then
A2:cos+sin is_integrable_on A & (cos+sin)|A is bounded by INTEGRA5:10,11;
Z = dom cos /\ dom sin by A1,VALUED_1:def 1;then
A3:Z c= dom (sin-cos) by VALUED_1:12;
then A4:sin-cos is_differentiable_on Z by FDIFF_7:39;
A5:for x being Element of REAL
st x in dom ((sin-cos)`|Z) holds ((sin-cos)`|Z).x=(cos+sin).x
proof
let x be Element of REAL;
assume x in dom((sin-cos)`|Z);then
A6:x in Z by A4,FDIFF_1:def 7;
then ((sin-cos)`|Z).x=cos.x+sin.x by A3,FDIFF_7:39
.=(cos+sin).x by A1,A6,VALUED_1:def 1;
hence thesis;
end;
dom((sin-cos)`|Z)=dom (cos+sin) by A1,A4,FDIFF_1:def 7;
then((sin-cos)`|Z)= (cos+sin) by A5,PARTFUN1:5;
hence thesis by A1,A2,A3,FDIFF_7:39,INTEGRA5:13;
end;
theorem Th7:
Z c= dom ((-1/2)(#)((sin+cos)/exp_R)) implies
(-1/2)(#)((sin+cos)/exp_R) is_differentiable_on Z &
for x st x in Z holds (((-1/2)(#)((sin+cos)/exp_R))`|Z).x = sin.x/exp_R.x
proof
assume
A1:Z c= dom ((-1/2)(#)((sin+cos)/exp_R));
then A2:Z c= dom ((sin+cos)/exp_R) by VALUED_1:def 5;then
Z c= dom (sin+cos) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then A3:Z c= dom (sin+cos) by XBOOLE_1:18; then
A4:sin+cos is_differentiable_on Z &
for x st x in Z holds ((sin+cos)`|Z).x =cos.x-sin.x by FDIFF_7:38;
A5:(sin+cos)/exp_R is_differentiable_on Z by A2,FDIFF_7:42;then
A6:(-1/2)(#)((sin+cos)/exp_R) is_differentiable_on Z by FDIFF_2:19;
for x st x in Z holds ((((-1/2)(#)((sin+cos)/exp_R)))`|Z).x =sin.x/exp_R.x
proof
let x;
A7: x in REAL by XREAL_0:def 1;
assume
A8: x in Z;
A9: exp_R is_differentiable_in x by SIN_COS:65;
A10:sin+cos is_differentiable_in x by A4,A8,FDIFF_1:9;
A11:(sin+cos).x=sin.x+cos.x by VALUED_1:1,A7;
A12:exp_R.x <>0 by SIN_COS:54;
(((-1/2)(#)((sin+cos)/exp_R))`|Z).x=(-1/2)*(diff((sin+cos)/exp_R,x))
by A1,A5,A8,FDIFF_1:20
.=(-1/2)*((diff(sin+cos,x) * exp_R.x
- diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2) by A9,A10,A12,FDIFF_2:14
.=(-1/2)*((((sin+cos)`|Z).x* exp_R.x
- diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2) by A4,A8,FDIFF_1:def 7
.=(-1/2)*(((cos.x-sin.x)* exp_R.x
- diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2) by A3,A8,FDIFF_7:38
.=(-1/2)*(((cos.x-sin.x)* exp_R.x
- exp_R.x*(sin.x+cos.x))/(exp_R.x)^2) by A11,SIN_COS:65
.=(-1/2)*((-2*sin.x)*(exp_R.x/((exp_R.x)*(exp_R.x))))
.=(-1/2)*((-2*sin.x)*((exp_R.x)/(exp_R.x)/(exp_R.x))) by XCMPLX_1:78
.=(-1/2)*((-2*sin.x)*(1/exp_R.x)) by A12,XCMPLX_1:60
.=sin.x/exp_R.x;
hence thesis;
end;
hence thesis by A6;
end;
::f.x=sin.x/exp_R.x
theorem
A c= Z & f=sin/exp_R
& Z c= dom ((-1/2)(#)((sin+cos)/exp_R)) & Z = dom f & f|A is continuous
implies integral(f,A)=((-1/2)(#)((sin+cos)/exp_R)).(upper_bound A)
-((-1/2)(#)((sin+cos)/exp_R)).(lower_bound A)
proof
assume
A1:A c= Z & f=sin/exp_R
& Z c= dom ((-1/2)(#)((sin+cos)/exp_R)) & Z = dom f & f|A is continuous;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(-1/2)(#)((sin+cos)/exp_R) is_differentiable_on Z by A1,Th7;
A4:for x st x in Z holds f.x=sin.x/exp_R.x by A1,RFUNCT_1:def 1;
A5:for x being Element of REAL
st x in dom (((-1/2)(#)((sin+cos)/exp_R))`|Z) holds
(((-1/2)(#)((sin+cos)/exp_R))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((-1/2)(#)((sin+cos)/exp_R))`|Z);then
A6:x in Z by A3,FDIFF_1:def 7;then
(((-1/2)(#)((sin+cos)/exp_R))`|Z).x=sin.x/exp_R.x by A1,Th7
.=f.x by A6,A4;
hence thesis;
end;
dom (((-1/2)(#)((sin+cos)/exp_R))`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then (((-1/2)(#)((sin+cos)/exp_R))`|Z)= f by A5,PARTFUN1:5;
hence thesis by A1,A2,Th7,INTEGRA5:13;
end;
theorem Th9:
Z c= dom ((1/2)(#)((sin-cos)/exp_R)) implies
(1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z &
for x st x in Z holds (((1/2)(#)((sin-cos)/exp_R))`|Z).x =cos.x/exp_R.x
proof
assume
A1:Z c= dom ((1/2)(#)((sin-cos)/exp_R));
then A2:Z c= dom ((sin-cos)/exp_R) by VALUED_1:def 5;then
Z c= dom (sin-cos) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then A3:Z c= dom (sin-cos) by XBOOLE_1:18; then
A4:sin-cos is_differentiable_on Z &
for x st x in Z holds ((sin-cos)`|Z).x =cos.x+sin.x by FDIFF_7:39;
A5:(sin-cos)/exp_R is_differentiable_on Z by A2,FDIFF_7:43;then
A6:(1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z by FDIFF_2:19;
for x st x in Z holds (((1/2)(#)((sin-cos)/exp_R))`|Z).x =cos.x/exp_R.x
proof
let x;
assume
A7:x in Z;
A8:exp_R is_differentiable_in x by SIN_COS:65;
A9:sin-cos is_differentiable_in x by A4,A7,FDIFF_1:9;
A10:(sin-cos).x=sin.x-cos.x by A3,A7,VALUED_1:13;
A11:exp_R.x <>0 by SIN_COS:54;
(((1/2)(#)((sin-cos)/exp_R))`|Z).x=(1/2)*(diff((sin-cos)/exp_R,x))
by A1,A5,A7,FDIFF_1:20
.=(1/2)*((diff(sin-cos,x) * exp_R.x
- diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2) by A8,A9,A11,FDIFF_2:14
.=(1/2)*((((sin-cos)`|Z).x* exp_R.x
- diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2) by A4,A7,FDIFF_1:def 7
.=(1/2)*(((cos.x+sin.x)* exp_R.x
- diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2) by A3,A7,FDIFF_7:39
.=(1/2)*(((cos.x+sin.x)* exp_R.x
- exp_R.x*(sin.x-cos.x))/(exp_R.x)^2) by A10,SIN_COS:65
.=(1/2)*((2*cos.x)*(exp_R.x/((exp_R.x)*(exp_R.x))))
.=(1/2)*((2*cos.x)*((exp_R.x)/(exp_R.x)/(exp_R.x))) by XCMPLX_1:78
.=(1/2)*((2*cos.x)*(1/exp_R.x)) by A11,XCMPLX_1:60
.=cos.x/exp_R.x;
hence thesis;
end;
hence thesis by A6;
end;
::f.x=cos.x/exp_R.x
theorem
A c= Z & f=cos/exp_R
& Z c= dom ((1/2)(#)((sin-cos)/exp_R)) & Z = dom f & f|A is continuous
implies integral(f,A)=((1/2)(#)((sin-cos)/exp_R)).(upper_bound A)
-((1/2)(#)((sin-cos)/exp_R)).(lower_bound A)
proof
assume
A1:A c= Z & f=cos/exp_R
& Z c= dom ((1/2)(#)((sin-cos)/exp_R)) & Z = dom f & f|A is continuous;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z by A1,Th9;
A4:for x st x in Z holds f.x=cos.x/exp_R.x by A1,RFUNCT_1:def 1;
A5:for x being Element of REAL
st x in dom (((1/2)(#)((sin-cos)/exp_R))`|Z) holds
(((1/2)(#)((sin-cos)/exp_R))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((1/2)(#)((sin-cos)/exp_R))`|Z);then
A6:x in Z by A3,FDIFF_1:def 7;then
(((1/2)(#)((sin-cos)/exp_R))`|Z).x=cos.x/exp_R.x by A1,Th9
.=f.x by A4,A6;
hence thesis;
end;
dom (((1/2)(#)((sin-cos)/exp_R))`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then (((1/2)(#)((sin-cos)/exp_R))`|Z)= f by A5,PARTFUN1:5;
hence thesis by A1,A2,Th9,INTEGRA5:13;
end;
::f.x=exp_R.x*(sin.x+cos.x)
theorem
A c= Z & f=exp_R(#)(sin+cos)
& Z c= dom (exp_R(#)sin) & Z = dom f & f|A is continuous implies
integral(f,A)=(exp_R(#)sin).(upper_bound A)-(exp_R(#)sin).(lower_bound A)
proof
assume
A1:A c= Z & f=exp_R(#)(sin+cos)
& Z c= dom (exp_R(#)sin) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)sin is_differentiable_on Z by A1,FDIFF_7:44;
dom f = dom exp_R /\ dom (sin+cos) by A1,VALUED_1:def 4;then
A4:Z c= dom (sin+cos) by A1,XBOOLE_1:18;
A5:for x st x in Z holds f.x=exp_R.x*(sin.x+cos.x)
proof
let x;
assume
A6:x in Z;
(exp_R(#)(sin+cos)).x=exp_R.x*((sin+cos).x) by VALUED_1:5
.=exp_R.x*(sin.x+cos.x) by A4,A6,VALUED_1:def 1;
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.x*(sin.x+cos.x) by A1,FDIFF_7:44
.=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,FDIFF_7:44,INTEGRA5:13;
end;
::f.x=exp_R.x*(cos.x-sin.x)
theorem
A c= Z & f=exp_R(#)(cos-sin)
& Z c= dom (exp_R(#)cos) & Z = dom f & f|A is continuous implies
integral(f,A)=(exp_R(#)cos).(upper_bound A)-(exp_R(#)cos).(lower_bound A)
proof
assume
A1:A c= Z & f=exp_R(#)(cos-sin)
& Z c= dom (exp_R(#)cos) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)cos is_differentiable_on Z by A1,FDIFF_7:45;
dom f = dom exp_R /\ dom (cos-sin) by A1,VALUED_1:def 4;then
A4:Z c= dom (cos-sin) by A1,XBOOLE_1:18;
A5:for x st x in Z holds f.x=exp_R.x*(cos.x-sin.x)
proof
let x;
assume
A6:x in Z;
(exp_R(#)(cos-sin)).x=exp_R.x*((cos-sin).x) by VALUED_1:5
.=exp_R.x*(cos.x-sin.x) by A4,A6,VALUED_1:13;
hence thesis by A1;
end;
A7: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
A8:x in Z by A3,FDIFF_1:def 7;then
((exp_R(#)cos)`|Z).x=exp_R.x*(cos.x-sin.x) by A1,FDIFF_7:45
.=f.x by A5,A8;
hence thesis;
end;
dom ((exp_R(#)cos)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((exp_R(#)cos)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_7:45,INTEGRA5:13;
end;
::f.x=-sin.x/cos.x/x^2+1/x/(cos.x)^2
theorem
A c= Z & f1=#Z 2 & f=-sin/cos/f1 + (id Z)^/cos^2
& Z c= dom ((id Z)^(#)tan) & Z = dom f & f|A is continuous implies
integral(f,A)=((id Z)^(#)tan).(upper_bound A)-((id Z)^(#)tan).(lower_bound A)
proof
assume
A1:A c= Z & f1=#Z 2 & f= -sin/cos/f1 + (id Z)^/cos^2
& Z c= dom ((id Z)^(#)tan) & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
set g = id Z;
Z c= dom (g^) /\ dom tan by A1,VALUED_1:def 4;
then A3:Z c= dom (g^) by XBOOLE_1:18;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then
A6:(id Z)^(#)tan is_differentiable_on Z by A1,FDIFF_8:34;
dom f = dom (-sin/cos/f1) /\ dom ((id Z)^/cos^2) by A1,VALUED_1:def 1;then
dom f c= dom (-sin/cos/f1) & dom f c= dom ((id Z)^/cos^2) by XBOOLE_1:18;
then A7:Z c= dom (sin/cos/f1) & Z c= dom ((id Z)^/cos^2) by A1,VALUED_1:8;
dom (sin/cos/f1) = dom (sin/cos) /\ (dom f1 \ f1"{0}) by RFUNCT_1:def 1;then
A8:Z c= dom (sin/cos) by A7,XBOOLE_1:18;
dom ((id Z)^/cos^2) c= dom ((id Z)^) /\ (dom (cos^2) \ (cos^2)"{0})
by RFUNCT_1:def 1;then
dom ((id Z)^/cos^2) c= dom ((id Z)^)
& dom ((id Z)^/cos^2) c= dom (cos^2) \ (cos^2)"{0} by XBOOLE_1:18;then
A9:Z c= dom ((id Z)^) & Z c= dom (cos^2) \ (cos^2)"{0} by A7;
A10:for x st x in Z holds f.x=-sin.x/cos.x/x^2+1/x/(cos.x)^2
proof
let x;
assume
A11:x in Z;then
(-sin/cos/f1 + (id Z)^/cos^2).x
=(-sin/cos/f1).x+((id Z)^/cos^2).x by A1,VALUED_1:def 1
.=-(sin/cos/f1).x+((id Z)^/cos^2).x by VALUED_1:8
.=-((sin/cos).x/f1.x)+((id Z)^/cos^2).x by A11,A7,RFUNCT_1:def 1
.=-((sin.x*(cos.x)")/f1.x)+((id Z)^/cos^2).x by A8,A11,RFUNCT_1:def 1
.=-sin.x/cos.x/f1.x+((id Z)^).x/(cos^2).x by A7,A11,RFUNCT_1:def 1
.=-sin.x/cos.x/f1.x+(((id Z).x)")/(cos^2).x by A9,A11,RFUNCT_1:def 2
.=-sin.x/cos.x/f1.x+1/x/(cos^2).x by A11,FUNCT_1:18
.=-sin.x/cos.x/f1.x+1/x/(cos.x)^2 by VALUED_1:11
.=-sin.x/cos.x/(x #Z 2)+1/x/(cos.x)^2 by A1,TAYLOR_1:def 1
.=-sin.x/cos.x/x^2+1/x/(cos.x)^2 by FDIFF_7:1;
hence thesis by A1;
end;
A12:for x being Element of REAL
st x in dom(((id Z)^(#)tan)`|Z) holds (((id Z)^(#)tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)^(#)tan)`|Z);then
A13:x in Z by A6,FDIFF_1:def 7;then
(((id Z)^(#)tan)`|Z).x=-sin.x/cos.x/x^2+1/x/(cos.x)^2 by A4,A1,FDIFF_8:34
.=f.x by A13,A10;
hence thesis;
end;
dom(((id Z)^(#)tan)`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then(((id Z)^(#)tan)`|Z)= f by A12,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
::f.x=-cos.x/sin.x/x^2-1/x/(sin.x)^2
theorem
A c= Z & f=-cos/sin/f1-(id Z)^/sin^2 & f1=#Z 2
& Z c= dom ((id Z)^(#)cot) & Z = dom f & f|A is continuous
implies
integral(f,A)=((id Z)^(#)cot).(upper_bound A)-((id Z)^(#)cot).(lower_bound A)
proof
assume
A1:A c= Z & f=-cos/sin/f1-(id Z)^/sin^2 & f1=#Z 2
& Z c= dom ((id Z)^(#)cot) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
set g = id Z;
Z c= dom (g^(#)cot) by A1;
then Z c= dom (g^) /\ dom cot by VALUED_1:def 4;then
A3:Z c= dom (g^) by XBOOLE_1:18;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;then
A6:(id Z)^(#)cot is_differentiable_on Z by A1,FDIFF_8:35;
dom f = dom (-cos/sin/f1) /\ dom ((id Z)^/sin^2) by A1,VALUED_1:12;then
A7:dom f c= dom (-cos/sin/f1) & dom f c= dom ((id Z)^/sin^2) by XBOOLE_1:18;
then dom f c= dom (cos/sin/f1) by VALUED_1:8;
then A8:Z c= dom (cos/sin/f1) & Z c= dom ((id Z)^/sin^2) by A1,A7;
dom (cos/sin/f1) = dom (cos/sin) /\ (dom f1 \ f1"{0}) by RFUNCT_1:def 1;then
A9:Z c= dom (cos/sin) by A8,XBOOLE_1:18;
dom ((id Z)^/sin^2) c= dom ((id Z)^) /\ (dom (sin^2) \ (sin^2)"{0})
by RFUNCT_1:def 1;then
dom ((id Z)^/sin^2) c= dom ((id Z)^)
& dom ((id Z)^/sin^2) c= dom (sin^2) \ (sin^2)"{0} by XBOOLE_1:18;then
A10:Z c= dom ((id Z)^) & Z c= dom (sin^2) \ (sin^2)"{0} by A8;
A11:for x st x in Z holds f.x=-cos.x/sin.x/x^2-1/x/(sin.x)^2
proof
let x;
assume
A12:x in Z;then
(-cos/sin/f1 - (id Z)^/sin^2).x
=(-cos/sin/f1).x-((id Z)^/sin^2).x by A1,VALUED_1:13
.=-(cos/sin/f1).x-((id Z)^/sin^2).x by VALUED_1:8
.=-((cos/sin).x/f1.x)-((id Z)^/sin^2).x by A12,A8,RFUNCT_1:def 1
.=-cos.x/sin.x/f1.x-((id Z)^/sin^2).x by A9,A12,RFUNCT_1:def 1
.=-cos.x/sin.x/f1.x-((id Z)^).x/(sin^2).x by A8,A12,RFUNCT_1:def 1
.=-cos.x/sin.x/f1.x-(((id Z).x)")/(sin^2).x by A10,A12,RFUNCT_1:def 2
.=-cos.x/sin.x/f1.x-1/x/(sin^2).x by A12,FUNCT_1:18
.=-cos.x/sin.x/f1.x-1/x/(sin.x)^2 by VALUED_1:11
.=-cos.x/sin.x/(x #Z 2)-1/x/(sin.x)^2 by A1,TAYLOR_1:def 1
.=-cos.x/sin.x/x^2-1/x/(sin.x)^2 by FDIFF_7:1;
hence thesis by A1;
end;
A13:for x being Element of REAL
st x in dom(((id Z)^(#)cot)`|Z) holds (((id Z)^(#)cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)^(#)cot)`|Z);then
A14:x in Z by A6,FDIFF_1:def 7;then
(((id Z)^(#)cot)`|Z).x=-cos.x/sin.x/x^2-1/x/(sin.x)^2 by A1,A4,FDIFF_8:35
.=f.x by A11,A14;
hence thesis;
end;
dom(((id Z)^(#)cot)`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then(((id Z)^(#)cot)`|Z)= f by A13,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
::f.x=sin.x/cos.x/x+ln.x/(cos.x)^2
theorem
A c= Z & f=sin/cos/(id Z)+ln/cos^2
& Z c= dom (ln(#)tan) & Z = dom f & f|A is continuous implies
integral(f,A)=(ln(#)tan).(upper_bound A)-(ln(#)tan).(lower_bound A)
proof
assume
A1:A c= Z & f=sin/cos/(id Z)+ln/cos^2
& Z c= dom (ln(#)tan) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)tan) is_differentiable_on Z by A1,FDIFF_8:32;
Z = dom (sin/cos/(id Z)) /\ dom (ln/cos^2) by A1,VALUED_1:def 1; then
A4:Z c= dom (sin/cos/(id Z)) & Z c= dom (ln/cos^2) by XBOOLE_1:18;
dom (sin/cos/(id Z)) c= dom (sin/cos) /\ (dom (id Z) \ (id Z)"{0})
by RFUNCT_1:def 1;then
dom (sin/cos/(id Z)) c= dom (sin/cos) by XBOOLE_1:18;then
A5:Z c= dom (sin/cos) by A4;
A6:for x st x in Z holds f.x=sin.x/cos.x/x+ln.x/(cos.x)^2
proof
let x;
assume
A7:x in Z;then
(sin/cos/(id Z)+ln/cos^2).x=(sin/cos/(id Z)).x+(ln/cos^2).x
by A1,VALUED_1:def 1
.=(sin/cos).x/(id Z).x+(ln/cos^2).x by A7,A4,RFUNCT_1:def 1
.=sin.x/cos.x/(id Z).x+(ln/cos^2).x by A5,A7,RFUNCT_1:def 1
.=sin.x/cos.x/x+(ln/cos^2).x by A7,FUNCT_1:18
.=sin.x/cos.x/x+ln.x/(cos^2).x by A7,A4,RFUNCT_1:def 1
.=sin.x/cos.x/x+ln.x/(cos.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A8:for x being Element of REAL
st x in dom ((ln(#)tan)`|Z) holds ((ln(#)tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((ln(#)tan)`|Z);then
A9:x in Z by A3,FDIFF_1:def 7;then
((ln(#)tan)`|Z).x=sin.x/cos.x/x+ln.x/(cos.x)^2 by A1,FDIFF_8:32
.=f.x by A9,A6;
hence thesis;
end;
dom ((ln(#)tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((ln(#)tan)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:32,INTEGRA5:13;
end;
::f.x=cos.x/sin.x/x-ln.x/(sin.x)^2
theorem
A c= Z & f=cos/sin/(id Z)-ln/sin^2
& Z c= dom (ln(#)cot) & Z = dom f & f|A is continuous implies
integral(f,A)=(ln(#)cot).(upper_bound A)-(ln(#)cot).(lower_bound A)
proof
assume
A1:A c= Z & f=cos/sin/(id Z)-ln/sin^2
& Z c= dom (ln(#)cot) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)cot) is_differentiable_on Z by A1,FDIFF_8:33;
Z = dom (cos/sin/(id Z)) /\ dom (ln/sin^2) by A1,VALUED_1:12;
then
A4:Z c= dom (cos/sin/(id Z)) & Z c= dom (ln/sin^2) by XBOOLE_1:18;
dom (cos/sin/(id Z)) c= dom (cos/sin) /\ (dom (id Z) \ (id Z)"{0})
by RFUNCT_1:def 1;then
dom (cos/sin/(id Z)) c= dom (cos/sin) by XBOOLE_1:18;then
A5:Z c= dom (cos/sin) by A4;
A6:for x st x in Z holds f.x=cos.x/sin.x/x-ln.x/(sin.x)^2
proof
let x;
assume
A7:x in Z;then
(cos/sin/(id Z)-ln/sin^2).x=(cos/sin/(id Z)).x-(ln/sin^2).x
by A1,VALUED_1:13
.=(cos/sin).x/(id Z).x-(ln/sin^2).x by A7,A4,RFUNCT_1:def 1
.=cos.x/sin.x/(id Z).x-(ln/sin^2).x by A5,A7,RFUNCT_1:def 1
.=cos.x/sin.x/x-(ln/sin^2).x by A7,FUNCT_1:18
.=cos.x/sin.x/x-ln.x/(sin^2).x by A7,A4,RFUNCT_1:def 1
.=cos.x/sin.x/x-ln.x/(sin.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A8:for x being Element of REAL
st x in dom ((ln(#)cot)`|Z) holds ((ln(#)cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((ln(#)cot)`|Z);then
A9:x in Z by A3,FDIFF_1:def 7;then
((ln(#)cot)`|Z).x=cos.x/sin.x/x-ln.x/(sin.x)^2 by A1,FDIFF_8:33
.=f.x by A9,A6;
hence thesis;
end;
dom ((ln(#)cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((ln(#)cot)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:33,INTEGRA5:13;
end;
::f.x=tan.x/x+ln.x/(cos.x)^2
theorem
A c= Z & f=tan/(id Z)+ln/cos^2
& Z c= dom (ln(#)tan) & Z c= dom tan & Z = dom f & f|A is continuous implies
integral(f,A)=(ln(#)tan).(upper_bound A)-(ln(#)tan).(lower_bound A)
proof
assume
A1:A c= Z & f=tan/(id Z)+ln/cos^2
& Z c= dom (ln(#)tan) & Z c= dom tan & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)tan) is_differentiable_on Z by A1,FDIFF_8:32;
Z = dom (tan/(id Z)) /\ dom(ln/cos^2) by A1,VALUED_1:def 1;then
A4:Z c= dom (tan/(id Z)) & Z c= dom(ln/cos^2) by XBOOLE_1:18;
A5:for x st x in Z holds f.x=tan.x/x+ln.x/(cos.x)^2
proof
let x;
assume
A6:x in Z;then
(tan/(id Z)+ln/cos^2).x =(tan/(id Z)).x+(ln/cos^2).x by A1,VALUED_1:def 1
.=tan.x/(id Z).x+(ln/cos^2).x by A6,A4,RFUNCT_1:def 1
.=tan.x/x+(ln/cos^2).x by A6,FUNCT_1:18
.=tan.x/x+ln.x/(cos^2).x by A6,A4,RFUNCT_1:def 1
.=tan.x/x+ln.x/(cos.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A7:for x being Element of REAL
st x in dom ((ln(#)tan)`|Z) holds ((ln(#)tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((ln(#)tan)`|Z);then
A8:x in Z by A3,FDIFF_1:def 7;then
((ln(#)tan)`|Z).x=tan(x)/x+ln.x/(cos.x)^2 by A1,FDIFF_8:32
.=tan.x/x+ln.x/(cos.x)^2 by A1,A8,FDIFF_8:1,SIN_COS9:15
.=f.x by A8,A5;
hence thesis;
end;
dom ((ln(#)tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((ln(#)tan)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:32,INTEGRA5:13;
end;
::f.x=cot.x/x-ln.x/(sin.x)^2
theorem
A c= Z & f=cot/(id Z)-ln/sin^2
& Z c= dom (ln(#)cot) & Z c= dom cot & Z = dom f & f|A is continuous implies
integral(f,A)=(ln(#)cot).(upper_bound A)-(ln(#)cot).(lower_bound A)
proof
assume
A1:A c= Z & f=cot/(id Z)-ln/sin^2
& Z c= dom (ln(#)cot) & Z c= dom cot & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(ln(#)cot) is_differentiable_on Z by A1,FDIFF_8:33;
Z = dom (cot/(id Z)) /\ dom(ln/sin^2) by A1,VALUED_1:12;then
A4:Z c= dom (cot/(id Z)) & Z c= dom(ln/sin^2) by XBOOLE_1:18;
A5:for x st x in Z holds f.x=cot.x/x-ln.x/(sin.x)^2
proof
let x;
assume
A6:x in Z;then
(cot/(id Z)-ln/sin^2).x =(cot/(id Z)).x-(ln/sin^2).x by A1,VALUED_1:13
.=cot.x/(id Z).x-(ln/sin^2).x by A6,A4,RFUNCT_1:def 1
.=cot.x/x-(ln/sin^2).x by A6,FUNCT_1:18
.=cot.x/x-ln.x/(sin^2).x by A6,A4,RFUNCT_1:def 1
.=cot.x/x-ln.x/(sin.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A7:for x being Element of REAL
st x in dom ((ln(#)cot)`|Z) holds ((ln(#)cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((ln(#)cot)`|Z);then
A8:x in Z by A3,FDIFF_1:def 7;then
((ln(#)cot)`|Z).x=cot(x)/x-ln.x/(sin.x)^2 by A1,FDIFF_8:33
.=cot.x/x-ln.x/(sin.x)^2 by A1,A8,FDIFF_8:2,SIN_COS9:16
.=f.x by A5,A8;
hence thesis;
end;
dom ((ln(#)cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((ln(#)cot)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:33,INTEGRA5:13;
end;
::f.x=arctan.x/x+ln.x/(1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(id Z)+ln/(f1+( #Z 2))
& Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies
integral(f,A)=(ln(#)arctan).(upper_bound A)-(ln(#)arctan).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(id Z)+ln/(f1+( #Z 2))
& Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (arctan/(id Z)) /\ dom (ln/(f1+( #Z 2))) by A1,VALUED_1:def 1;
then
A3:Z c= dom (arctan/(id Z)) & Z c= dom (ln/(f1+( #Z 2))) by XBOOLE_1:18;
then
Z c= dom (arctan) /\ (dom (id Z) \ (id Z)"{0}) by RFUNCT_1:def 1;then
A4:Z c= dom (arctan) by XBOOLE_1:18;
Z c= dom ln /\ (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by A3,RFUNCT_1:def 1;
then
A5:Z c= dom ln & Z c= (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by XBOOLE_1:18;
then Z c= dom (arctan) /\ dom ln by A4,XBOOLE_1:19;then
A6:Z c= dom (ln(#)arctan) by VALUED_1:def 4;
then A7:ln(#)arctan is_differentiable_on Z by A1,SIN_COS9:127;
A8:Z c= dom ((f1+#Z 2)^) by A5,RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A9:Z c= dom (f1+#Z 2) by A8;
A10:for x st x in Z holds f.x=arctan.x/x+ln.x/(1+x^2)
proof
let x;
assume
A11:x in Z;
then (arctan/(id Z)+ln/(f1+( #Z 2))).x
=(arctan/(id Z)).x+(ln/(f1+( #Z 2))).x by A1,VALUED_1:def 1
.=arctan.x*((id Z).x)" +(ln/(f1+( #Z 2))).x by A3,A11,RFUNCT_1:def 1
.=arctan.x*((id Z).x)"+(ln.x*((f1+( #Z 2)).x)") by A3,A11,RFUNCT_1:def 1
.=arctan.x/x+(ln.x/(f1+( #Z 2)).x) by A11,FUNCT_1:18
.=arctan.x/x+ln.x/(f1.x+( #Z 2).x) by A9,A11,VALUED_1:def 1
.=arctan.x/x+ln.x/(1+( #Z 2).x) by A1,A11
.=arctan.x/x+ln.x/(1+(x #Z 2)) by TAYLOR_1:def 1
.=arctan.x/x+ln.x/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A12:for x being Element of REAL
st x in dom((ln(#)arctan)`|Z) holds ((ln(#)arctan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((ln(#)arctan)`|Z);then
A13: x in Z by A7,FDIFF_1:def 7;then
((ln(#)arctan)`|Z).x=arctan.x/x+ln.x/(1+x^2) by A1,A6,SIN_COS9:127
.=f.x by A13,A10;
hence thesis;
end;
dom((ln(#)arctan)`|Z)=dom f by A1,A7,FDIFF_1:def 7;
then ((ln(#)arctan)`|Z)= f by A12,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13,SIN_COS9:127;
end;
::f.x=arccot.x/x-ln.x/(1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(id Z)-ln/(f1+( #Z 2))
& Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies
integral(f,A)=(ln(#)arccot).(upper_bound A)-(ln(#)arccot).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(id Z)-ln/(f1+( #Z 2))
& Z c= ]. -1,1 .[ & Z = dom f
& f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (arccot/(id Z)) /\ dom (ln/(f1+( #Z 2))) by A1,VALUED_1:12;
then
A3:Z c= dom (arccot/(id Z)) & Z c= dom (ln/(f1+( #Z 2))) by XBOOLE_1:18;
then
Z c= dom (arccot) /\ (dom (id Z) \ (id Z)"{0}) by RFUNCT_1:def 1;then
A4:Z c= dom (arccot) by XBOOLE_1:18;
Z c= dom ln /\ (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by A3,RFUNCT_1:def 1;
then
A5:Z c= dom ln & Z c= (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by XBOOLE_1:18;
then Z c= dom (arccot) /\ dom ln by A4,XBOOLE_1:19;then
A6:Z c= dom (ln(#)arccot) by VALUED_1:def 4;
then A7:ln(#)arccot is_differentiable_on Z by A1,SIN_COS9:128;
A8:Z c= dom ((f1+#Z 2)^) by A5,RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A9:Z c= dom (f1+#Z 2) by A8;
A10:for x st x in Z holds f.x=arccot.x/x-ln.x/(1+x^2)
proof
let x;
assume
A11:x in Z;
then (arccot/(id Z)-ln/(f1+( #Z 2))).x
=(arccot/(id Z)).x-(ln/(f1+( #Z 2))).x by A1,VALUED_1:13
.=arccot.x*((id Z).x)" -(ln/(f1+( #Z 2))).x by A3,A11,RFUNCT_1:def 1
.=arccot.x*((id Z).x)"-(ln.x*((f1+( #Z 2)).x)") by A3,A11,RFUNCT_1:def 1
.=arccot.x/x-(ln.x/(f1+( #Z 2)).x) by A11,FUNCT_1:18
.=arccot.x/x-ln.x/(f1.x+( #Z 2).x) by A9,A11,VALUED_1:def 1
.=arccot.x/x-ln.x/(1+( #Z 2).x) by A1,A11
.=arccot.x/x-ln.x/(1+(x #Z 2)) by TAYLOR_1:def 1
.=arccot.x/x-ln.x/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A12: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
A13:x in Z by A7,FDIFF_1:def 7;then
((ln(#)arccot)`|Z).x=arccot.x/x-ln.x/(1+x^2) by A1,A6,SIN_COS9:128
.=f.x by A10,A13;
hence thesis;
end;
dom((ln(#)arccot)`|Z)=dom f by A1,A7,FDIFF_1:def 7;
then ((ln(#)arccot)`|Z)= f by A12,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13,SIN_COS9:128;
end;
::f.x=exp_R.(tan.x)/(cos.x)^2
theorem
A c= Z & f=exp_R*tan/cos^2 & Z = dom f & f|A is continuous
implies integral(f,A)=(exp_R*tan).(upper_bound A)-(exp_R*tan).(lower_bound A)
proof
assume
A1:A c= Z & f=exp_R*tan/cos^2 & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (exp_R*tan) /\ (dom (cos^2) \ (cos^2)"{0}) by A1,RFUNCT_1:def 1;then
A3:Z c= dom (exp_R*tan) by XBOOLE_1:18;
then A4:exp_R*tan is_differentiable_on Z by FDIFF_8:16;
A5:for x st x in Z holds f.x=exp_R.(tan.x)/(cos.x)^2
proof
let x;
assume
A6:x in Z;
then (exp_R*tan/cos^2).x=(exp_R*tan).x/(cos^2).x by A1,RFUNCT_1:def 1
.=exp_R.(tan.x)/(cos^2).x by A3,A6,FUNCT_1:12
.=exp_R.(tan.x)/(cos.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A7: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
A8:x in Z by A4,FDIFF_1:def 7;then
((exp_R*tan)`|Z).x=exp_R.(tan.x)/(cos.x)^2 by A3,FDIFF_8:16
.=f.x by A5,A8;
hence thesis;
end;
dom ((exp_R*tan)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((exp_R*tan)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,A3,FDIFF_8:16,INTEGRA5:13;
end;
::f.x=-exp_R.(cot.x)/(sin.x)^2
theorem
A c= Z & f=-exp_R*cot/sin^2 & Z = dom f & f|A is continuous
implies integral(f,A)=(exp_R*cot).(upper_bound A)-(exp_R*cot).(lower_bound A)
proof
assume
A1:A c= Z & f=-exp_R*cot/sin^2 & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z = dom (exp_R*cot/sin^2) by A1,VALUED_1:8;
then Z c= dom (exp_R*cot) /\ (dom (sin^2) \ (sin^2)"{0})
by RFUNCT_1:def 1;then
A4:Z c= dom (exp_R*cot) by XBOOLE_1:18;
then A5:exp_R*cot is_differentiable_on Z by FDIFF_8:17;
A6:for x st x in Z holds f.x=-exp_R.(cot.x)/(sin.x)^2
proof
let x;
assume
A7:x in Z;
(-exp_R*cot/sin^2).x =-(exp_R*cot/sin^2).x by VALUED_1:8
.=-(exp_R*cot).x/(sin^2).x by A7,A3,RFUNCT_1:def 1
.=-exp_R.(cot.x)/(sin^2).x by A4,A7,FUNCT_1:12
.=-exp_R.(cot.x)/(sin.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A8: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
A9:x in Z by A5,FDIFF_1:def 7;then
((exp_R*cot)`|Z).x=-exp_R.(cot.x)/(sin.x)^2 by A4,FDIFF_8:17
.=f.x by A6,A9;
hence thesis;
end;
dom ((exp_R*cot)`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then ((exp_R*cot)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,A4,FDIFF_8:17,INTEGRA5:13;
end;
theorem Th23:
Z c= dom (exp_R*cot) implies -exp_R*cot is_differentiable_on Z &
for x st x in Z holds ((-exp_R*cot)`|Z).x = exp_R.(cot.x)/(sin.x)^2
proof
assume
A1:Z c= dom (exp_R*cot);
then A2:Z c= dom (-exp_R*cot) by VALUED_1:8;
A3: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;
A4:exp_R*cot is_differentiable_on Z by A1,FDIFF_8:17;
then A5:(-1)(#)(exp_R*cot) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-exp_R*cot)`|Z).x = exp_R.(cot.x)/(sin.x)^2
proof
let x;
assume
A6:x in Z; then
A7:sin.x<>0 by A3; then
A8:cot is_differentiable_in x by FDIFF_7:47;
A9:exp_R is_differentiable_in cot.x by SIN_COS:65;
A10:exp_R*cot is_differentiable_in x by A4,A6,FDIFF_1:9;
((-exp_R*cot)`|Z).x=diff(-exp_R*cot,x) by A5,A6,FDIFF_1:def 7
.=(-1)*(diff(exp_R*cot,x)) by A10,FDIFF_1:15
.=(-1)*(diff(exp_R,cot.x)*diff(cot,x))
by A8,A9,FDIFF_2:13
.=(-1)*(diff(exp_R,cot.x)*(-1/(sin.x)^2))
by A7,FDIFF_7:47
.=(-1)*(exp_R.(cot.x) * (-1/(sin.x)^2)) by SIN_COS:65
.=exp_R.(cot.x)/(sin.x)^2;
hence thesis;
end;
hence thesis by A2,A4,FDIFF_1:20;
end;
::f.x=exp_R.(cot.x)/(sin.x)^2
theorem
A c= Z & f=exp_R*cot/sin^2 & Z = dom f & f|A is continuous
implies integral(f,A)=(-exp_R*cot).(upper_bound A)-
(-exp_R*cot).(lower_bound A)
proof
assume
A1: A c= Z & f=exp_R*cot/sin^2 & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (exp_R*cot) /\ (dom (sin^2) \ (sin^2)"{0}) by A1,RFUNCT_1:def 1;then
A3:Z c= dom (exp_R*cot) by XBOOLE_1:18;
then A4:-exp_R*cot is_differentiable_on Z by Th23;
A5:for x st x in Z holds f.x=exp_R.(cot.x)/(sin.x)^2
proof
let x;
assume
A6:x in Z;
then (exp_R*cot/sin^2).x=(exp_R*cot).x/(sin^2).x by A1,RFUNCT_1:def 1
.=exp_R.(cot.x)/(sin^2).x by A3,A6,FUNCT_1:12
.=exp_R.(cot.x)/(sin.x)^2 by VALUED_1:11;
hence thesis by A1;
end;
A7: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
A8:x in Z by A4,FDIFF_1:def 7;then
((-exp_R*cot)`|Z).x=exp_R.(cot.x)/(sin.x)^2 by Th23,A3
.=f.x by A5,A8;
hence thesis;
end;
dom ((-exp_R*cot)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((-exp_R*cot)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,Th23,A3,INTEGRA5:13;
end;
::f.x=1/(x*(cos.(ln.x))^2)
theorem
A c= Z & f=((id Z)(#)(cos*ln)^2)^
& Z c= dom (tan*ln) & Z = dom f & f|A is continuous
implies integral(f,A)=(tan*ln).(upper_bound A)-(tan*ln).(lower_bound A)
proof
assume
A1:A c= Z & f=((id Z)(#)(cos*ln)^2)^
& Z c= dom (tan*ln) & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan*ln is_differentiable_on Z by A1,FDIFF_8:14;
Z c= dom ((id Z)(#)(cos*ln)^2) by A1,RFUNCT_1:1;
then Z c= dom (id Z) /\ dom ((cos*ln)^2) by VALUED_1:def 4;then
Z c= dom ((cos*ln)^2) by XBOOLE_1:18;
then A4:Z c= dom (cos*ln) by VALUED_1:11;
A5:for x st x in Z holds f.x=1/(x*(cos.(ln.x))^2)
proof
let x;
assume
A6:x in Z;
then (((id Z)(#)(cos*ln)^2)^).x
=1/(((id Z)(#)(cos*ln)^2).x) by A1,RFUNCT_1:def 2
.=1/((id Z).x*((cos*ln)^2).x) by VALUED_1:5
.=1/(x*((cos*ln)^2).x) by A6,FUNCT_1:18
.=1/(x*((cos*ln).x)^2) by VALUED_1:11
.=1/(x*(cos.(ln.x))^2) by A4,A6,FUNCT_1:12;
hence thesis by A1;
end;
A7:for x being Element of REAL
st x in dom ((tan*ln)`|Z) holds ((tan*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((tan*ln)`|Z);then
A8:x in Z by A3,FDIFF_1:def 7;then
((tan*ln)`|Z).x=1/(x*(cos.(ln.x))^2) by A1,FDIFF_8:14
.=f.x by A5,A8;
hence thesis;
end;
dom ((tan*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan*ln)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:14,INTEGRA5:13;
end;
::f.x= -1/(x*(sin.(ln.x))^2)
theorem
A c= Z & f=-((id Z)(#)(sin*ln)^2)^
& Z c= dom (cot*ln) & Z = dom f & f|A is continuous
implies integral(f,A)=(cot*ln).(upper_bound A)-(cot*ln).(lower_bound A)
proof
assume
A1:A c= Z & f=-((id Z)(#)(sin*ln)^2)^
& Z c= dom (cot*ln) & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:cot*ln is_differentiable_on Z by A1,FDIFF_8:15;
A4:Z = dom (((id Z)(#)(sin*ln)^2)^) by A1,VALUED_1:8;
then Z c= dom ((id Z)(#)(sin*ln)^2) by RFUNCT_1:1;
then Z c= dom (id Z) /\ dom ((sin*ln)^2) by VALUED_1:def 4;then
Z c= dom ((sin*ln)^2) by XBOOLE_1:18;
then A5:Z c= dom (sin*ln) by VALUED_1:11;
A6:for x st x in Z holds f.x=-1/(x*(sin.(ln.x))^2)
proof
let x;
assume
A7:x in Z;
(-((id Z)(#)(sin*ln)^2)^).x =-(((id Z)(#)(sin*ln)^2)^).x by VALUED_1:8
.=-1/(((id Z)(#)(sin*ln)^2).x) by A4,A7,RFUNCT_1:def 2
.=-1/((id Z).x*((sin*ln)^2).x) by VALUED_1:5
.=-1/(x*((sin*ln)^2).x) by A7,FUNCT_1:18
.=-1/(x*((sin*ln).x)^2) by VALUED_1:11
.=-1/(x*(sin.(ln.x))^2) by A5,A7,FUNCT_1:12;
hence thesis by A1;
end;
A8:for x being Element of REAL
st x in dom ((cot*ln)`|Z) holds ((cot*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((cot*ln)`|Z);then
A9:x in Z by A3,FDIFF_1:def 7;then
((cot*ln)`|Z).x= -1/(x*(sin.(ln.x))^2) by A1,FDIFF_8:15
.=f.x by A6,A9;
hence thesis;
end;
dom ((cot*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((cot*ln)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:15,INTEGRA5:13;
end;
theorem Th27:
Z c= dom (cot*ln) implies -cot*ln is_differentiable_on Z &
for x st x in Z holds ((-cot*ln)`|Z).x = 1/(x*(sin.(ln.x))^2)
proof
assume
A1:Z c= dom (cot*ln);
then A2:Z c= dom (-cot*ln) by VALUED_1:8;
dom (cot*ln) c= dom ln by RELAT_1:25;
then A3:Z c= dom ln by A1;
A4: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A3,TAYLOR_1:18;
then ex g being Real st x=g & 0<g by Lm2;
hence thesis;
end;
A5: for x st x in Z holds sin.(ln.x)<>0
proof
let x;
assume x in Z;
then ln.x in dom (cos/sin) by A1,FUNCT_1:11;
hence thesis by FDIFF_8:2;
end;
A6:for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A4;
then x in right_open_halfline(0) by Lm2;
hence thesis by TAYLOR_1:18;
end;
A7:cot*ln is_differentiable_on Z by A1,FDIFF_8:15;
then A8:(-1)(#)(cot*ln) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-cot*ln)`|Z).x = 1/(x*(sin.(ln.x))^2)
proof
let x;
assume
A9:x in Z; then
A10:ln is_differentiable_in x by A4,TAYLOR_1:18;
A11:x>0 & sin.(ln.x)<>0 by A4,A5,A9;then
A12:cot is_differentiable_in ln.x by FDIFF_7:47;
A13:cot*ln is_differentiable_in x by A7,A9,FDIFF_1:9;
((-cot*ln)`|Z).x=diff(-cot*ln,x) by A8,A9,FDIFF_1:def 7
.=(-1)*(diff(cot*ln,x)) by A13,FDIFF_1:15
.=(-1)*(diff(cot,ln.x)*diff(ln,x)) by A10,A12,FDIFF_2:13
.=(-1)*((-1/(sin.(ln.x))^2) * diff(ln,x)) by A11,FDIFF_7:47
.=(-1)*(-diff(ln,x)/(sin.(ln.x))^2)
.=(-1)*(-(1/x)/(sin.(ln.x))^2) by A6,A9
.=1/(x*(sin.(ln.x))^2) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A2,A7,FDIFF_1:20;
end;
::f.x= 1/(x*(sin.(ln.x))^2)
theorem
A c= Z & f=((id Z)(#)(sin*ln)^2)^
& Z c= dom (cot*ln) & Z = dom f & f|A is continuous
implies integral(f,A)=(-cot*ln).(upper_bound A)-(-cot*ln).(lower_bound A)
proof
assume
A1:A c= Z & f=((id Z)(#)(sin*ln)^2)^
& Z c= dom (cot*ln) & Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cot*ln is_differentiable_on Z by A1,Th27;
Z c= dom ((id Z)(#)(sin*ln)^2) by A1,RFUNCT_1:1;
then Z c= dom (id Z) /\ dom ((sin*ln)^2) by VALUED_1:def 4;then
Z c= dom ((sin*ln)^2) by XBOOLE_1:18;
then A4:Z c= dom (sin*ln) by VALUED_1:11;
A5:for x st x in Z holds f.x=1/(x*(sin.(ln.x))^2)
proof
let x;
assume
A6:x in Z;
then (((id Z)(#)(sin*ln)^2)^).x
=1/(((id Z)(#)(sin*ln)^2).x) by A1,RFUNCT_1:def 2
.=1/((id Z).x*((sin*ln)^2).x) by VALUED_1:5
.=1/(x*((sin*ln)^2).x) by A6,FUNCT_1:18
.=1/(x*((sin*ln).x)^2) by VALUED_1:11
.=1/(x*(sin.(ln.x))^2) by A4,A6,FUNCT_1:12;
hence thesis by A1;
end;
A7:for x being Element of REAL
st x in dom ((-cot*ln)`|Z) holds ((-cot*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cot*ln)`|Z);then
A8:x in Z by A3,FDIFF_1:def 7;then
((-cot*ln)`|Z).x= 1/(x*(sin.(ln.x))^2) by A1,Th27
.=f.x by A5,A8;
hence thesis;
end;
dom ((-cot*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cot*ln)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,Th27,INTEGRA5:13;
end;
::f.x=exp_R.x/(cos.(exp_R.x))^2
theorem
A c= Z & f=exp_R/(cos*exp_R)^2
& Z c= dom (tan*exp_R) & Z = dom f & f|A is continuous
implies integral(f,A)=(tan*exp_R).(upper_bound A)-(tan*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & f=exp_R/(cos*exp_R)^2
& Z c= dom (tan*exp_R) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan*exp_R is_differentiable_on Z by A1,FDIFF_8:12;
Z = dom exp_R /\ (dom ((cos*exp_R)^2) \ ((cos*exp_R)^2)"{0})
by A1,RFUNCT_1:def 1;then
Z c= dom ((cos*exp_R)^2) \ ((cos*exp_R)^2)"{0} by XBOOLE_1:18; then
A4:Z c= dom (((cos*exp_R)^2)^) by RFUNCT_1:def 2;
dom (((cos*exp_R)^2)^) c= dom ((cos*exp_R)^2) by RFUNCT_1:1;then
Z c= dom ((cos*exp_R)^2) by A4;
then A5:Z c= dom (cos*exp_R) by VALUED_1:11;
A6:for x st x in Z holds f.x=exp_R.x/(cos.(exp_R.x))^2
proof
let x;
assume
A7:x in Z;
then
(exp_R/(cos*exp_R)^2).x =exp_R.x/((cos*exp_R)^2).x by A1,RFUNCT_1:def 1
.=exp_R.x/((cos*exp_R).x)^2 by VALUED_1:11
.=exp_R.x/(cos.(exp_R.x))^2 by A5,A7,FUNCT_1:12;
hence thesis by A1;
end;
A8:for x being Element of REAL st x in dom ((tan*exp_R)`|Z)
holds ((tan*exp_R)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((tan*exp_R)`|Z);then
A9:x in Z by A3,FDIFF_1:def 7;then
((tan*exp_R)`|Z).x=exp_R.x/(cos.(exp_R.x))^2 by A1,FDIFF_8:12
.=f.x by A6,A9;
hence thesis;
end;
dom ((tan*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan*exp_R)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:12,INTEGRA5:13;
end;
::f.x=-exp_R.x/(sin.(exp_R.x))^2
theorem
A c= Z & f=-exp_R/(sin*exp_R)^2
& Z c= dom (cot*exp_R) & Z = dom f & f|A is continuous
implies integral(f,A)=(cot*exp_R).(upper_bound A)-(cot*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & f=-exp_R/(sin*exp_R)^2
& Z c= dom (cot*exp_R) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:cot*exp_R is_differentiable_on Z by A1,FDIFF_8:13;
A4:Z = dom (exp_R/(sin*exp_R)^2) by A1,VALUED_1:8;
then Z c= dom (exp_R) /\ (dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0})
by RFUNCT_1:def 1;then
Z c= dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0} by XBOOLE_1:18;
then
A5:Z c= dom (((sin*exp_R)^2)^) by RFUNCT_1:def 2;
dom (((sin*exp_R)^2)^) c= dom ((sin*exp_R)^2) by RFUNCT_1:1;then
Z c= dom ((sin*exp_R)^2) by A5;
then A6:Z c= dom (sin*exp_R) by VALUED_1:11;
A7:for x st x in Z holds f.x=-exp_R.x/(sin.(exp_R.x))^2
proof
let x;
assume
A8:x in Z;
(-exp_R/(sin*exp_R)^2).x =-(exp_R/(sin*exp_R)^2).x by VALUED_1:8
.=-exp_R.x/((sin*exp_R)^2).x by A4,A8,RFUNCT_1:def 1
.=-exp_R.x/((sin*exp_R).x)^2 by VALUED_1:11
.=-exp_R.x/(sin.(exp_R.x))^2 by A6,A8,FUNCT_1:12;
hence thesis by A1;
end;
A9:for x being Element of REAL
st x in dom ((cot*exp_R)`|Z) holds ((cot*exp_R)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((cot*exp_R)`|Z);then
A10:x in Z by A3,FDIFF_1:def 7;then
((cot*exp_R)`|Z).x=-exp_R.x/(sin.(exp_R.x))^2 by A1,FDIFF_8:13
.=f.x by A7,A10;
hence thesis;
end;
dom ((cot*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((cot*exp_R)`|Z)= f by A9,PARTFUN1:5;
hence thesis by A1,A2,FDIFF_8:13,INTEGRA5:13;
end;
theorem Th31:
Z c= dom (cot*exp_R) implies -cot*exp_R is_differentiable_on Z &
for x st x in Z holds ((-cot*exp_R)`|Z).x = exp_R.x/(sin.(exp_R.x))^2
proof
assume
A1:Z c= dom (cot*exp_R);
then A2:Z c= dom (-cot*exp_R) by VALUED_1:8;
A3:cot*exp_R is_differentiable_on Z by A1,FDIFF_8:13;
then A4:(-1)(#)(cot*exp_R) is_differentiable_on Z by A2,FDIFF_1:20;
A5:for x st x in Z holds sin.(exp_R.x)<>0
proof
let x;
assume x in Z;
then exp_R.x in dom (cos/sin) by A1,FUNCT_1:11;
hence thesis by FDIFF_8:2;
end;
for x st x in Z holds ((-cot*exp_R)`|Z).x = exp_R.x/(sin.(exp_R.x))^2
proof
let x;
assume
A6: x in Z;
A7: exp_R is_differentiable_in x by SIN_COS:65;
A8: sin.(exp_R.x)<>0 by A5,A6;then
A9: cot is_differentiable_in exp_R.x by FDIFF_7:47;
A10:cot*exp_R is_differentiable_in x by A3,A6,FDIFF_1:9;
((-cot*exp_R)`|Z).x=diff(-cot*exp_R,x) by A4,A6,FDIFF_1:def 7
.=(-1)*(diff(cot*exp_R,x)) by A10,FDIFF_1:15
.=(-1)*(diff(cot, exp_R.x)*diff(exp_R,x))
by A7,A9,FDIFF_2:13
.=(-1)*((-1/(sin.(exp_R.x))^2) * diff(exp_R,x))
by A8,FDIFF_7:47
.=(-1)*(-diff(exp_R,x)/(sin.(exp_R.x))^2)
.=exp_R.x/(sin.(exp_R.x))^2 by SIN_COS:65;
hence thesis;
end;
hence thesis by A4;
end;
::f.x=exp_R.x/(sin.(exp_R.x))^2
theorem
A c= Z & f=exp_R/(sin*exp_R)^2
& Z c= dom (cot*exp_R) & Z = dom f & f|A is continuous
implies integral(f,A)=(-cot*exp_R).(upper_bound A)-
(-cot*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & f=exp_R/(sin*exp_R)^2
& Z c= dom (cot*exp_R) & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cot*exp_R is_differentiable_on Z by A1,Th31;
Z c= dom (exp_R) /\ (dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0})
by A1,RFUNCT_1:def 1;then
Z c= dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0} by XBOOLE_1:18;
then A4:Z c= dom (((sin*exp_R)^2)^) by RFUNCT_1:def 2;
dom (((sin*exp_R)^2)^) c= dom ((sin*exp_R)^2) by RFUNCT_1:1;then
Z c= dom ((sin*exp_R)^2) by A4;
then A5:Z c= dom (sin*exp_R) by VALUED_1:11;
A6:for x st x in Z holds f.x=exp_R.x/(sin.(exp_R.x))^2
proof
let x;
assume
A7:x in Z;then
(exp_R/(sin*exp_R)^2).x=exp_R.x/((sin*exp_R)^2).x by A1,RFUNCT_1:def 1
.=exp_R.x/((sin*exp_R).x)^2 by VALUED_1:11
.=exp_R.x/(sin.(exp_R.x))^2 by A5,A7,FUNCT_1:12;
hence thesis by A1;
end;
A8:for x being Element of REAL
st x in dom ((-cot*exp_R)`|Z) holds ((-cot*exp_R)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cot*exp_R)`|Z);then
A9:x in Z by A3,FDIFF_1:def 7;then
((-cot*exp_R)`|Z).x=exp_R.x/(sin.(exp_R.x))^2 by A1,Th31
.=f.x by A6,A9;
hence thesis;
end;
dom ((-cot*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cot*exp_R)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,Th31,INTEGRA5:13;
end;
::f.x=-1/(x^2*(cos.(1/x))^2)
theorem
A c= Z & (for x st x in Z holds f.x=-1/(x^2*(cos.(1/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=-1/(x^2*(cos.(1/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: Z c= dom ((id Z)^) by A1,FUNCT_1:101;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then
A6:(tan*((id Z)^)) is_differentiable_on Z by A1,FDIFF_8:8;
A7: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
A8:x in Z by A6,FDIFF_1:def 7;then
((tan*((id Z)^))`|Z).x=-1/(x^2*(cos.(1/x))^2) by A1,A4,FDIFF_8:8
.=f.x by A1,A8;
hence thesis;
end;
dom ((tan*((id Z)^))`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((tan*((id Z)^))`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
theorem Th34:
Z c= dom (tan*((id Z)^)) implies (-tan*((id Z)^)) is_differentiable_on Z &
for x st x in Z holds ((-tan*((id Z)^))`|Z).x = 1/(x^2*(cos.(1/x))^2)
proof
set f = id Z;
assume
A1:Z c= dom (tan*((id Z)^));
dom (tan*(f^)) c= dom (f^) by RELAT_1:25; then
A2:Z c= dom (f^) by A1;
A3:not 0 in Z
proof
assume A4: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A4; then
not 0 in {0} by A4,A2,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
A5:Z c= dom (-tan*((id Z)^)) by A1,VALUED_1:8;
A6:(tan*((id Z)^)) is_differentiable_on Z by A1,A3,FDIFF_8:8; then
A7:(-1)(#)(tan*((id Z)^)) is_differentiable_on Z by A5,FDIFF_1:20;
A8:f^ is_differentiable_on Z &
for x st x in Z holds ((f^)`|Z).x = -1/x^2 by A3,FDIFF_5:4;
A9: for x st x in Z holds (cos.((f^).x))<>0
proof
let x;
assume x in Z;
then f^.x in dom (sin/cos) by A1,FUNCT_1:11;
hence thesis by FDIFF_8:1;
end;
for x st x in Z holds ((-tan*(f^))`|Z).x = 1/(x^2*(cos.(1/x))^2)
proof
let x;
assume
A10: x in Z; then
A11: f^ is_differentiable_in x by A8,FDIFF_1:9;
A12: cos.((f^).x)<>0 by A9,A10;then
A13:tan is_differentiable_in (f^).x by FDIFF_7:46;
A14:tan*(f^) is_differentiable_in x by A6,A10,FDIFF_1:9;
((-tan*(f^))`|Z).x=diff(-tan*(f^),x) by A7,A10,FDIFF_1:def 7
.=(-1)*(diff(tan*(f^),x)) by A14,FDIFF_1:15
.=(-1)*(diff(tan,(f^).x)*diff((f^),x))
by A11,A13,FDIFF_2:13
.=(-1)*((1/(cos.((f^).x))^2) * diff((f^),x))
by A12,FDIFF_7:46
.=(-1)*(diff((f^),x)/(cos.((f.x)"))^2)
by A2,A10,RFUNCT_1:def 2
.=(-1)*(diff((f^),x)/(cos.(1*x"))^2) by A10,FUNCT_1:18
.=(-1)*(((f^)`|Z).x/(cos.(1*x"))^2)
by A8,A10,FDIFF_1:def 7
.=(-1)*((-1/x^2)/(cos.(1*x"))^2) by A10,A3,FDIFF_5:4
.=(-1)*((-1)/x^2/(cos.(1/x))^2)
.=(-1)*((-1)/(x^2*(cos.(1/x))^2)) by XCMPLX_1:78
.=1/(x^2*(cos.(1/x))^2);
hence thesis;
end;
hence thesis by A7;
end;
::f.x=1/(x^2*(cos.(1/x))^2)
theorem
A c= Z & (for x st x in Z holds f.x=1/(x^2*(cos.(1/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=1/(x^2*(cos.(1/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,Th34;
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=1/(x^2*(cos.(1/x))^2) by A1,Th34
.=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,A3,INTEGRA5:13;
end;
::f.x=1/(x^2*(sin.(1/x))^2)
theorem
A c= Z & (for x st x in Z holds f.x=1/(x^2*(sin.(1/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=1/(x^2*(sin.(1/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: Z c= dom ((id Z)^) by A1,FUNCT_1:101;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then
A6:(cot*((id Z)^)) is_differentiable_on Z by A1,FDIFF_8:9;
A7: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
A8:x in Z by A6,FDIFF_1:def 7;then
((cot*((id Z)^))`|Z).x=1/(x^2*(sin.(1/x))^2) by A1,A4,FDIFF_8:9
.=f.x by A1,A8;
hence thesis;
end;
dom ((cot*((id Z)^))`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((cot*((id Z)^))`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
::f.x=1/((1+x^2)*arctan.x)
theorem
A c= Z & (for x st x in Z holds f1.x=1 & arctan.x>0) & f=((f1+#Z 2)(#)arctan)^
& Z c= ]. -1,1 .[ & Z c= dom (ln*(arctan)) & Z = dom f
& f|A is continuous implies
integral(f,A)=(ln*(arctan)).(upper_bound A)-(ln* (arctan)).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1 & arctan.x>0)
& f=((f1+#Z 2)(#)arctan)^
& Z c= ]. -1,1 .[ & Z c= dom (ln*(arctan)) & 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 arctan.x>0 by A1;
then A4:ln*(arctan) is_differentiable_on Z by A1,SIN_COS9:89;
Z c= dom ((f1+#Z 2)(#)arctan) by A1,RFUNCT_1:1; then
Z c= dom (f1+#Z 2) /\ dom arctan by VALUED_1:def 4;then
A5:Z c= dom (f1+#Z 2) by XBOOLE_1:18;
A6:for x st x in Z holds f.x=1/((1+x^2)*arctan.x)
proof
let x;
assume
A7:x in Z;
then
(((f1+#Z 2)(#)arctan)^).x =1/((f1+#Z 2)(#)arctan).x by A1,RFUNCT_1:def 2
.=1/((f1+#Z 2).x*arctan.x) by VALUED_1:5
.=1/((f1.x+( #Z 2).x)*arctan.x) by A5,A7,VALUED_1:def 1
.=1/((f1.x+(x #Z 2))*arctan.x) by TAYLOR_1:def 1
.=1/((1+(x #Z 2))*arctan.x) by A1,A7
.=1/((1+x^2)*arctan.x) by FDIFF_7:1;
hence thesis by A1;
end;
A8:for x being Element of REAL
st x in dom ((ln*(arctan))`|Z) holds ((ln*(arctan))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((ln*(arctan))`|Z);then
A9:x in Z by A4,FDIFF_1:def 7;then
((ln*(arctan))`|Z).x=1/((1+x^2)*arctan.x) by A1,A3,SIN_COS9:89
.=f.x by A6,A9;
hence thesis;
end;
dom ((ln*(arctan))`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((ln*(arctan))`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,A4,INTEGRA5:13;
end;
::f.x=n*(arctan.x) #Z (n-1) / (1+x^2)
theorem
A c= Z & f=n(#)((( #Z (n-1))*arctan)/(f1+#Z 2))
& (for x st x in Z holds f1.x=1)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*(arctan)) & Z = dom f
& f|A is continuous implies
integral(f,A)=(( #Z n)*arctan).(upper_bound A)-
(( #Z n)*arctan).(lower_bound A)
proof
assume
A1:A c= Z & f=n(#)((( #Z (n-1))*arctan)/(f1+#Z 2))
& (for x st x in Z holds f1.x=1)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*(arctan)) & Z = dom f
& f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:( #Z n)*(arctan) is_differentiable_on Z by A1,SIN_COS9:91;
A4:Z = dom ((( #Z (n-1))*arctan)/(f1+#Z 2)) by A1,VALUED_1:def 5;
then Z c= dom (( #Z (n-1))*arctan) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by RFUNCT_1:def 1;then
A5:Z c= dom (( #Z (n-1))*arctan) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0}
by XBOOLE_1:18;
then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A7:Z c= dom (f1+#Z 2) by A6;
A8:for x st x in Z holds f.x=n*(arctan.x) #Z (n-1) / (1+x^2)
proof
let x;
assume
A9:x in Z;
(n(#)((( #Z (n-1))*arctan)/(f1+#Z 2))).x
=n*(((( #Z (n-1))*arctan)/(f1+#Z 2)).x) by VALUED_1:6
.=n*((( #Z (n-1))*arctan).x*((f1+#Z 2).x)") by A4,A9,RFUNCT_1:def 1
.=n*(( #Z (n-1))*arctan).x/(f1+#Z 2).x
.=n*(( #Z (n-1)).(arctan.x))/(f1+#Z 2).x by A5,A9,FUNCT_1:12
.=n*(arctan.x) #Z (n-1)/(f1+#Z 2).x by TAYLOR_1:def 1
.=n*(arctan.x) #Z (n-1)/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1
.=n*(arctan.x) #Z (n-1)/(1+( #Z 2).x) by A1,A9
.=n*(arctan.x) #Z (n-1)/(1+(x #Z 2)) by TAYLOR_1:def 1
.=n*(arctan.x) #Z (n-1) / (1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A10:for x being Element of REAL st x in dom((( #Z n)*(arctan))`|Z) holds
((( #Z n)*(arctan))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((( #Z n)*(arctan))`|Z);then
A11:x in Z by A3,FDIFF_1:def 7;then
((( #Z n)*(arctan))`|Z).x=n*(arctan.x) #Z (n-1) / (1+x^2) by A1,SIN_COS9:91
.=f.x by A8,A11;
hence thesis;
end;
dom((( #Z n)*(arctan))`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then((( #Z n)*(arctan))`|Z)= f by A10,PARTFUN1:5;
hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:91;
end;
::f.x=-n*(arccot.x) #Z (n-1) / (1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1)
& f=-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2)))
& Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & Z = dom f
& f|A is continuous implies
integral(f,A)=(( #Z n)*arccot).(upper_bound A)-
(( #Z n)*arccot).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1)
& f=-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2)))
& Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & Z = dom f
& f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:( #Z n)*(arccot) is_differentiable_on Z by A1,SIN_COS9:92;
Z = dom (n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))) by A1,VALUED_1:8;
then A4:Z = dom ((( #Z (n-1))*arccot)/(f1+#Z 2)) by VALUED_1:def 5;
then Z c= dom (( #Z (n-1))*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by RFUNCT_1:def 1;then
A5:Z c= dom (( #Z (n-1))*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0}
by XBOOLE_1:18;
then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A7:Z c= dom (f1+#Z 2) by A6;
A8:for x st x in Z holds f.x=-n*(arccot.x) #Z (n-1) / (1+x^2)
proof
let x;
assume
A9: x in Z;
(-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2)))).x
=-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))).x by VALUED_1:8
.=-n*(((( #Z (n-1))*arccot)/(f1+#Z 2))).x by VALUED_1:6
.=-n*((( #Z (n-1))*arccot).x*((f1+#Z 2).x)") by A4,A9,RFUNCT_1:def 1
.=-n*(( #Z (n-1))*arccot).x/(f1+#Z 2).x
.=-n*(( #Z (n-1)).(arccot.x))/(f1+#Z 2).x by A5,A9,FUNCT_1:12
.=-n*(arccot.x) #Z (n-1)/(f1+#Z 2).x by TAYLOR_1:def 1
.=-n*(arccot.x) #Z (n-1)/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1
.=-n*(arccot.x) #Z (n-1)/(1+( #Z 2).x) by A1,A9
.=-n*(arccot.x) #Z (n-1)/(1+(x #Z 2)) by TAYLOR_1:def 1
.=-n*(arccot.x) #Z (n-1) / (1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A10:for x being Element of REAL st x in dom((( #Z n)*(arccot))`|Z) holds
((( #Z n)*(arccot))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((( #Z n)*(arccot))`|Z);then
A11:x in Z by A3,FDIFF_1:def 7;then
((( #Z n)*arccot)`|Z).x=-n*(arccot.x) #Z (n-1) / (1+x^2) by A1,SIN_COS9:92
.=f.x by A11,A8;
hence thesis;
end;
dom((( #Z n)*arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then((( #Z n)*arccot)`|Z)= f by A10,PARTFUN1:5;
hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:92;
end;
theorem Th40:
Z c= dom (( #Z n)*arccot) & Z c= ]. -1,1 .[ implies
-( #Z n)*arccot is_differentiable_on Z & for x st x in Z holds
((-( #Z n)*arccot)`|Z).x = n*(arccot.x) #Z (n-1) / (1+x^2)
proof
assume
A1:Z c= dom (( #Z n)*arccot) & Z c= ]. -1,1 .[;
then A2:Z c= dom (-( #Z n)*arccot) by VALUED_1:8;
A3:( #Z n)*(arccot) is_differentiable_on Z by A1,SIN_COS9:92;
then A4:(-1)(#)(( #Z n)*(arccot)) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-( #Z n)*arccot)`|Z).x
= n*(arccot.x) #Z (n-1) / (1+x^2)
proof
let x;
assume
A5:x in Z;then
A6:-1 < x & x < 1 by A1,XXREAL_1:4;
arccot is_differentiable_on Z by A1,SIN_COS9:82;
then A7:arccot is_differentiable_in x by A5,FDIFF_1:9;
A8:( #Z n)*(arccot) is_differentiable_in x by A3,A5,FDIFF_1:9;
((-( #Z n)*arccot)`|Z).x=diff(-( #Z n)*arccot,x) by A4,A5,FDIFF_1:def 7
.=(-1)*(diff(( #Z n)*arccot,x)) by A8,FDIFF_1:15
.=(-1)*((n*((arccot.x) #Z (n-1))) * diff(arccot,x)) by A7,TAYLOR_1:3
.=(-1)*((n*((arccot.x) #Z (n-1))) * (-1/(1+x^2))) by A6,SIN_COS9:76
.=n*(arccot.x) #Z (n-1) / (1+x^2);
hence thesis;
end;
hence thesis by A2,A3,FDIFF_1:20;
end;
::f.x=n*(arccot.x) #Z (n-1) / (1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1)
& f=n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))
& Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & Z = dom f
& f|A is continuous implies
integral(f,A)=(-( #Z n)*arccot).(upper_bound A)-
(-( #Z n)*arccot).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1)
& f=n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))
& Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & Z = dom f
& f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-( #Z n)*(arccot) is_differentiable_on Z by A1,Th40;
A4:Z = dom ((( #Z (n-1))*arccot)/(f1+#Z 2)) by A1,VALUED_1:def 5;
then Z c= dom (( #Z (n-1))*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by RFUNCT_1:def 1;then
A5:Z c= dom (( #Z (n-1))*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0}
by XBOOLE_1:18;
then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A7:Z c= dom (f1+#Z 2) by A6;
A8:for x st x in Z holds f.x=n*(arccot.x) #Z (n-1) / (1+x^2)
proof
let x;
assume
A9:x in Z;
(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))).x
=n*(((( #Z (n-1))*arccot)/(f1+#Z 2)).x) by VALUED_1:6
.=n*((( #Z (n-1))*arccot).x*((f1+#Z 2).x)") by A4,A9,RFUNCT_1:def 1
.=n*(( #Z (n-1))*arccot).x/(f1+#Z 2).x
.=n*(( #Z (n-1)).(arccot.x))/(f1+#Z 2).x by A5,A9,FUNCT_1:12
.=n*(arccot.x) #Z (n-1)/(f1+#Z 2).x by TAYLOR_1:def 1
.=n*(arccot.x) #Z (n-1)/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1
.=n*(arccot.x) #Z (n-1)/(1+( #Z 2).x) by A1,A9
.=n*(arccot.x) #Z (n-1)/(1+(x #Z 2)) by TAYLOR_1:def 1
.=n*(arccot.x) #Z (n-1) / (1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A10:for x being Element of REAL st x in dom((-( #Z n)*(arccot))`|Z) holds
((-( #Z n)*arccot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((-( #Z n)*(arccot))`|Z);then
A11:x in Z by A3,FDIFF_1:def 7;then
((-( #Z n)*arccot)`|Z).x=n*(arccot.x) #Z (n-1) / (1+x^2) by A1,Th40
.=f.x by A11,A8;
hence thesis;
end;
dom((-( #Z n)*arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then((-( #Z n)*arccot)`|Z)= f by A10,PARTFUN1:5;
hence thesis by A1,A2,Th40,INTEGRA5:13;
end;
::f.x=arctan.x / (1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arctan))
& Z = dom f & f|A is continuous implies
integral(f,A)=((1/2)(#)(( #Z 2)*(arctan))).(upper_bound A)
-((1/2)(#)(( #Z 2)*(arctan))).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arctan))
& Z = dom f & f|A is continuous;then
A2:Z c= dom((1/2)(#)(( #Z 2)*(arctan))) by VALUED_1:def 5;
A3:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A4:(1/2)(#)(( #Z 2)*arctan) is_differentiable_on Z by A1,A2,SIN_COS9:93;
Z c= dom (arctan) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by A1,RFUNCT_1:def 1;then
Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
then A5:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A6:Z c= dom (f1+#Z 2) by A5;
A7:for x st x in Z holds f.x=arctan.x / (1+x^2)
proof
let x;
assume
A8:x in Z;then
(arctan/(f1+#Z 2)).x =arctan.x/(f1+#Z 2).x by A1,RFUNCT_1:def 1
.=arctan.x/(f1.x+(( #Z 2).x)) by A6,A8,VALUED_1:def 1
.=arctan.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1
.=arctan.x/(1+(x #Z 2)) by A1,A8
.=arctan.x / (1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A9:for x being Element of REAL st x in dom(((1/2)(#)(( #Z 2)*(arctan)))`|Z)
holds
(((1/2)(#)(( #Z 2)*arctan))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((1/2)(#)(( #Z 2)*arctan))`|Z);then
A10:x in Z by A4,FDIFF_1:def 7;then
(((1/2)(#)(( #Z 2)*arctan))`|Z).x=arctan.x / (1+x^2) by A1,A2,SIN_COS9:93
.=f.x by A7,A10;
hence thesis;
end;
dom(((1/2)(#)(( #Z 2)*arctan))`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then(((1/2)(#)(( #Z 2)*arctan))`|Z)= f by A9,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13,SIN_COS9:93;
end;
::f.x=-arccot.x / (1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & f=-arccot/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot))
& Z = dom f & f|A is continuous implies
integral(f,A)=((1/2)(#)(( #Z 2)*(arccot))).(upper_bound A)
-((1/2)(#)(( #Z 2)*(arccot))).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & f=-arccot/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot))
& Z = dom f & f|A is continuous;
then
A2:Z c= dom((1/2)(#)(( #Z 2)*(arccot))) by VALUED_1:def 5;
A3:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11;
A4:(1/2)(#)(( #Z 2)*arccot) is_differentiable_on Z by A1,A2,SIN_COS9:94;
A5:Z = dom (arccot/(f1+#Z 2)) by A1,VALUED_1:8;
then
Z c= dom (arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;then
Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A7:Z c= dom (f1+#Z 2) by A6;
A8:for x st x in Z holds f.x=-arccot.x / (1+x^2)
proof
let x;
assume
A9:x in Z;
(-arccot/(f1+#Z 2)).x =-(arccot/(f1+#Z 2)).x by VALUED_1:8
.=-arccot.x/(f1+#Z 2).x by A5,A9,RFUNCT_1:def 1
.=-arccot.x/(f1.x+(( #Z 2).x)) by A7,A9,VALUED_1:def 1
.=-arccot.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1
.=-arccot.x/(1+(x #Z 2)) by A1,A9
.=-arccot.x / (1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A10:for x being Element of REAL st x in dom(((1/2)(#)(( #Z 2)*arccot))`|Z)
holds
(((1/2)(#)(( #Z 2)*arccot))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((1/2)(#)(( #Z 2)*arccot))`|Z);then
A11:x in Z by A4,FDIFF_1:def 7;then
(((1/2)(#)(( #Z 2)*arccot))`|Z).x=-arccot.x / (1+x^2) by A1,A2,SIN_COS9:94
.=f.x by A8,A11;
hence thesis;
end;
dom(((1/2)(#)(( #Z 2)*(arccot)))`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then(((1/2)(#)(( #Z 2)*(arccot)))`|Z)= f by A10,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13,SIN_COS9:94;
end;
theorem Th44:
Z c= dom (( #Z 2)*(arccot)) & Z c= ]. -1,1 .[ implies
-(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z & for x st x in Z holds
((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x = arccot.x / (1+x^2)
proof
assume
A1:Z c= dom (( #Z 2)*(arccot)) & Z c= ]. -1,1 .[;
then A2:Z c= dom((1/2)(#)(( #Z 2)*(arccot))) by VALUED_1:def 5;
then A3:Z c= dom (-(1/2)(#)(( #Z 2)*(arccot))) by VALUED_1:8;
A4:(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z by A2,A1,SIN_COS9:94;
then A5:(-1)(#)((1/2)(#)(( #Z 2)*(arccot))) is_differentiable_on Z
by A3,FDIFF_1:20;
A6:( #Z 2)*(arccot) is_differentiable_on Z & for x st x in Z holds
((( #Z 2)*(arccot))`|Z).x = -2*(arccot.x) #Z (2-1) / (1+x^2)
by A1,SIN_COS9:92;
for x st x in Z holds
((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x = arccot.x / (1+x^2)
proof
let x;
assume
A7: x in Z;then
A8:(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_in x by A4,FDIFF_1:9;
A9:( #Z 2)*(arccot) is_differentiable_in x by A6,A7,FDIFF_1:9;
((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=diff(-(1/2)(#)(( #Z 2)*(arccot)),x)
by A5,A7,FDIFF_1:def 7
.=(-1)*(diff((1/2)(#)(( #Z 2)*(arccot)),x)) by A8,FDIFF_1:15
.=(-1)*((1/2)*diff(( #Z 2)*(arccot),x)) by A9,FDIFF_1:15
.=(-1)*((1/2)*((( #Z 2)*(arccot))`|Z).x) by A6,A7,FDIFF_1:def 7
.=(-1)*((1/2)*(-2*(arccot.x) #Z (2-1) / (1+x^2)))
by A1,A7,SIN_COS9:92
.=(-1)*(-(1/2)*(2*(arccot.x) #Z 1 / (1+x^2)))
.=(-1)*(-(1/2)*(2*arccot.x / (1+x^2))) by PREPOWER:35
.=arccot.x / (1+x^2);
hence thesis;
end;
hence thesis by A3,A4,FDIFF_1:20;
end;
::f.x=arccot.x / (1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot))
& Z = dom f & f|A is continuous implies
integral(f,A)=(-(1/2)(#)(( #Z 2)*(arccot))).(upper_bound A)
-(-(1/2)(#)(( #Z 2)*(arccot))).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot))
& Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z by A1,Th44;
Z c= dom (arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by A1,RFUNCT_1:def 1;then
Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
then A4:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A5:Z c= dom (f1+#Z 2) by A4;
A6:for x st x in Z holds f.x=arccot.x / (1+x^2)
proof
let x;
assume
A7:x in Z;then
(arccot/(f1+#Z 2)).x =arccot.x/(f1+#Z 2).x by A1,RFUNCT_1:def 1
.=arccot.x/(f1.x+(( #Z 2).x)) by A5,A7,VALUED_1:def 1
.=arccot.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1
.=arccot.x/(1+(x #Z 2)) by A1,A7
.=arccot.x / (1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A8:for x being Element of REAL st x in dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z)
holds
((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z);then
A9:x in Z by A3,FDIFF_1:def 7;then
((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=arccot.x / (1+x^2) by A1,Th44
.=f.x by A6,A9;
hence thesis;
end;
dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then((-(1/2)(#)(( #Z 2)*(arccot)))`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,Th44,INTEGRA5:13;
end;
::f.x=arctan.x + x/(1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & f=arctan+(id Z)/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies
integral(f,A)=((id Z)(#)(arctan)).(upper_bound A)-
((id Z)(#)(arctan)).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arctan+(id Z)/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom arctan /\ dom ((id Z)/(f1+#Z 2)) by A1,VALUED_1:def 1;
then
A3:Z c= dom arctan & Z c= dom ((id Z)/(f1+#Z 2)) by XBOOLE_1:18;
then
Z c= dom (id Z) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;
then A4: Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
A5:(id Z)(#)(arctan) is_differentiable_on Z by A1,SIN_COS9:95;
A6:Z c= dom ((f1+#Z 2)^) by A4,RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A7:Z c= dom (f1+#Z 2) by A6;
A8:for x st x in Z holds f.x=arctan.x + x/(1+x^2)
proof
let x;
assume
A9: x in Z;
then (arctan+(id Z)/(f1+#Z 2)).x
=arctan.x+((id Z)/(f1+#Z 2)).x by A1,VALUED_1:def 1
.=arctan.x+(id Z).x/(f1+#Z 2).x by A3,A9,RFUNCT_1:def 1
.=arctan.x+x/(f1+#Z 2).x by A9,FUNCT_1:18
.=arctan.x+x/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1
.=arctan.x+x/(1+( #Z 2).x) by A1,A9
.=arctan.x+x/(1+(x #Z 2)) by TAYLOR_1:def 1
.=arctan.x + x/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A10:for x being Element of REAL st x in dom(((id Z)(#)(arctan))`|Z) holds
(((id Z)(#)(arctan))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)(arctan))`|Z);then
A11:x in Z by A5,FDIFF_1:def 7;then
(((id Z)(#)(arctan))`|Z).x=arctan.x + x/(1+x^2) by A1,SIN_COS9:95
.=f.x by A8,A11;
hence thesis;
end;
dom(((id Z)(#)(arctan))`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then(((id Z)(#)(arctan))`|Z)= f by A10,PARTFUN1:5;
hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:95;
end;
::f.x=arccot.x - x/(1+x^2)
theorem
A c= Z & (for x st x in Z holds f1.x=1) & f=arccot-(id Z)/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies
integral(f,A)=((id Z)(#)(arccot)).(upper_bound A)-
((id Z)(#)(arccot)).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arccot-(id Z)/(f1+#Z 2)
& Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom arccot /\ dom ((id Z)/(f1+#Z 2)) by A1,VALUED_1:12;
then
A3:Z c= dom arccot & Z c= dom ((id Z)/(f1+#Z 2)) by XBOOLE_1:18;
then
Z c= dom (id Z) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;
then A4:Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
A5:(id Z)(#)(arccot) is_differentiable_on Z by A1,SIN_COS9:96;
A6:Z c= dom ((f1+#Z 2)^) by A4,RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A7:Z c= dom (f1+#Z 2) by A6;
A8:for x st x in Z holds f.x=arccot.x - x/(1+x^2)
proof
let x;
assume
A9: x in Z;
then (arccot-(id Z)/(f1+#Z 2)).x
=arccot.x-((id Z)/(f1+#Z 2)).x by A1,VALUED_1:13
.=arccot.x-(id Z).x/(f1+#Z 2).x by A3,A9,RFUNCT_1:def 1
.=arccot.x-x/(f1+#Z 2).x by A9,FUNCT_1:18
.=arccot.x-x/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1
.=arccot.x-x/(1+( #Z 2).x) by A1,A9
.=arccot.x-x/(1+(x #Z 2)) by TAYLOR_1:def 1
.=arccot.x-x/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A10:for x being Element of REAL st x in dom(((id Z)(#)(arccot))`|Z) holds
(((id Z)(#)(arccot))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((id Z)(#)(arccot))`|Z);then
A11:x in Z by A5,FDIFF_1:def 7;then
(((id Z)(#)(arccot))`|Z).x=arccot.x - x/(1+x^2) by A1,SIN_COS9:96
.=f.x by A11,A8;
hence thesis;
end;
dom(((id Z)(#)(arccot))`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then(((id Z)(#)(arccot))`|Z)= f by A10,PARTFUN1:5;
hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:96;
end;
::f.x=exp_R.(arctan.x)/(1+x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arctan/(f1+#Z 2)
& (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous
implies integral(f,A)=(exp_R*arctan).(upper_bound A) -
(exp_R*arctan).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arctan/(f1+#Z 2)
& (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (exp_R*arctan) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by A1,RFUNCT_1:def 1;then
A3:Z c= dom (exp_R*arctan) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
then A4:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A5:Z c= dom (f1+#Z 2) by A4;
A6:exp_R*arctan is_differentiable_on Z by A1,A3,SIN_COS9:119;
A7:for x st x in Z holds f.x=exp_R.(arctan.x)/(1+x^2)
proof
let x;
assume
A8:x in Z;
then (exp_R*arctan/(f1+#Z 2)).x
=(exp_R*arctan).x/(f1+#Z 2).x by A1,RFUNCT_1:def 1
.=exp_R.(arctan.x)/(f1+#Z 2).x by A3,A8,FUNCT_1:12
.=exp_R.(arctan.x)/(f1.x+( #Z 2).x) by A5,A8,VALUED_1:def 1
.=exp_R.(arctan.x)/(1+( #Z 2).x) by A1,A8
.=exp_R.(arctan.x)/(1+(x #Z 2)) by TAYLOR_1:def 1
.=exp_R.(arctan.x)/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A9: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
A10: x in Z by A6,FDIFF_1:def 7;then
((exp_R*arctan)`|Z).x=exp_R.(arctan.x)/(1+x^2) by A1,A3,SIN_COS9:119
.=f.x by A10,A7;
hence thesis;
end;
dom ((exp_R*arctan)`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((exp_R*arctan)`|Z)= f by A9,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13,SIN_COS9:119;
end;
::f.x=-exp_R.(arccot.x)/(1+x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & f=-exp_R*arccot/(f1+#Z 2)
& (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous
implies integral(f,A)=(exp_R*arccot).(upper_bound A) -
(exp_R*arccot).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ & f=-exp_R*arccot/(f1+#Z 2)
& (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z = dom (exp_R*arccot/(f1+#Z 2)) by A1,VALUED_1:8;
then Z = dom (exp_R*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by RFUNCT_1:def 1;then
A4:Z c= dom (exp_R*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
then A5:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A6:Z c= dom (f1+#Z 2) by A5;
A7:exp_R*arccot is_differentiable_on Z by A1,A4,SIN_COS9:120;
A8:for x st x in Z holds f.x=-exp_R.(arccot.x)/(1+x^2)
proof
let x;
assume
A9:x in Z;
(-exp_R*arccot/(f1+#Z 2)).x =-(exp_R*arccot/(f1+#Z 2)).x by VALUED_1:8
.=-(exp_R*arccot).x/(f1+#Z 2).x by A9,A3,RFUNCT_1:def 1
.=-exp_R.(arccot.x)/(f1+#Z 2).x by A4,A9,FUNCT_1:12
.=-exp_R.(arccot.x)/(f1.x+( #Z 2).x) by A6,A9,VALUED_1:def 1
.=-exp_R.(arccot.x)/(1+( #Z 2).x) by A1,A9
.=-exp_R.(arccot.x)/(1+(x #Z 2)) by TAYLOR_1:def 1
.=-exp_R.(arccot.x)/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A10: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
A11: x in Z by A7,FDIFF_1:def 7;then
((exp_R*arccot)`|Z).x=-exp_R.(arccot.x)/(1+x^2) by A1,A4,SIN_COS9:120
.=f.x by A11,A8;
hence thesis;
end;
dom ((exp_R*arccot)`|Z)=dom f by A1,A7,FDIFF_1:def 7;
then ((exp_R*arccot)`|Z)= f by A10,PARTFUN1:5;
hence thesis by A1,A2,A4,INTEGRA5:13,SIN_COS9:120;
end;
theorem Th50:
Z c= dom (exp_R*arccot) & Z c= ]. -1,1 .[ implies
-exp_R*arccot is_differentiable_on Z & for x st x in Z holds
((-exp_R*arccot)`|Z).x = exp_R.(arccot.x)/(1+x^2)
proof
assume
A1:Z c= dom (exp_R*arccot) & Z c= ]. -1,1 .[;
then A2:Z c= dom (-exp_R*arccot) by VALUED_1:8;
A3:exp_R*arccot is_differentiable_on Z by A1,SIN_COS9:120;
then A4:(-1)(#)(exp_R*arccot) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-exp_R*arccot)`|Z).x = exp_R.(arccot.x)/(1+x^2)
proof
let x;
assume
A5:x in Z;
A6:arccot is_differentiable_on Z by A1,SIN_COS9:82;then
A7:arccot is_differentiable_in x by A5,FDIFF_1:9;
A8:exp_R is_differentiable_in arccot.x by SIN_COS:65;
A9:exp_R*arccot is_differentiable_in x by A3,A5,FDIFF_1:9;
((-exp_R*arccot)`|Z).x=diff(-exp_R*arccot,x) by A4,A5,FDIFF_1:def 7
.=(-1)*(diff(exp_R*arccot,x)) by A9,FDIFF_1:15
.=(-1)*(diff(exp_R,arccot.x)*diff(arccot,x))
by A7,A8,FDIFF_2:13
.=(-1)*(diff(exp_R,arccot.x)*((arccot)`|Z).x)
by A5,A6,FDIFF_1:def 7
.=(-1)*(diff(exp_R,arccot.x)*(-1/(1+x^2)))
by A5,A1,SIN_COS9:82
.=(-1)*(-diff(exp_R,arccot.x)*(1/(1+x^2)))
.=exp_R.(arccot.x)/(1+x^2) by SIN_COS:65;
hence thesis;
end;
hence thesis by A2,A3,FDIFF_1:20;
end;
::f.x=exp_R.(arccot.x)/(1+x^2)
theorem
A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arccot/(f1+#Z 2)
& (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous
implies integral(f,A)=(-exp_R*arccot).(upper_bound A)
-(-exp_R*arccot).(lower_bound A)
proof
assume
A1:A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arccot/(f1+#Z 2)
& (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (exp_R*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0})
by A1,RFUNCT_1:def 1;then
A3:Z c= dom (exp_R*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18;
then A4:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2;
dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then
A5:Z c= dom (f1+#Z 2) by A4;
A6:-exp_R*arccot is_differentiable_on Z by A1,A3,Th50;
A7:for x st x in Z holds f.x=exp_R.(arccot.x)/(1+x^2)
proof
let x;
assume
A8:x in Z;
then (exp_R*arccot/(f1+#Z 2)).x
=(exp_R*arccot).x/(f1+#Z 2).x by A1,RFUNCT_1:def 1
.=exp_R.(arccot.x)/(f1+#Z 2).x by A3,A8,FUNCT_1:12
.=exp_R.(arccot.x)/(f1.x+( #Z 2).x) by A5,A8,VALUED_1:def 1
.=exp_R.(arccot.x)/(1+( #Z 2).x) by A1,A8
.=exp_R.(arccot.x)/(1+(x #Z 2)) by TAYLOR_1:def 1
.=exp_R.(arccot.x)/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A9: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
A10: x in Z by A6,FDIFF_1:def 7;then
((-exp_R*arccot)`|Z).x=exp_R.(arccot.x)/(1+x^2) by A1,A3,Th50
.=f.x by A7,A10;
hence thesis;
end;
dom ((-exp_R*arccot)`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((-exp_R*arccot)`|Z)= f by A9,PARTFUN1:5;
hence thesis by A1,A2,A3,Th50,INTEGRA5:13;
end;
::f.x=x/(1+x^2)
theorem
A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(f1+f2)
& f2=#Z 2 & (for x st x in Z holds f1.x=1) & Z = dom f
& f|A is continuous implies
integral(f,A)=((1/2)(#)(ln*(f1+f2))).(upper_bound A)
-((1/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(f1+f2)
& f2=#Z 2 & (for x st x in Z holds f1.x=1) & Z = dom f
& f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3: Z c= dom ((1/2)(#)(ln*(f1+f2))) by A1,VALUED_1:def 5;
Z c= dom (id Z) /\ (dom (f1+f2) \ (f1+f2)"{0}) by A1,RFUNCT_1:def 1; then
Z c= dom (f1+f2) \ (f1+f2)"{0} by XBOOLE_1:18;then
A4:Z c= dom ((f1+f2)^) by RFUNCT_1:def 2;
dom ((f1+f2)^) c= dom (f1+f2) by RFUNCT_1:1;then
A5:Z c= dom (f1+f2) by A4;
A6:(1/2)(#)(ln*(f1+f2)) is_differentiable_on Z by A1,A3,SIN_COS9:102;
A7: for x st x in Z holds f.x=x/(1+x^2)
proof
let x;
assume
A8: x in Z;
then ((id Z)/(f1+f2)).x=(id Z).x/(f1+f2).x by A1,RFUNCT_1:def 1
.=x/(f1+f2).x by A8,FUNCT_1:18
.=x/(f1.x+f2.x) by A5,A8,VALUED_1:def 1
.=x/(1+( #Z 2).x) by A1,A8
.=x/(1+(x #Z 2)) by TAYLOR_1:def 1
.=x/(1+x^2) by FDIFF_7:1;
hence thesis by A1;
end;
A9:for x being Element of REAL st x in dom(((1/2)(#)(ln*(f1+f2)))`|Z) holds
(((1/2)(#)(ln*(f1+f2)))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((1/2)(#)(ln*(f1+f2)))`|Z);then
A10: x in Z by A6,FDIFF_1:def 7;then
(((1/2)(#)(ln*(f1+f2)))`|Z).x=x/(1+x^2) by A1,A3,SIN_COS9:102
.=f.x by A10,A7;
hence thesis;
end;
dom(((1/2)(#)(ln*(f1+f2)))`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then(((1/2)(#)(ln*(f1+f2)))`|Z)= f by A9,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
::f.x=x/(a*(1+(x/a)^2))
theorem
A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(a(#)(f1+f2))
& (for x st x in Z holds h.x=x/a & f1.x=1)
& a <> 0 & f2=( #Z 2)*h & Z = dom f & f|A is continuous
implies integral(f,A)=((a/2)(#)(ln*(f1+f2))).(upper_bound A)
-((a/2)(#)(ln*(f1+f2))).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(a(#)(f1+f2))
& (for x st x in Z holds h.x=x/a & f1.x=1)
& a <> 0 & f2=( #Z 2)*h
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z c= dom ((a/2)(#)(ln*(f1+f2))) by A1,VALUED_1:def 5;
A4:for x st x in Z holds f1.x=1 by A1;
A5:for x st x in Z holds h.x=x/a by A1;
then
A6:((a/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A1,A3,A4,SIN_COS9:108;
A7:for x st x in Z holds f.x=x/(a*(1+(x/a)^2))
proof
let x;
assume
A8:x in Z; then
A9:x in dom (f1+f2) by A1,FUNCT_1:11;
dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;then
dom (f1+f2) c= dom f2 by XBOOLE_1:18;then
A10:x in dom f2 by A9;
((id Z)/(a(#)(f1+f2))).x=(id Z).x/(a(#)(f1+f2)).x by A1,A8,RFUNCT_1:def 1
.=x/(a(#)(f1+f2)).x by A8,FUNCT_1:18
.=x/(a*(f1+f2).x) by VALUED_1:6
.=x/(a*(f1.x+f2.x)) by A9,VALUED_1:def 1
.=x/(a*(1+f2.x)) by A4,A8
.=x/(a*(1+( #Z 2).(h.x))) by A1,A10,FUNCT_1:12
.=x/(a*(1+((h.x) #Z 2))) by TAYLOR_1:def 1
.=x/(a*(1+(h.x)^2)) by FDIFF_7:1
.=x/(a*(1+(x/a)^2)) by A5,A8;
hence thesis by A1;
end;
A11:for x being Element of REAL st x in dom(((a/2)(#)(ln*(f1+f2)))`|Z) holds
(((a/2)(#)(ln*(f1+f2)))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom(((a/2)(#)(ln*(f1+f2)))`|Z);then
A12: x in Z by A6,FDIFF_1:def 7;then
(((a/2)(#)(ln*(f1+f2)))`|Z).x
=x/(a*(1+(x/a)^2)) by A1,A3,A4,A5,SIN_COS9:108
.=f.x by A7,A12;
hence thesis;
end;
dom(((a/2)(#)(ln*(f1+f2)))`|Z) = dom f by A1,A6,FDIFF_1:def 7;
then (((a/2)(#)(ln*(f1+f2)))`|Z) = f by A11,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
theorem Th54:
Z c= dom ((id Z)^(#)arctan) & Z c= ]. -1,1 .[
implies (-(id Z)^(#)arctan) is_differentiable_on Z &
for x st x in Z holds
((-(id Z)^(#)arctan)`|Z).x = arctan.x/(x^2)-1/(x*(1+x^2))
proof
set f = id Z;
assume that
A1:Z c= dom (f^(#)arctan) and
A2: Z c= ]. -1,1 .[;
A3:Z c= dom (-f^(#)arctan) by A1,VALUED_1:8;
A4:for x st x in Z holds f.x=x by FUNCT_1:18;
Z c= dom (f^) /\ dom arctan by A1,VALUED_1:def 4;then
A5: Z c= dom (f^) by XBOOLE_1:18;
A6:not 0 in Z
proof
assume A7: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A7; then
not 0 in {0} by A7,A5,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end; then
A8:f^ is_differentiable_on Z & for x st x in Z holds
((f^)`|Z).x = -1/x^2 by FDIFF_5:4;
A9:arctan is_differentiable_on Z by A2,SIN_COS9:81;
A10:(f^(#)arctan) is_differentiable_on Z by A1,A2,A6,SIN_COS9:129;
then A11:(-1)(#)(f^(#)arctan) is_differentiable_on Z by A3,FDIFF_1:20;
for x st x in Z holds ((-f^(#)arctan)`|Z).x = arctan.x/(x^2)-1/(x*(1+x^2))
proof
let x;
assume
A12: x in Z;
then A13:(f^(#)arctan) is_differentiable_in x by A10,FDIFF_1:9;
A14:f^ is_differentiable_in x by A8,A12,FDIFF_1:9;
A15:arctan is_differentiable_in x by A9,A12,FDIFF_1:9;
((-f^(#)arctan)`|Z).x=diff(-f^(#)arctan,x) by A11,A12,FDIFF_1:def 7
.=(-1)*(diff(f^(#)arctan,x)) by A13,FDIFF_1:15
.=(-1)*((arctan.x)*diff(f^,x)+((f^).x)*diff(arctan,x))
by A14,A15,FDIFF_1:16
.=(-1)*((arctan.x)*((f^)`|Z).x+((f^).x)*diff(arctan,x))
by A8,A12,FDIFF_1:def 7
.=(-1)*((arctan.x)*(-1/x^2)+((f^).x)*diff(arctan,x))
by A6,A12,FDIFF_5:4
.=(-1)*(-(arctan.x)*(1/x^2)+((f^).x)*((arctan)`|Z).x)
by A9,A12,FDIFF_1:def 7
.=(-1)*(-((arctan.x)*1)/(x^2)+((f^).x)*(1/(1+x^2)))
by A2,A12,SIN_COS9:81
.=(-1)*(-arctan.x/(x^2)+(f.x)"*(1/(1+x^2)))
by A5,A12,RFUNCT_1:def 2
.=(-1)*(-arctan.x/(x^2)+(1/x)*(1/(1+x^2))) by A4,A12
.=(-1)*(-arctan.x/(x^2)+(1*1)/(x*(1+x^2))) by XCMPLX_1:76
.=arctan.x/(x^2)-1/(x*(1+x^2));
hence thesis;
end;
hence thesis by A3,A10,FDIFF_1:20;
end;
theorem Th55:
Z c= dom ((id Z)^(#)arccot) & Z c= ]. -1,1 .[
implies (-(id Z)^(#)arccot) is_differentiable_on Z &
for x st x in Z holds
((-(id Z)^(#)arccot)`|Z).x = arccot.x/(x^2)+1/(x*(1+x^2))
proof
set f = id Z;
assume that
A1:Z c= dom (f^(#)arccot) and
A2: Z c= ]. -1,1 .[;
A3:Z c= dom (-f^(#)arccot) by A1,VALUED_1:8;
A4:for x st x in Z holds f.x=x by FUNCT_1:18;
Z c= dom (f^) /\ dom arccot by A1,VALUED_1:def 4;then
A5:Z c= dom (f^) by XBOOLE_1:18;
A6:not 0 in Z
proof
assume A7: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A7; then
not 0 in {0} by A7,A5,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end; then
A8:f^ is_differentiable_on Z & for x st x in Z holds
((f^)`|Z).x = -1/x^2 by FDIFF_5:4;
A9:arccot is_differentiable_on Z by A2,SIN_COS9:82;
A10:(f^(#)arccot) is_differentiable_on Z by A6,A1,A2,SIN_COS9:130;
then A11:(-1)(#)(f^(#)arccot) is_differentiable_on Z by A3,FDIFF_1:20;
for x st x in Z holds ((-f^(#)arccot)`|Z).x = arccot.x/(x^2)+1/(x*(1+x^2))
proof
let x;
assume
A12: x in Z;
then A13: (f^(#)arccot) is_differentiable_in x by A10,FDIFF_1:9;
A14: f^ is_differentiable_in x by A8,A12,FDIFF_1:9;
A15: arccot is_differentiable_in x by A9,A12,FDIFF_1:9;
((-f^(#)arccot)`|Z).x=diff(-f^(#)arccot,x) by A11,A12,FDIFF_1:def 7
.=(-1)*(diff(f^(#)arccot,x)) by A13,FDIFF_1:15
.=(-1)*((arccot.x)*diff(f^,x)+((f^).x)*diff(arccot,x))
by A14,A15,FDIFF_1:16
.=(-1)*((arccot.x)*((f^)`|Z).x+((f^).x)*diff(arccot,x))
by A8,A12,FDIFF_1:def 7
.=(-1)*((arccot.x)*(-1/x^2)+((f^).x)*diff(arccot,x))
by A12,A6,FDIFF_5:4
.=(-1)*(-(arccot.x)*(1/x^2)+((f^).x)*((arccot)`|Z).x)
by A9,A12,FDIFF_1:def 7
.=(-1)*(-(arccot.x)*(1/x^2)+((f^).x)*(-1/(1+x^2)))
by A2,A12,SIN_COS9:82
.=(-1)*(-((arccot.x)*1)/(x^2)-((f^).x)*(1/(1+x^2)))
.=(-1)*(-arccot.x/(x^2)-(f.x)"*(1/(1+x^2)))
by A5,A12,RFUNCT_1:def 2
.=(-1)*(-arccot.x/(x^2)-(1/x)*(1/(1+x^2))) by A4,A12
.=(-1)*(-arccot.x/(x^2)-(1*1)/(x*(1+x^2))) by XCMPLX_1:76
.=arccot.x/(x^2)+1/(x*(1+x^2));
hence thesis;
end;
hence thesis by A11;
end;
::f.x=arctan.x/(x^2)-1/(x*(1+x^2))
theorem
A c= Z & (for x st x in Z holds f1.x=1)
& f=arctan/( #Z 2)-((id Z)(#)(f1+#Z 2))^
& Z c= dom ((id Z)^(#)arctan) & Z c= ]. -1,1 .[
& Z = dom f & f|A is continuous implies
integral(f,A)=(-(id Z)^(#)arctan).(upper_bound A)-
(-(id Z)^(#)arctan).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1)
& f=arctan/( #Z 2)-((id Z)(#)(f1+#Z 2))^
& Z c= dom ((id Z)^(#)arctan) & Z c= ]. -1,1 .[
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(-(id Z)^(#)arctan) is_differentiable_on Z by A1,Th54;
A4:Z=dom (arctan/( #Z 2)) /\ dom (((id Z)(#)(f1+#Z 2))^) by A1,VALUED_1:12;then
A5:Z c= dom (arctan/( #Z 2)) by XBOOLE_1:18;
A6:Z c= dom (((id Z)(#)(f1+#Z 2))^) by A4,XBOOLE_1:18;
dom (((id Z)(#)(f1+#Z 2))^) c= dom ((id Z)(#)(f1+#Z 2)) by RFUNCT_1:1;then
Z c= dom ((id Z)(#)(f1+#Z 2)) by A6;
then Z c= dom (id Z) /\ dom (f1+#Z 2) by VALUED_1:def 4;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:18;
A8:for x st x in Z holds f.x=arctan.x/(x^2)-1/(x*(1+x^2))
proof
let x;
assume
A9:x in Z;then
A10:x in dom (((id Z)(#)(f1+#Z 2))^) by A6;
(arctan/( #Z 2)-((id Z)(#)(f1+#Z 2))^).x
=(arctan/( #Z 2)).x-(((id Z)(#)(f1+#Z 2))^).x by A1,A9,VALUED_1:13
.=(arctan/( #Z 2)).x-1/(((id Z)(#)(f1+#Z 2)).x) by A10,RFUNCT_1:def 2
.=(arctan/( #Z 2)).x-1/((id Z).x*(f1+#Z 2).x) by VALUED_1:5
.=(arctan/( #Z 2)).x-1/((id Z).x*(f1.x+( #Z 2).x)) by A7,A9,VALUED_1:def 1
.=(arctan/( #Z 2)).x-1/(x*(f1.x+( #Z 2).x)) by A9,FUNCT_1:18
.=(arctan/( #Z 2)).x-1/(x*(1+( #Z 2).x)) by A1,A9
.=arctan.x/( #Z 2).x-1/(x*(1+( #Z 2).x)) by A9,A5,RFUNCT_1:def 1
.=arctan.x/(x #Z 2)-1/(x*(1+( #Z 2).x)) by TAYLOR_1:def 1
.=arctan.x/(x #Z 2)-1/(x*(1+( x #Z 2))) by TAYLOR_1:def 1
.=arctan.x/(x^2)-1/(x*(1+( x #Z 2))) by FDIFF_7:1
.=arctan.x/(x^2)-1/(x*(1+x^2)) by FDIFF_7:1;
hence thesis by A1;
end;
A11:for x being Element of REAL st x in dom((-(id Z)^(#)arctan)`|Z) holds
((-(id Z)^(#)arctan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((-(id Z)^(#)arctan)`|Z);then
A12: x in Z by A3,FDIFF_1:def 7;then
((-(id Z)^(#)arctan)`|Z).x=arctan.x/(x^2)-1/(x*(1+x^2)) by A1,Th54
.=f.x by A8,A12;
hence thesis;
end;
dom((-(id Z)^(#)arctan)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then((-(id Z)^(#)arctan)`|Z)= f by A11,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=arccot.x/(x^2)+1/(x*(1+x^2))
theorem
A c= Z & (for x st x in Z holds f1.x=1)
& f=arccot/( #Z 2)+((id Z)(#)(f1+#Z 2))^
& Z c= dom ((id Z)^(#)arccot) & Z c= ]. -1,1 .[
& Z = dom f & f|A is continuous implies
integral(f,A)=(-(id Z)^(#)arccot).(upper_bound A)-
(-(id Z)^(#)arccot).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f1.x=1)
& f=arccot/( #Z 2)+((id Z)(#)(f1+#Z 2))^
& Z c= dom ((id Z)^(#)arccot) & Z c= ]. -1,1 .[
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(-(id Z)^(#)arccot) is_differentiable_on Z by A1,Th55;
A4:Z=dom (arccot/( #Z 2)) /\ dom (((id Z)(#)(f1+#Z 2))^) by A1,VALUED_1:def 1;
then
A5:Z c= dom (arccot/( #Z 2)) by XBOOLE_1:18;
A6:Z c= dom (((id Z)(#)(f1+#Z 2))^) by A4,XBOOLE_1:18;
dom (((id Z)(#)(f1+#Z 2))^) c= dom ((id Z)(#)(f1+#Z 2)) by RFUNCT_1:1;then
Z c= dom ((id Z)(#)(f1+#Z 2)) by A6;
then Z c= dom (id Z) /\ dom (f1+#Z 2) by VALUED_1:def 4;then
A7:Z c= dom (f1+#Z 2) by XBOOLE_1:18;
A8:for x st x in Z holds f.x=arccot.x/(x^2)+1/(x*(1+x^2))
proof
let x;
assume
A9:x in Z;then
A10:x in dom (((id Z)(#)(f1+#Z 2))^) by A6;
(arccot/( #Z 2)+((id Z)(#)(f1+#Z 2))^).x
=(arccot/( #Z 2)).x+(((id Z)(#)(f1+#Z 2))^).x by A1,A9,VALUED_1:def 1
.=(arccot/( #Z 2)).x+1/(((id Z)(#)(f1+#Z 2)).x) by A10,RFUNCT_1:def 2
.=(arccot/( #Z 2)).x+1/((id Z).x*(f1+#Z 2).x) by VALUED_1:5
.=(arccot/( #Z 2)).x+1/((id Z).x*(f1.x+( #Z 2).x)) by A7,A9,VALUED_1:def 1
.=(arccot/( #Z 2)).x+1/(x*(f1.x+( #Z 2).x)) by A9,FUNCT_1:18
.=(arccot/( #Z 2)).x+1/(x*(1+( #Z 2).x)) by A1,A9
.=arccot.x/( #Z 2).x+1/(x*(1+( #Z 2).x)) by A9,A5,RFUNCT_1:def 1
.=arccot.x/(x #Z 2)+1/(x*(1+( #Z 2).x)) by TAYLOR_1:def 1
.=arccot.x/(x #Z 2)+1/(x*(1+( x #Z 2))) by TAYLOR_1:def 1
.=arccot.x/(x^2)+1/(x*(1+( x #Z 2))) by FDIFF_7:1
.=arccot.x/(x^2)+1/(x*(1+x^2)) by FDIFF_7:1;
hence thesis by A1;
end;
A11:for x being Element of REAL st x in dom((-(id Z)^(#)arccot)`|Z) holds
((-(id Z)^(#)arccot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom((-(id Z)^(#)arccot)`|Z);then
A12:x in Z by A3,FDIFF_1:def 7;then
((-(id Z)^(#)arccot)`|Z).x=arccot.x/(x^2)+1/(x*(1+x^2)) by A1,Th55
.=f.x by A12,A8;
hence thesis;
end;
dom((-(id Z)^(#)arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then((-(id Z)^(#)arccot)`|Z)= f by A11,PARTFUN1:5;
hence thesis by A1,A2,Th55,INTEGRA5:13;
end;