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