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 & 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 f, f1 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;
A2:
Z c= dom (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos)
by A1, RFUNCT_1:1;
dom (((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) = (dom ((#R (1 / 2)) * (f1 - (#Z 2)))) /\ (dom arccos)
by VALUED_1:def 4;
then A3:
( Z c= dom ((#R (1 / 2)) * (f1 - (#Z 2))) & Z c= dom arccos )
by A2, XBOOLE_1:18;
A4:
arccos is_differentiable_on Z
by A1, FDIFF_1:26, SIN_COS6:106;
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 A3, FDIFF_7:22;
then A7:
((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos is_differentiable_on Z
by A2, A4, FDIFF_1:21;
for x being Real st x in Z holds
(((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) . x <> 0
by A1, RFUNCT_1:3;
then
f is_differentiable_on Z
by A1, A7, FDIFF_2:22;
then
f | Z is continuous
by FDIFF_1:25;
then
f | A is continuous
by A1, FCONT_1:16;
then A8:
( 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 A9:
ln * arccos is_differentiable_on Z
by A1, FDIFF_7:9;
Z c= dom (- (ln * arccos))
by A1, VALUED_1:8;
then A10:
(- 1) (#) (ln * arccos) is_differentiable_on Z
by A9, FDIFF_1:20;
A11:
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 A12:
x in Z
;
((- (ln * arccos)) `| Z) . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x))
then A13:
(
- 1
< x &
x < 1 )
by A1, XXREAL_1:4;
A14:
arccos is_differentiable_in x
by A1, A12, FDIFF_1:9, SIN_COS6:106;
A15:
arccos . x > 0
by A1, A12;
A16:
ln * arccos is_differentiable_in x
by A9, A12, FDIFF_1:9;
((- (ln * arccos)) `| Z) . x =
diff (
(- (ln * arccos)),
x)
by A10, A12, FDIFF_1:def 7
.=
(- 1) * (diff ((ln * arccos),x))
by A16, FDIFF_1:15
.=
(- 1) * ((diff (arccos,x)) / (arccos . x))
by A14, A15, TAYLOR_1:20
.=
(- 1) * ((- (1 / (sqrt (1 - (x ^2))))) / (arccos . x))
by A13, SIN_COS6:106
.=
(- 1) * (- ((1 / (sqrt (1 - (x ^2)))) / (arccos . x)))
.=
1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
by XCMPLX_1:78
;
hence
((- (ln * arccos)) `| Z) . x = 1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
;
verum
end;
A17:
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 A18:
x in Z
;
f . x = 1 / ((sqrt (1 - (x ^2))) * (arccos . x))
then A19:
(
x in dom (f1 - (#Z 2)) &
(f1 - (#Z 2)) . x in dom (#R (1 / 2)) )
by A3, FUNCT_1:11;
then A20:
(f1 - (#Z 2)) . x in right_open_halfline 0
by TAYLOR_1:def 4;
(
- 1
< x &
x < 1 )
by A1, A18, XXREAL_1:4;
then
(
0 < 1
+ x &
0 < 1
- x )
by XREAL_1:50, XREAL_1:148;
then A21:
0 < (1 + x) * (1 - x)
by XREAL_1:129;
((((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) ^) . x =
1
/ ((((#R (1 / 2)) * (f1 - (#Z 2))) (#) arccos) . x)
by A1, A18, RFUNCT_1:def 2
.=
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 A3, A18, FUNCT_1:12
.=
1
/ ((((f1 - (#Z 2)) . x) #R (1 / 2)) * (arccos . x))
by A20, TAYLOR_1:def 4
.=
1
/ ((((f1 . x) - ((#Z 2) . x)) #R (1 / 2)) * (arccos . x))
by A19, VALUED_1:13
.=
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, A18
.=
1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
by A21, FDIFF_7:2
;
hence
f . x = 1
/ ((sqrt (1 - (x ^2))) * (arccos . x))
by A1;
verum
end;
A22:
for x being Element of REAL st x in dom ((- (ln * arccos)) `| Z) holds
((- (ln * arccos)) `| Z) . x = f . x
dom ((- (ln * arccos)) `| Z) = dom f
by A1, A10, FDIFF_1:def 7;
then
(- (ln * arccos)) `| Z = f
by A22, PARTFUN1:5;
hence
integral (f,A) = ((- (ln * arccos)) . (upper_bound A)) - ((- (ln * arccos)) . (lower_bound A))
by A1, A8, A10, INTEGRA5:13; verum