let a, b be Real; (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
A1:
min (a,b) <= a
by XXREAL_0:17;
A2:
[.(min (a,b)),(max (a,b)).] c= REAL
;
( exp_R | REAL is continuous & a <= max (a,b) )
by XXREAL_0:25;
then A3:
exp_R . (max (a,b)) = (integral (exp_R,(min (a,b)),(max (a,b)))) + (exp_R . (min (a,b)))
by A1, A2, INTEGRA7:20, INTEGRA7:27, SIN_COS:47, XXREAL_0:2;
A4:
( min (a,b) = a implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) )
( min (a,b) = b implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) )
proof
assume A6:
min (
a,
b)
= b
;
(exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
then A7:
max (
a,
b)
= a
by XXREAL_0:36;
(
b < a implies
(exp_R . b) - (exp_R . a) = integral (
exp_R,
a,
b) )
proof
assume
b < a
;
(exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
then
integral (
exp_R,
a,
b)
= - (integral (exp_R,['b,a']))
by INTEGRA5:def 4;
then
exp_R . a = (- (integral (exp_R,a,b))) + (exp_R . b)
by A1, A3, A6, A7, INTEGRA5:def 4;
hence
(exp_R . b) - (exp_R . a) = integral (
exp_R,
a,
b)
;
verum
end;
hence
(exp_R . b) - (exp_R . a) = integral (
exp_R,
a,
b)
by A1, A4, A6, XXREAL_0:1;
verum
end;
hence
(exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
by A4, XXREAL_0:15; verum