let A be non empty closed_interval Subset of REAL; for f, f2, g1, g2 being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & f = ((g1 + g2) ^) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = 1 / ((1 + (x ^2)) * (arccot . x)) & g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f holds
integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A))
let f, f2, g1, g2 be PartFunc of REAL,REAL; for Z being open Subset of REAL st A c= Z & f = ((g1 + g2) ^) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = 1 / ((1 + (x ^2)) * (arccot . x)) & g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f holds
integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A))
let Z be open Subset of REAL; ( A c= Z & f = ((g1 + g2) ^) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = 1 / ((1 + (x ^2)) * (arccot . x)) & g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f implies integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A)) )
assume A1:
( A c= Z & f = ((g1 + g2) ^) / f2 & f2 = arccot & Z c= ].(- 1),1.[ & g2 = #Z 2 & ( for x being Real st x in Z holds
( f . x = 1 / ((1 + (x ^2)) * (arccot . x)) & g1 . x = 1 & f2 . x > 0 ) ) & Z = dom f )
; integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A))
then
Z = (dom ((g1 + g2) ^)) /\ ((dom f2) \ (f2 " {0}))
by RFUNCT_1:def 1;
then A2:
( Z c= dom ((g1 + g2) ^) & Z c= (dom f2) \ (f2 " {0}) )
by XBOOLE_1:18;
for x being Real st x in Z holds
g1 . x = 1
by A1;
then A3:
(g1 + g2) ^ is_differentiable_on Z
by A1, A2, Th1;
A4:
f2 is_differentiable_on Z
by A1, SIN_COS9:82;
for x being Real st x in Z holds
f2 . x <> 0
by A1;
then
f is_differentiable_on Z
by A1, A3, A4, FDIFF_2:21;
then
f | Z is continuous
by FDIFF_1:25;
then A5:
f | A is continuous
by A1, FCONT_1:16;
A6:
Z c= dom (f2 ^)
by A2, RFUNCT_1:def 2;
dom (f2 ^) c= dom f2
by RFUNCT_1:1;
then A7:
Z c= dom f2
by A6;
A8:
for x being Real st x in Z holds
f2 . x > 0
by A1;
rng (f2 | Z) c= right_open_halfline 0
then
f2 .: Z c= dom ln
by RELAT_1:115, TAYLOR_1:18;
then A10:
Z c= dom (ln * arccot)
by A1, A7, FUNCT_1:101;
A11:
( f is_integrable_on A & f | A is bounded )
by A1, A5, INTEGRA5:10, INTEGRA5:11;
A12:
ln * arccot is_differentiable_on Z
by A1, A10, A8, SIN_COS9:90;
Z c= dom (- (ln * arccot))
by A10, VALUED_1:8;
then A13:
- (ln * arccot) is_differentiable_on Z
by A12, FDIFF_1:20;
A14:
for x being Real st x in Z holds
((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x))
proof
let x be
Real;
( x in Z implies ((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x)) )
assume A15:
x in Z
;
((- (ln * arccot)) `| Z) . x = 1 / ((1 + (x ^2)) * (arccot . x))
then A16:
(
- 1
< x &
x < 1 )
by A1, XXREAL_1:4;
arccot is_differentiable_on Z
by A1, SIN_COS9:82;
then A17:
arccot is_differentiable_in x
by A15, FDIFF_1:9;
A18:
arccot . x > 0
by A1, A15;
A19:
ln * arccot is_differentiable_in x
by A12, A15, FDIFF_1:9;
((- (ln * arccot)) `| Z) . x =
diff (
(- (ln * arccot)),
x)
by A13, A15, FDIFF_1:def 7
.=
(- 1) * (diff ((ln * arccot),x))
by A19, FDIFF_1:15
.=
(- 1) * ((diff (arccot,x)) / (arccot . x))
by A17, A18, TAYLOR_1:20
.=
(- 1) * ((- (1 / (1 + (x ^2)))) / (arccot . x))
by A16, SIN_COS9:76
.=
(1 / (1 + (x ^2))) / (arccot . x)
.=
1
/ ((1 + (x ^2)) * (arccot . x))
by XCMPLX_1:78
;
hence
((- (ln * arccot)) `| Z) . x = 1
/ ((1 + (x ^2)) * (arccot . x))
;
verum
end;
A20:
for x being Element of REAL st x in dom ((- (ln * arccot)) `| Z) holds
((- (ln * arccot)) `| Z) . x = f . x
dom ((- (ln * arccot)) `| Z) = dom f
by A1, A13, FDIFF_1:def 7;
then
(- (ln * arccot)) `| Z = f
by A20, PARTFUN1:5;
hence
integral (f,A) = ((- (ln * arccot)) . (upper_bound A)) - ((- (ln * arccot)) . (lower_bound A))
by A1, A11, A13, INTEGRA5:13; verum