let a, b be Real; for n being Element of NAT holds ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)
let n be Element of NAT ; ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)
A1:
[#] REAL c= dom ((n + 1) (#) (#Z n))
by FUNCT_2:def 1;
A2:
dom (#Z n) = REAL
by FUNCT_2:def 1;
for x being Real st x in REAL holds
(#Z n) | REAL is_differentiable_in x
by TAYLOR_1:2;
then
#Z n is_differentiable_on REAL
by A2;
then A3:
((n + 1) (#) (#Z n)) | REAL is continuous
by A1, FDIFF_1:20, FDIFF_1:25;
A4:
min (a,b) <= a
by XXREAL_0:17;
A5:
[.(min (a,b)),(max (a,b)).] c= REAL
;
a <= max (a,b)
by XXREAL_0:25;
then
min (a,b) <= max (a,b)
by A4, XXREAL_0:2;
then A6:
(#Z (n + 1)) . (max (a,b)) = (integral (((n + 1) (#) (#Z n)),(min (a,b)),(max (a,b)))) + ((#Z (n + 1)) . (min (a,b)))
by A1, A3, A5, Th20, Th29;
A7:
( min (a,b) = a implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) )
( min (a,b) = b implies ((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b) )
proof
assume A9:
min (
a,
b)
= b
;
((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)
then A10:
max (
a,
b)
= a
by XXREAL_0:36;
(
b < a implies
((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (
((n + 1) (#) (#Z n)),
a,
b) )
proof
assume
b < a
;
((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)
then
integral (
((n + 1) (#) (#Z n)),
a,
b)
= - (integral (((n + 1) (#) (#Z n)),['b,a']))
by INTEGRA5:def 4;
then
(#Z (n + 1)) . a = (- (integral (((n + 1) (#) (#Z n)),a,b))) + ((#Z (n + 1)) . b)
by A4, A6, A9, A10, INTEGRA5:def 4;
hence
((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (
((n + 1) (#) (#Z n)),
a,
b)
;
verum
end;
hence
((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (
((n + 1) (#) (#Z n)),
a,
b)
by A4, A7, A9, XXREAL_0:1;
verum
end;
hence
((#Z (n + 1)) . b) - ((#Z (n + 1)) . a) = integral (((n + 1) (#) (#Z n)),a,b)
by A7, XXREAL_0:15; verum