let A be closed-interval Subset of REAL; for f1, f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = 1 & arccos . x > 0 ) ) & Z c= dom (ln * arccos) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) ^ holds
integral (f,A) = ((- (ln * arccos)) . (upper_bound A)) - ((- (ln * arccos)) . (lower_bound A))
let f1, f be PartFunc of REAL,REAL; for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = 1 & arccos . x > 0 ) ) & Z c= dom (ln * arccos) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) ^ holds
integral (f,A) = ((- (ln * arccos)) . (upper_bound A)) - ((- (ln * arccos)) . (lower_bound A))
let Z be open Subset of REAL; ( A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = 1 & arccos . x > 0 ) ) & Z c= dom (ln * arccos) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) ^ implies integral (f,A) = ((- (ln * arccos)) . (upper_bound A)) - ((- (ln * arccos)) . (lower_bound A)) )
assume A1:
( A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( f1 . x = 1 & arccos . x > 0 ) ) & Z c= dom (ln * arccos) & Z = dom f & f = (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) ^ )
; integral (f,A) = ((- (ln * arccos)) . (upper_bound A)) - ((- (ln * arccos)) . (lower_bound A))
set g = ((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos;
A3:
Z c= dom (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos)
by A1, RFUNCT_1:11;
dom (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) = (dom ((#R (1 / 2)) * (f1 - (#Z 2)))) /\ (dom arccos)
by VALUED_1:def 4;
then A5:
( Z c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) & Z c= dom arccos )
by A3, XBOOLE_1:18;
A6:
arccos is_differentiable_on Z
by A1, FDIFF_1:34, SIN_COS6:108;
set f2 = #Z 2;
for x being Real st x in Z holds
(f1 - (#Z 2)) . x > 0
then
for x being Real st x in Z holds
( f1 . x = 1 & (f1 - (#Z 2)) . x > 0 )
by A1;
then
(#R (1 / 2)) * (f1 - (#Z 2)) is_differentiable_on Z
by A5, FDIFF_7:22;
then A19:
((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos is_differentiable_on Z
by A3, A6, FDIFF_1:29;
for x being Real st x in Z holds
(((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) . x <> 0
by RFUNCT_1:13, A1;
then
f is_differentiable_on Z
by A1, A19, FDIFF_2:22;
then
f | Z is continuous
by FDIFF_1:33;
then
f | A is continuous
by A1, FCONT_1:17;
then A23:
( f is_integrable_on A & f | A is bounded )
by A1, INTEGRA5:10, INTEGRA5:11;
for x being Real st x in Z holds
arccos . x > 0
by A1;
then A25:
ln * arccos is_differentiable_on Z
by A1, FDIFF_7:9;
Z c= dom (- (ln * arccos))
by A1, VALUED_1:8;
then A27:
(- 1) (#) (ln * arccos) is_differentiable_on Z
by A25, FDIFF_1:28, X;
A28:
for x being Real st x in Z holds
((- (ln * arccos)) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x))
proof
let x be
Real;
( x in Z implies ((- (ln * arccos)) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x)) )
assume A29:
x in Z
;
((- (ln * arccos)) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x))
then A30:
(
- 1
< x &
x < 1 )
by A1, XXREAL_1:4;
A31:
arccos is_differentiable_in x
by A1, A29, FDIFF_1:16, SIN_COS6:108;
A32:
arccos . x > 0
by A1, A29;
A33:
ln * arccos is_differentiable_in x
by A25, A29, FDIFF_1:16;
((- (ln * arccos)) `| Z) . x =
diff (
(- (ln * arccos)),
x)
by A27, A29, FDIFF_1:def 8
.=
(- 1) * (diff ((ln * arccos),x))
by A33, FDIFF_1:23, X
.=
(- 1) * ((diff (arccos,x)) / (arccos . x))
by A31, A32, TAYLOR_1:20
.=
(- 1) * ((- (1 / (sqrt (1 - (x ^2))))) / (arccos . x))
by A30, SIN_COS6:108
.=
(- 1) * (- ((1 / (sqrt (1 - (x ^2)))) / (arccos . x)))
.=
1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
by XCMPLX_1:79
;
hence
((- (ln * arccos)) `| Z) . x = 1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
;
verum
end;
B1:
for x being Real st x in Z holds
f . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x))
proof
let x be
Real;
( x in Z implies f . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x)) )
assume B2:
x in Z
;
f . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x))
then B3:
(
x in dom (f1 - (#Z 2)) &
(f1 - (#Z 2)) . x in dom (#R (1 / 2)) )
by FUNCT_1:21, A5;
then B4:
(f1 - (#Z 2)) . x in right_open_halfline 0
by TAYLOR_1:def 4;
(
- 1
< x &
x < 1 )
by A1, XXREAL_1:4, B2;
then
(
0 < 1
+ x &
0 < 1
- x )
by XREAL_1:150, XREAL_1:52;
then B6:
0 < (1 + x) * (1 - x)
by XREAL_1:131;
((((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) ^) . x =
1
/ ((((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) . x)
by RFUNCT_1:def 8, A1, B2
.=
1
/ ((((#R (1 / 2)) * (f1 - (#Z 2))) . x) * (arccos . x))
by VALUED_1:5
.=
1
/ (((#R (1 / 2)) . ((f1 - (#Z 2)) . x)) * (arccos . x))
by FUNCT_1:22, A5, B2
.=
1
/ ((((f1 - (#Z 2)) . x) #R (1 / 2)) * (arccos . x))
by TAYLOR_1:def 4, B4
.=
1
/ ((((f1 . x) - ((#Z 2) . x)) #R (1 / 2)) * (arccos . x))
by VALUED_1:13, B3
.=
1
/ ((((f1 . x) - (x #Z 2)) #R (1 / 2)) * (arccos . x))
by TAYLOR_1:def 1
.=
1
/ ((((f1 . x) - (x ^2)) #R (1 / 2)) * (arccos . x))
by FDIFF_7:1
.=
1
/ (((1 - (x ^2)) #R (1 / 2)) * (arccos . x))
by A1, B2
.=
1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
by FDIFF_7:2, B6
;
hence
f . x = 1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
by A1;
verum
end;
A34:
for x being Real st x in dom ((- (ln * arccos)) `| Z) holds
((- (ln * arccos)) `| Z) . x = f . x
dom ((- (ln * arccos)) `| Z) = dom f
by A1, A27, FDIFF_1:def 8;
then
(- (ln * arccos)) `| Z = f
by A34, PARTFUN1:34;
hence
integral (f,A) = ((- (ln * arccos)) . (upper_bound A)) - ((- (ln * arccos)) . (lower_bound A))
by A1, A23, A27, INTEGRA5:13; verum