let A be non empty closed_interval Subset of REAL; for f, f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = (exp_R (#) arccot) - (exp_R / (f1 + (#Z 2))) holds
integral (f,A) = ((exp_R (#) arccot) . (upper_bound A)) - ((exp_R (#) arccot) . (lower_bound A))
let f, f1 be PartFunc of REAL,REAL; for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = (exp_R (#) arccot) - (exp_R / (f1 + (#Z 2))) holds
integral (f,A) = ((exp_R (#) arccot) . (upper_bound A)) - ((exp_R (#) arccot) . (lower_bound A))
let Z be open Subset of REAL; ( A c= Z & ( for x being Real 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)) )
assume A1:
( A c= Z & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z = dom f & f = (exp_R (#) arccot) - (exp_R / (f1 + (#Z 2))) )
; integral (f,A) = ((exp_R (#) arccot) . (upper_bound A)) - ((exp_R (#) arccot) . (lower_bound A))
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, FDIFF_1: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, INTEGRA5:11;
A10:
for x being Real st x in Z holds
f . x = ((exp_R . x) * (arccot . x)) - ((exp_R . x) / (1 + (x ^2)))
A12:
for x being Element of REAL st x in dom ((exp_R (#) arccot) `| Z) holds
((exp_R (#) arccot) `| Z) . x = f . x
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
integral (f,A) = ((exp_R (#) arccot) . (upper_bound A)) - ((exp_R (#) arccot) . (lower_bound A))
by A1, A9, INTEGRA5:13, SIN_COS9:124; verum