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 )) . (sup A)) - ((- (ln * arccos )) . (inf 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 )) . (sup A)) - ((- (ln * arccos )) . (inf 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 )) . (sup A)) - ((- (ln * arccos )) . (inf 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 )) . (sup A)) - ((- (ln * arccos )) . (inf 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;
A4:
dom (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos ) = (dom ((#R (1 / 2)) * (f1 - (#Z 2)))) /\ (dom arccos )
by VALUED_1:def 4;
A5:
( Z c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) & Z c= dom arccos )
by A3, XBOOLE_1:18, A4;
A6:
arccos is_differentiable_on Z
by A1, FDIFF_1:34, SIN_COS6:108;
set f2 = #Z 2;
A8:
for x being Real st x in Z holds
(f1 - (#Z 2)) . x > 0
A17:
for x being Real st x in Z holds
( f1 . x = 1 & (f1 - (#Z 2)) . x > 0 )
by A1, A8;
A18:
(#R (1 / 2)) * (f1 - (#Z 2)) is_differentiable_on Z
by A5, A17, FDIFF_7:22;
A19:
((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos is_differentiable_on Z
by A3, A6, A18, FDIFF_1:29;
A20:
for x being Real st x in Z holds
(((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos ) . x <> 0
by RFUNCT_1:13, A1;
A21:
f is_differentiable_on Z
by A1, A19, A20, FDIFF_2:22;
f | Z is continuous
by A21, FDIFF_1:33;
then A22:
f | A is continuous
by A1, FCONT_1:17;
A23:
( f is_integrable_on A & f | A is bounded )
by A1, A22, INTEGRA5:10, INTEGRA5:11;
A24:
for x being Real st x in Z holds
arccos . x > 0
by A1;
A25:
ln * arccos is_differentiable_on Z
by A1, A24, FDIFF_7:9;
A26:
Z c= dom (- (ln * arccos ))
by A1, VALUED_1:8;
A27:
(- 1) (#) (ln * arccos ) is_differentiable_on Z
by A25, A26, 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))
B3:
(
x in dom (f1 - (#Z 2)) &
(f1 - (#Z 2)) . x in dom (#R (1 / 2)) )
by FUNCT_1:21, B2, A5;
B4:
(f1 - (#Z 2)) . x in right_open_halfline 0
by B3, TAYLOR_1:def 4;
B5:
(
- 1
< x &
x < 1 )
by A1, XXREAL_1:4, B2;
(
0 < 1
+ x &
0 < 1
- x )
by XREAL_1:150, B5, 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 )) . (sup A)) - ((- (ln * arccos )) . (inf A))
by A1, A23, A27, INTEGRA5:13; verum