:: ROLLE semantic presentation
begin
theorem Th1: :: ROLLE:1
for p, g being Real st p < g holds
for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f . p = f . g & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 )
proof
let p, g be Real; ::_thesis: ( p < g implies for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f . p = f . g & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 ) )
assume A1: p < g ; ::_thesis: for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f . p = f . g & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 )
reconsider Z = ].p,g.[ as open Subset of REAL ;
let f be PartFunc of REAL,REAL; ::_thesis: ( [.p,g.] c= dom f & f | [.p,g.] is continuous & f . p = f . g & f is_differentiable_on ].p,g.[ implies ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 ) )
assume that
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous and
A4: f . p = f . g and
A5: f is_differentiable_on ].p,g.[ ; ::_thesis: ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 )
A6: f .: [.p,g.] is compact by A2, A3, FCONT_1:29, RCOMP_1:6;
[.p,g.] is compact by RCOMP_1:6;
then A7: f .: [.p,g.] is real-bounded by A2, A3, FCONT_1:29, RCOMP_1:10;
p in [.p,g.] by A1, XXREAL_1:1;
then consider x1, x2 being real number such that
A8: x1 in [.p,g.] and
A9: x2 in [.p,g.] and
A10: f . x1 = upper_bound (f .: [.p,g.]) and
A11: f . x2 = lower_bound (f .: [.p,g.]) by A2, A3, FCONT_1:31, RCOMP_1:6;
reconsider x1 = x1, x2 = x2 as Real by XREAL_0:def_1;
p in { r where r is Real : ( p <= r & r <= g ) } by A1;
then p in [.p,g.] by RCOMP_1:def_1;
then f . p in f .: [.p,g.] by A2, FUNCT_1:def_6;
then A12: not f . x1 < f . x2 by A10, A11, A6, RCOMP_1:10, SEQ_4:11;
A13: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
then A14: ].p,g.[ c= dom f by A2, XBOOLE_1:1;
percases ( f . x1 = f . x2 or f . x2 < f . x1 ) by A12, XXREAL_0:1;
supposeA15: f . x1 = f . x2 ; ::_thesis: ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 )
p / 2 < g / 2 by A1, XREAL_1:74;
then ( (p / 2) + (g / 2) < (g / 2) + (g / 2) & (p / 2) + (p / 2) < (p / 2) + (g / 2) ) by XREAL_1:8;
then (p / 2) + (g / 2) in { r where r is Real : ( p < r & r < g ) } ;
then A16: (p / 2) + (g / 2) in Z by RCOMP_1:def_2;
f | [.p,g.] is V8() by A10, A11, A7, A15, RFUNCT_2:19;
then f | Z is V8() by PARTFUN2:38, XXREAL_1:25;
then (f `| Z) . ((p / 2) + (g / 2)) = 0 by A14, A16, FDIFF_1:22;
then diff (f,((p / 2) + (g / 2))) = 0 by A5, A16, FDIFF_1:def_7;
hence ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 ) by A16; ::_thesis: verum
end;
supposeA17: f . x2 < f . x1 ; ::_thesis: ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 )
A18: ( x2 in ].p,g.[ or x1 in ].p,g.[ )
proof
assume that
A19: not x2 in ].p,g.[ and
A20: not x1 in ].p,g.[ ; ::_thesis: contradiction
x1 in ].p,g.[ \/ {p,g} by A1, A8, XXREAL_1:128;
then x1 in {p,g} by A20, XBOOLE_0:def_3;
then A21: ( x1 = p or x1 = g ) by TARSKI:def_2;
x2 in ].p,g.[ \/ {p,g} by A1, A9, XXREAL_1:128;
then x2 in {p,g} by A19, XBOOLE_0:def_3;
hence contradiction by A4, A17, A21, TARSKI:def_2; ::_thesis: verum
end;
now__::_thesis:_(_(_x2_in_].p,g.[_&_x2_in_].p,g.[_&_diff_(f,x2)_=_0_)_or_(_x1_in_].p,g.[_&_x1_in_].p,g.[_&_diff_(f,x1)_=_0_)_)
percases ( x2 in ].p,g.[ or x1 in ].p,g.[ ) by A18;
caseA22: x2 in ].p,g.[ ; ::_thesis: ( x2 in ].p,g.[ & diff (f,x2) = 0 )
then consider N1 being Neighbourhood of x2 such that
A23: N1 c= Z by RCOMP_1:18;
consider r being real number such that
A24: 0 < r and
A25: N1 = ].(x2 - r),(x2 + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
deffunc H1( Element of NAT ) -> Element of REAL = r / ($1 + 2);
consider s2 being Real_Sequence such that
A26: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_s2_._n
let n be Element of NAT ; ::_thesis: 0 <> s2 . n
0 <> r / (n + 2) by A24, XREAL_1:139;
hence 0 <> s2 . n by A26; ::_thesis: verum
end;
then A27: s2 is non-zero by SEQ_1:5;
( s2 is convergent & lim s2 = 0 ) by A26, SEQ_4:31;
then reconsider h1 = s2 as non-zero 0 -convergent Real_Sequence by A27, FDIFF_1:def_1;
consider s1 being Real_Sequence such that
A28: rng s1 = {x2} by SEQ_1:6;
reconsider c = s1 as V8() Real_Sequence by A28, FUNCT_2:111;
A29: now__::_thesis:_for_n_being_Element_of_NAT_holds_c_._n_=_x2
let n be Element of NAT ; ::_thesis: c . n = x2
c . n in {x2} by A28, VALUED_0:28;
hence c . n = x2 by TARSKI:def_1; ::_thesis: verum
end;
deffunc H2( Element of NAT ) -> Element of REAL = - (r / ($1 + 2));
consider s3 being Real_Sequence such that
A30: for n being Element of NAT holds s3 . n = H2(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s3_._n_=_(-_r)_/_(n_+_2)
let n be Element of NAT ; ::_thesis: s3 . n = (- r) / (n + 2)
s3 . n = - (r / (n + 2)) by A30;
hence s3 . n = (- r) / (n + 2) ; ::_thesis: verum
end;
then A31: ( s3 is convergent & lim s3 = 0 ) by SEQ_4:31;
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_s3_._n
let n be Element of NAT ; ::_thesis: 0 <> s3 . n
- 0 <> - (r / (n + 2)) by A24, XREAL_1:139;
hence 0 <> s3 . n by A30; ::_thesis: verum
end;
then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as non-zero 0 -convergent Real_Sequence by A31, FDIFF_1:def_1;
A32: N1 c= dom f by A14, A23, XBOOLE_1:1;
A33: now__::_thesis:_for_n_being_Element_of_NAT_holds_x2_-_(r_/_(n_+_2))_in_N1
let n be Element of NAT ; ::_thesis: x2 - (r / (n + 2)) in N1
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A24, XREAL_1:76;
then A34: x2 - r < x2 - (r / (n + 2)) by XREAL_1:15;
x2 - (r / (n + 2)) < x2 + r by A24, XREAL_1:6;
then x2 - (r / (n + 2)) in { s where s is Real : ( x2 - r < s & s < x2 + r ) } by A34;
hence x2 - (r / (n + 2)) in N1 by A25, RCOMP_1:def_2; ::_thesis: verum
end;
A35: rng (h2 + c) c= N1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h2 + c) or y in N1 )
assume y in rng (h2 + c) ; ::_thesis: y in N1
then consider n being Element of NAT such that
A36: (h2 + c) . n = y by FUNCT_2:113;
y = (h2 . n) + (c . n) by A36, SEQ_1:7
.= (- (r / (n + 2))) + (c . n) by A30
.= x2 - (r / (n + 2)) by A29 ;
hence y in N1 by A33; ::_thesis: verum
end;
A37: now__::_thesis:_for_n_being_Element_of_NAT_holds_x2_+_(r_/_(n_+_2))_in_N1
let n be Element of NAT ; ::_thesis: x2 + (r / (n + 2)) in N1
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A24, XREAL_1:76;
then A38: x2 + (r / (n + 2)) < x2 + r by XREAL_1:6;
0 < r / (n + 2) by A24, XREAL_1:139;
then x2 - r < x2 + (r / (n + 2)) by A24, XREAL_1:6;
then x2 + (r / (n + 2)) in { s where s is Real : ( x2 - r < s & s < x2 + r ) } by A38;
hence x2 + (r / (n + 2)) in N1 by A25, RCOMP_1:def_2; ::_thesis: verum
end;
A39: rng (h1 + c) c= N1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h1 + c) or y in N1 )
assume y in rng (h1 + c) ; ::_thesis: y in N1
then consider n being Element of NAT such that
A40: (h1 + c) . n = y by FUNCT_2:113;
y = (h1 . n) + (c . n) by A40, SEQ_1:7
.= (r / (n + 2)) + (c . n) by A26
.= x2 + (r / (n + 2)) by A29 ;
hence y in N1 by A37; ::_thesis: verum
end;
A41: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_s2_._n
let n be Element of NAT ; ::_thesis: 0 < s2 . n
0 < r / (n + 2) by A24, XREAL_1:139;
hence 0 < s2 . n by A26; ::_thesis: verum
end;
A42: for n being Element of NAT holds 0 <= ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n
A43: ( 0 < h1 . n & (h1 ") . n = (h1 . n) " ) by A41, VALUED_1:10;
(h1 + c) . n in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n in N1 by A39;
then (h1 + c) . n in Z by A23;
then f . ((h1 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def_6;
then f . x2 <= f . ((h1 + c) . n) by A11, A7, SEQ_4:def_2;
then A44: 0 <= (f . ((h1 + c) . n)) - (f . x2) by XREAL_1:48;
now__::_thesis:_for_n1_being_Element_of_NAT_holds_(h1_+_c)_._n1_in_].p,g.[
let n1 be Element of NAT ; ::_thesis: (h1 + c) . n1 in ].p,g.[
(h1 + c) . n1 in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n1 in N1 by A39;
hence (h1 + c) . n1 in ].p,g.[ by A23; ::_thesis: verum
end;
then A45: rng (h1 + c) c= ].p,g.[ by FUNCT_2:114;
A46: rng c c= dom f by A2, A9, A28, ZFMISC_1:31;
((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n = ((h1 ") . n) * (((f /* (h1 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - ((f /* c) . n)) by A14, A45, FUNCT_2:108, XBOOLE_1:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . (c . n))) by A46, FUNCT_2:108
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . x2)) by A29 ;
hence 0 <= ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n by A44, A43; ::_thesis: verum
end;
A47: f is_differentiable_in x2 by A5, A22, FDIFF_1:9;
then ( (h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is convergent & diff (f,x2) = lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) ) by A32, A28, A39, FDIFF_1:12;
then A48: 0 <= diff (f,x2) by A42, SEQ_2:17;
A49: now__::_thesis:_for_n_being_Element_of_NAT_holds_s3_._n_<_0
let n be Element of NAT ; ::_thesis: s3 . n < 0
0 < r / (n + 2) by A24, XREAL_1:139;
then - (r / (n + 2)) < - 0 by XREAL_1:24;
hence s3 . n < 0 by A30; ::_thesis: verum
end;
A50: for n being Element of NAT holds ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n <= 0
proof
let n be Element of NAT ; ::_thesis: ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n <= 0
now__::_thesis:_for_n1_being_Element_of_NAT_holds_(h2_+_c)_._n1_in_].p,g.[
let n1 be Element of NAT ; ::_thesis: (h2 + c) . n1 in ].p,g.[
(h2 + c) . n1 in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n1 in N1 by A35;
hence (h2 + c) . n1 in ].p,g.[ by A23; ::_thesis: verum
end;
then A51: rng (h2 + c) c= ].p,g.[ by FUNCT_2:114;
h2 . n < 0 by A49;
then - 0 < - (h2 . n) by XREAL_1:24;
then 0 < 1 / (- (h2 . n)) ;
then ( (h2 ") . n = (h2 . n) " & 0 < - (1 / (h2 . n)) ) by VALUED_1:10, XCMPLX_1:188;
then A52: (h2 ") . n <= 0 ;
(h2 + c) . n in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n in N1 by A35;
then (h2 + c) . n in Z by A23;
then f . ((h2 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def_6;
then f . x2 <= f . ((h2 + c) . n) by A11, A7, SEQ_4:def_2;
then A53: 0 <= (f . ((h2 + c) . n)) - (f . x2) by XREAL_1:48;
A54: rng c c= dom f by A2, A9, A28, ZFMISC_1:31;
((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n = ((h2 ") . n) * (((f /* (h2 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - ((f /* c) . n)) by A14, A51, FUNCT_2:108, XBOOLE_1:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . (c . n))) by A54, FUNCT_2:108
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . x2)) by A29 ;
hence ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n <= 0 by A53, A52; ::_thesis: verum
end;
( (h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is convergent & diff (f,x2) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) ) by A47, A32, A28, A35, FDIFF_1:12;
hence ( x2 in ].p,g.[ & diff (f,x2) = 0 ) by A22, A48, A50, RFUNCT_2:7; ::_thesis: verum
end;
caseA55: x1 in ].p,g.[ ; ::_thesis: ( x1 in ].p,g.[ & diff (f,x1) = 0 )
then consider N1 being Neighbourhood of x1 such that
A56: N1 c= ].p,g.[ by RCOMP_1:18;
consider r being real number such that
A57: 0 < r and
A58: N1 = ].(x1 - r),(x1 + r).[ by RCOMP_1:def_6;
reconsider r = r as Real by XREAL_0:def_1;
deffunc H1( Element of NAT ) -> Element of REAL = r / ($1 + 2);
consider s2 being Real_Sequence such that
A59: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_s2_._n
let n be Element of NAT ; ::_thesis: 0 <> s2 . n
0 <> r / (n + 2) by A57, XREAL_1:139;
hence 0 <> s2 . n by A59; ::_thesis: verum
end;
then A60: s2 is non-zero by SEQ_1:5;
( s2 is convergent & lim s2 = 0 ) by A59, SEQ_4:31;
then reconsider h1 = s2 as non-zero 0 -convergent Real_Sequence by A60, FDIFF_1:def_1;
consider s1 being Real_Sequence such that
A61: rng s1 = {x1} by SEQ_1:6;
reconsider c = s1 as V8() Real_Sequence by A61, FUNCT_2:111;
A62: now__::_thesis:_for_n_being_Element_of_NAT_holds_c_._n_=_x1
let n be Element of NAT ; ::_thesis: c . n = x1
c . n in {x1} by A61, VALUED_0:28;
hence c . n = x1 by TARSKI:def_1; ::_thesis: verum
end;
deffunc H2( Element of NAT ) -> Element of REAL = - (r / ($1 + 2));
consider s3 being Real_Sequence such that
A63: for n being Element of NAT holds s3 . n = H2(n) from SEQ_1:sch_1();
now__::_thesis:_for_n_being_Element_of_NAT_holds_s3_._n_=_(-_r)_/_(n_+_2)
let n be Element of NAT ; ::_thesis: s3 . n = (- r) / (n + 2)
s3 . n = - (r / (n + 2)) by A63;
hence s3 . n = (- r) / (n + 2) ; ::_thesis: verum
end;
then A64: ( s3 is convergent & lim s3 = 0 ) by SEQ_4:31;
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_s3_._n
let n be Element of NAT ; ::_thesis: 0 <> s3 . n
- 0 <> - (r / (n + 2)) by A57, XREAL_1:139;
hence 0 <> s3 . n by A63; ::_thesis: verum
end;
then s3 is non-zero by SEQ_1:5;
then reconsider h2 = s3 as non-zero 0 -convergent Real_Sequence by A64, FDIFF_1:def_1;
A65: N1 c= dom f by A14, A56, XBOOLE_1:1;
A66: now__::_thesis:_for_n_being_Element_of_NAT_holds_x1_-_(r_/_(n_+_2))_in_N1
let n be Element of NAT ; ::_thesis: x1 - (r / (n + 2)) in N1
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A57, XREAL_1:76;
then A67: x1 - r < x1 - (r / (n + 2)) by XREAL_1:15;
x1 - (r / (n + 2)) < x1 + r by A57, XREAL_1:6;
then x1 - (r / (n + 2)) in { s where s is Real : ( x1 - r < s & s < x1 + r ) } by A67;
hence x1 - (r / (n + 2)) in N1 by A58, RCOMP_1:def_2; ::_thesis: verum
end;
A68: rng (h2 + c) c= N1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h2 + c) or y in N1 )
assume y in rng (h2 + c) ; ::_thesis: y in N1
then consider n being Element of NAT such that
A69: (h2 + c) . n = y by FUNCT_2:113;
y = (h2 . n) + (c . n) by A69, SEQ_1:7
.= (- (r / (n + 2))) + (c . n) by A63
.= x1 - (r / (n + 2)) by A62 ;
hence y in N1 by A66; ::_thesis: verum
end;
A70: now__::_thesis:_for_n_being_Element_of_NAT_holds_x1_+_(r_/_(n_+_2))_in_N1
let n be Element of NAT ; ::_thesis: x1 + (r / (n + 2)) in N1
0 + 1 <= n + 1 by XREAL_1:6;
then 1 < (n + 1) + 1 by NAT_1:13;
then r / (n + 2) < r / 1 by A57, XREAL_1:76;
then A71: x1 + (r / (n + 2)) < x1 + r by XREAL_1:6;
0 < r / (n + 2) by A57, XREAL_1:139;
then x1 - r < x1 + (r / (n + 2)) by A57, XREAL_1:6;
then x1 + (r / (n + 2)) in { s where s is Real : ( x1 - r < s & s < x1 + r ) } by A71;
hence x1 + (r / (n + 2)) in N1 by A58, RCOMP_1:def_2; ::_thesis: verum
end;
A72: rng (h1 + c) c= N1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h1 + c) or y in N1 )
assume y in rng (h1 + c) ; ::_thesis: y in N1
then consider n being Element of NAT such that
A73: (h1 + c) . n = y by FUNCT_2:113;
y = (h1 . n) + (c . n) by A73, SEQ_1:7
.= (r / (n + 2)) + (c . n) by A59
.= x1 + (r / (n + 2)) by A62 ;
hence y in N1 by A70; ::_thesis: verum
end;
A74: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_s2_._n
let n be Element of NAT ; ::_thesis: 0 < s2 . n
0 < r / (n + 2) by A57, XREAL_1:139;
hence 0 < s2 . n by A59; ::_thesis: verum
end;
A75: for n being Element of NAT holds ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n <= 0
proof
let n be Element of NAT ; ::_thesis: ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n <= 0
A76: ( 0 < h1 . n & (h1 ") . n = (h1 . n) " ) by A74, VALUED_1:10;
(h1 + c) . n in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n in N1 by A72;
then (h1 + c) . n in Z by A56;
then f . ((h1 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def_6;
then f . ((h1 + c) . n) <= f . x1 by A10, A7, SEQ_4:def_1;
then 0 <= (f . x1) - (f . ((h1 + c) . n)) by XREAL_1:48;
then A77: - ((f . x1) - (f . ((h1 + c) . n))) <= - 0 ;
now__::_thesis:_for_n1_being_Element_of_NAT_holds_(h1_+_c)_._n1_in_].p,g.[
let n1 be Element of NAT ; ::_thesis: (h1 + c) . n1 in ].p,g.[
(h1 + c) . n1 in rng (h1 + c) by VALUED_0:28;
then (h1 + c) . n1 in N1 by A72;
hence (h1 + c) . n1 in ].p,g.[ by A56; ::_thesis: verum
end;
then A78: rng (h1 + c) c= ].p,g.[ by FUNCT_2:114;
A79: rng c c= dom f by A2, A8, A61, ZFMISC_1:31;
((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n = ((h1 ") . n) * (((f /* (h1 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h1 ") . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - ((f /* c) . n)) by A14, A78, FUNCT_2:108, XBOOLE_1:1
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . (c . n))) by A79, FUNCT_2:108
.= ((h1 ") . n) * ((f . ((h1 + c) . n)) - (f . x1)) by A62 ;
hence ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) . n <= 0 by A77, A76; ::_thesis: verum
end;
A80: f is_differentiable_in x1 by A5, A55, FDIFF_1:9;
then ( (h1 ") (#) ((f /* (h1 + c)) - (f /* c)) is convergent & diff (f,x1) = lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) ) by A65, A61, A72, FDIFF_1:12;
then A81: diff (f,x1) <= 0 by A75, RFUNCT_2:7;
A82: now__::_thesis:_for_n_being_Element_of_NAT_holds_s3_._n_<_0
let n be Element of NAT ; ::_thesis: s3 . n < 0
0 < r / (n + 2) by A57, XREAL_1:139;
then - (r / (n + 2)) < - 0 by XREAL_1:24;
hence s3 . n < 0 by A63; ::_thesis: verum
end;
A83: for n being Element of NAT holds 0 <= ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n
now__::_thesis:_for_n1_being_Element_of_NAT_holds_(h2_+_c)_._n1_in_].p,g.[
let n1 be Element of NAT ; ::_thesis: (h2 + c) . n1 in ].p,g.[
(h2 + c) . n1 in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n1 in N1 by A68;
hence (h2 + c) . n1 in ].p,g.[ by A56; ::_thesis: verum
end;
then A84: rng (h2 + c) c= ].p,g.[ by FUNCT_2:114;
h2 . n < 0 by A82;
then - 0 < - (h2 . n) by XREAL_1:24;
then 0 < 1 / (- (h2 . n)) ;
then ( (h2 ") . n = (h2 . n) " & 0 < - (1 / (h2 . n)) ) by VALUED_1:10, XCMPLX_1:188;
then A85: (h2 ") . n <= 0 ;
(h2 + c) . n in rng (h2 + c) by VALUED_0:28;
then (h2 + c) . n in N1 by A68;
then (h2 + c) . n in Z by A56;
then f . ((h2 + c) . n) in f .: [.p,g.] by A13, A14, FUNCT_1:def_6;
then f . ((h2 + c) . n) <= f . x1 by A10, A7, SEQ_4:def_1;
then 0 <= (f . x1) - (f . ((h2 + c) . n)) by XREAL_1:48;
then A86: - ((f . x1) - (f . ((h2 + c) . n))) <= - 0 ;
A87: rng c c= dom f by A2, A8, A61, ZFMISC_1:31;
((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n = ((h2 ") . n) * (((f /* (h2 + c)) - (f /* c)) . n) by SEQ_1:8
.= ((h2 ") . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n)) by RFUNCT_2:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - ((f /* c) . n)) by A14, A84, FUNCT_2:108, XBOOLE_1:1
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . (c . n))) by A87, FUNCT_2:108
.= ((h2 ") . n) * ((f . ((h2 + c) . n)) - (f . x1)) by A62 ;
hence 0 <= ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) . n by A86, A85; ::_thesis: verum
end;
( (h2 ") (#) ((f /* (h2 + c)) - (f /* c)) is convergent & diff (f,x1) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c))) ) by A80, A65, A61, A68, FDIFF_1:12;
hence ( x1 in ].p,g.[ & diff (f,x1) = 0 ) by A55, A81, A83, SEQ_2:17; ::_thesis: verum
end;
end;
end;
hence ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = 0 ) ; ::_thesis: verum
end;
end;
end;
theorem :: ROLLE:2
for x, t being Real st 0 < t holds
for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 )
proof
let x, t be Real; ::_thesis: ( 0 < t implies for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 ) )
assume A1: 0 < t ; ::_thesis: for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 )
let f be PartFunc of REAL,REAL; ::_thesis: ( [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ implies ex s being Real st
( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 ) )
assume ( [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f . x = f . (x + t) & f is_differentiable_on ].x,(x + t).[ ) ; ::_thesis: ex s being Real st
( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 )
then consider x0 being Real such that
A2: x0 in ].x,(x + t).[ and
A3: diff (f,x0) = 0 by A1, Th1, XREAL_1:29;
take s = (x0 - x) / t; ::_thesis: ( 0 < s & s < 1 & diff (f,(x + (s * t))) = 0 )
x0 in { r where r is Real : ( x < r & r < x + t ) } by A2, RCOMP_1:def_2;
then A4: ex g being Real st
( g = x0 & x < g & g < x + t ) ;
then 0 < x0 - x by XREAL_1:50;
then 0 / t < (x0 - x) / t by A1, XREAL_1:74;
hence 0 < s ; ::_thesis: ( s < 1 & diff (f,(x + (s * t))) = 0 )
x0 - x < t by A4, XREAL_1:19;
then (x0 - x) / t < t / t by A1, XREAL_1:74;
hence s < 1 by A1, XCMPLX_1:60; ::_thesis: diff (f,(x + (s * t))) = 0
(s * t) + x = (x0 - x) + x by A1, XCMPLX_1:87;
hence diff (f,(x + (s * t))) = 0 by A3; ::_thesis: verum
end;
theorem Th3: :: ROLLE:3
for p, g being Real st p < g holds
for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
proof
let p, g be Real; ::_thesis: ( p < g implies for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) )
assume A1: p < g ; ::_thesis: for f being PartFunc of REAL,REAL st [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
A2: 0 <> g - p by A1;
reconsider Z = ].p,g.[ as open Subset of REAL ;
defpred S1[ set ] means $1 in [.p,g.];
let f be PartFunc of REAL,REAL; ::_thesis: ( [.p,g.] c= dom f & f | [.p,g.] is continuous & f is_differentiable_on ].p,g.[ implies ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) )
assume that
A3: [.p,g.] c= dom f and
A4: f | [.p,g.] is continuous and
A5: f is_differentiable_on ].p,g.[ ; ::_thesis: ex x0 being Real st
( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
set r = ((f . g) - (f . p)) / (g - p);
deffunc H1( Real) -> Element of REAL = (((f . g) - (f . p)) / (g - p)) * ($1 - p);
consider f1 being PartFunc of REAL,REAL such that
A6: ( ( for x being Real holds
( x in dom f1 iff S1[x] ) ) & ( for x being Real st x in dom f1 holds
f1 . x = H1(x) ) ) from SEQ_1:sch_3();
set f2 = f - f1;
A7: [.p,g.] c= dom f1
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [.p,g.] or y in dom f1 )
assume y in [.p,g.] ; ::_thesis: y in dom f1
hence y in dom f1 by A6; ::_thesis: verum
end;
then A8: [.p,g.] c= (dom f) /\ (dom f1) by A3, XBOOLE_1:19;
then A9: [.p,g.] c= dom (f - f1) by VALUED_1:12;
[.p,g.] = ].p,g.[ \/ {p,g} by A1, XXREAL_1:128;
then A10: {p,g} c= [.p,g.] by XBOOLE_1:7;
then A11: p in [.p,g.] by ZFMISC_1:32;
then A12: p in dom f1 by A6;
[.p,g.] c= (dom f) /\ (dom f1) by A3, A7, XBOOLE_1:19;
then A13: [.p,g.] c= dom (f - f1) by VALUED_1:12;
then A14: (f - f1) . p = (f . p) - (f1 . p) by A11, VALUED_1:13
.= (f . p) - ((((f . g) - (f . p)) / (g - p)) * (p - p)) by A6, A12
.= f . p ;
A15: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
then A16: Z c= dom f1 by A7, XBOOLE_1:1;
A17: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
f1_._x_=_((((f_._g)_-_(f_._p))_/_(g_-_p))_*_x)_+_(-_((((f_._g)_-_(f_._p))_/_(g_-_p))_*_p))
let x be Real; ::_thesis: ( x in Z implies f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) )
assume x in Z ; ::_thesis: f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))
then x in dom f1 by A15, A6;
hence f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) by A6
.= ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) ;
::_thesis: verum
end;
then A18: f1 is_differentiable_on Z by A16, FDIFF_1:23;
now__::_thesis:_for_x_being_real_number_st_x_in_[.p,g.]_holds_
f1_._x_=_((((f_._g)_-_(f_._p))_/_(g_-_p))_*_x)_+_(-_((((f_._g)_-_(f_._p))_/_(g_-_p))_*_p))
let x be real number ; ::_thesis: ( x in [.p,g.] implies f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) )
assume x in [.p,g.] ; ::_thesis: f1 . x = ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p))
then x in dom f1 by A6;
hence f1 . x = (((f . g) - (f . p)) / (g - p)) * (x - p) by A6
.= ((((f . g) - (f . p)) / (g - p)) * x) + (- ((((f . g) - (f . p)) / (g - p)) * p)) ;
::_thesis: verum
end;
then f1 | [.p,g.] is continuous by FCONT_1:41;
then A19: (f - f1) | [.p,g.] is continuous by A4, A8, FCONT_1:18;
A20: g in [.p,g.] by A10, ZFMISC_1:32;
then A21: g in dom f1 by A6;
Z c= dom f by A3, A15, XBOOLE_1:1;
then Z c= (dom f) /\ (dom f1) by A16, XBOOLE_1:19;
then A22: Z c= dom (f - f1) by VALUED_1:12;
(f - f1) . g = (f . g) - (f1 . g) by A20, A13, VALUED_1:13
.= (f . g) - ((((f . g) - (f . p)) / (g - p)) * (g - p)) by A6, A21
.= (f . g) - ((f . g) - (f . p)) by A2, XCMPLX_1:87
.= (f - f1) . p by A14 ;
then consider x0 being Real such that
A23: x0 in ].p,g.[ and
A24: diff ((f - f1),x0) = 0 by A1, A5, A18, A9, A19, A22, Th1, FDIFF_1:19;
take x0 ; ::_thesis: ( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) )
f - f1 is_differentiable_on Z by A5, A18, A22, FDIFF_1:19;
then diff ((f - f1),x0) = ((f - f1) `| Z) . x0 by A23, FDIFF_1:def_7
.= (diff (f,x0)) - (diff (f1,x0)) by A5, A18, A22, A23, FDIFF_1:19
.= (diff (f,x0)) - ((f1 `| Z) . x0) by A18, A23, FDIFF_1:def_7 ;
hence ( x0 in ].p,g.[ & diff (f,x0) = ((f . g) - (f . p)) / (g - p) ) by A16, A17, A23, A24, FDIFF_1:23; ::_thesis: verum
end;
theorem :: ROLLE:4
for x, t being Real st 0 < t holds
for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
proof
let x, t be Real; ::_thesis: ( 0 < t implies for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) ) )
assume A1: 0 < t ; ::_thesis: for f being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ holds
ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
let f be PartFunc of REAL,REAL; ::_thesis: ( [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ implies ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) ) )
assume ( [.x,(x + t).] c= dom f & f | [.x,(x + t).] is continuous & f is_differentiable_on ].x,(x + t).[ ) ; ::_thesis: ex s being Real st
( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
then consider x0 being Real such that
A2: x0 in ].x,(x + t).[ and
A3: diff (f,x0) = ((f . (x + t)) - (f . x)) / ((x + t) - x) by A1, Th3, XREAL_1:29;
take s = (x0 - x) / t; ::_thesis: ( 0 < s & s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
x0 in { r where r is Real : ( x < r & r < x + t ) } by A2, RCOMP_1:def_2;
then A4: ex g being Real st
( g = x0 & x < g & g < x + t ) ;
then 0 < x0 - x by XREAL_1:50;
then 0 / t < (x0 - x) / t by A1, XREAL_1:74;
hence 0 < s ; ::_thesis: ( s < 1 & f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) )
x0 - x < t by A4, XREAL_1:19;
then (x0 - x) / t < t / t by A1, XREAL_1:74;
hence s < 1 by A1, XCMPLX_1:60; ::_thesis: f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t)))))
A5: (s * t) + x = (x0 - x) + x by A1, XCMPLX_1:87;
(f . x) + (t * (diff (f,x0))) = (f . x) + ((f . (x + t)) - (f . x)) by A1, A3, XCMPLX_1:87;
hence f . (x + t) = (f . x) + (t * (diff (f,(x + (s * t))))) by A5; ::_thesis: verum
end;
theorem Th5: :: ROLLE:5
for p, g being Real st p < g holds
for f1, f2 being PartFunc of REAL,REAL st [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
proof
let p, g be Real; ::_thesis: ( p < g implies for f1, f2 being PartFunc of REAL,REAL st [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) )
assume A1: p < g ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ implies ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) )
assume that
A2: [.p,g.] c= dom f1 and
A3: [.p,g.] c= dom f2 and
A4: f1 | [.p,g.] is continuous and
A5: f1 is_differentiable_on ].p,g.[ and
A6: f2 | [.p,g.] is continuous and
A7: f2 is_differentiable_on ].p,g.[ ; ::_thesis: ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
A8: ].p,g.[ c= [.p,g.] by XXREAL_1:25;
now__::_thesis:_ex_x0_being_Real_st_
(_x0_in_].p,g.[_&_((f1_._g)_-_(f1_._p))_*_(diff_(f2,x0))_=_((f2_._g)_-_(f2_._p))_*_(diff_(f1,x0))_)
percases ( f2 . p = f2 . g or f2 . p <> f2 . g ) ;
supposeA9: f2 . p = f2 . g ; ::_thesis: ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
then consider x0 being Real such that
A10: ( x0 in ].p,g.[ & diff (f2,x0) = 0 ) by A1, A3, A6, A7, Th1;
take x0 = x0; ::_thesis: ( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
thus ( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) by A9, A10; ::_thesis: verum
end;
suppose f2 . p <> f2 . g ; ::_thesis: ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
then A11: (f2 . g) - (f2 . p) <> 0 ;
reconsider Z = ].p,g.[ as open Subset of REAL ;
set s = ((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p));
reconsider f3 = [.p,g.] --> ((f1 . p) - ((f2 . p) * (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))))) as PartFunc of [.p,g.],REAL by FUNCOP_1:45;
reconsider f3 = f3 as PartFunc of REAL,REAL ;
set f4 = (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2;
set f5 = f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2);
set f = (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1;
A12: Z c= dom f3 by A8, FUNCOP_1:13;
A13: dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) = dom f2 by VALUED_1:def_5;
then A14: Z c= dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) by A3, A8, XBOOLE_1:1;
then Z c= (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by A12, XBOOLE_1:19;
then A15: Z c= dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by VALUED_1:def_1;
A16: [.p,g.] = dom f3 by FUNCOP_1:13;
then for x being Real st x in [.p,g.] /\ (dom f3) holds
f3 . x = (f1 . p) - ((f2 . p) * (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p)))) by FUNCOP_1:7;
then A17: f3 | [.p,g.] is V8() by PARTFUN2:57;
then A18: f3 | ].p,g.[ is V8() by PARTFUN2:38, XXREAL_1:25;
then A19: f3 is_differentiable_on Z by A12, FDIFF_1:22;
A20: p in [.p,g.] by A1, XXREAL_1:1;
then p in (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by A3, A16, A13, XBOOLE_0:def_4;
then A21: p in dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by VALUED_1:def_1;
then p in (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1) by A2, A20, XBOOLE_0:def_4;
then p in dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by VALUED_1:12;
then A22: ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) . p = ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) . p) - (f1 . p) by VALUED_1:13
.= ((f3 . p) + (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) . p)) - (f1 . p) by A21, VALUED_1:def_1
.= ((f3 . p) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) - (f1 . p) by A3, A13, A20, VALUED_1:def_5
.= (((f1 . p) - ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) - (f1 . p) by A20, FUNCOP_1:7
.= 0 ;
A23: g in [.p,g.] by A1, XXREAL_1:1;
then g in (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by A3, A16, A13, XBOOLE_0:def_4;
then A24: g in dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by VALUED_1:def_1;
then g in (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1) by A2, A23, XBOOLE_0:def_4;
then g in dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by VALUED_1:12;
then A25: ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) . g = ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) . g) - (f1 . g) by VALUED_1:13
.= ((f3 . g) + (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) . g)) - (f1 . g) by A24, VALUED_1:def_1
.= ((f3 . g) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . g))) - (f1 . g) by A3, A13, A23, VALUED_1:def_5
.= (((f1 . p) - ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . g))) - (f1 . g) by A23, FUNCOP_1:7
.= (- (f1 . g)) + ((f1 . p) - (((- ((f1 . g) - (f1 . p))) / ((f2 . g) - (f2 . p))) * ((f2 . g) - (f2 . p))))
.= (- (f1 . g)) + ((f1 . p) - ((f1 . p) - (f1 . g))) by A11, XCMPLX_1:87
.= ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) . p by A22 ;
Z c= dom f1 by A2, A8, XBOOLE_1:1;
then Z c= (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1) by A15, XBOOLE_1:19;
then A26: Z c= dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by VALUED_1:12;
dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) = dom f2 by VALUED_1:def_5;
then A27: [.p,g.] c= (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by A3, A16, XBOOLE_1:19;
then [.p,g.] c= dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by VALUED_1:def_1;
then A28: [.p,g.] c= (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1) by A2, XBOOLE_1:19;
((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) | [.p,g.] is continuous by A3, A6, FCONT_1:20;
then (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) | [.p,g.] is continuous by A17, A27, FCONT_1:18;
then A29: ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) | [.p,g.] is continuous by A4, A28, FCONT_1:18;
A30: (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2 is_differentiable_on Z by A7, A14, FDIFF_1:20;
then A31: f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) is_differentiable_on Z by A19, A15, FDIFF_1:18;
[.p,g.] c= dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by A28, VALUED_1:12;
then consider x0 being Real such that
A32: x0 in ].p,g.[ and
A33: diff (((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1),x0) = 0 by A1, A5, A29, A31, A26, A25, Th1, FDIFF_1:19;
take x0 = x0; ::_thesis: ( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
(f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1 is_differentiable_on Z by A5, A31, A26, FDIFF_1:19;
then diff (((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1),x0) = (((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) `| Z) . x0 by A32, FDIFF_1:def_7
.= (diff ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)),x0)) - (diff (f1,x0)) by A5, A31, A26, A32, FDIFF_1:19
.= (((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) `| Z) . x0) - (diff (f1,x0)) by A31, A32, FDIFF_1:def_7
.= ((diff (f3,x0)) + (diff (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0))) - (diff (f1,x0)) by A19, A30, A15, A32, FDIFF_1:18
.= (((f3 `| Z) . x0) + (diff (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0))) - (diff (f1,x0)) by A19, A32, FDIFF_1:def_7
.= (0 + (diff (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0))) - (diff (f1,x0)) by A18, A12, A32, FDIFF_1:22
.= ((((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) `| Z) . x0) - (diff (f1,x0)) by A30, A32, FDIFF_1:def_7
.= ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (diff (f2,x0))) - (diff (f1,x0)) by A7, A14, A32, FDIFF_1:20 ;
then (((diff (f2,x0)) * ((f1 . g) - (f1 . p))) / ((f2 . g) - (f2 . p))) * ((f2 . g) - (f2 . p)) = (diff (f1,x0)) * ((f2 . g) - (f2 . p)) by A33, XCMPLX_1:15;
hence ( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) by A11, A32, XCMPLX_1:87; ::_thesis: verum
end;
end;
end;
hence ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) ; ::_thesis: verum
end;
theorem :: ROLLE:6
for x, t being Real st 0 < t holds
for f1, f2 being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff (f2,x1) <> 0 ) holds
ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) )
proof
let x, t be Real; ::_thesis: ( 0 < t implies for f1, f2 being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff (f2,x1) <> 0 ) holds
ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) ) )
assume A1: 0 < t ; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff (f2,x1) <> 0 ) holds
ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( [.x,(x + t).] c= dom f1 & [.x,(x + t).] c= dom f2 & f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ & f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ & ( for x1 being Real st x1 in ].x,(x + t).[ holds
diff (f2,x1) <> 0 ) implies ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) ) )
assume that
A2: [.x,(x + t).] c= dom f1 and
A3: [.x,(x + t).] c= dom f2 and
A4: ( f1 | [.x,(x + t).] is continuous & f1 is_differentiable_on ].x,(x + t).[ ) and
A5: ( f2 | [.x,(x + t).] is continuous & f2 is_differentiable_on ].x,(x + t).[ ) and
A6: for x1 being Real st x1 in ].x,(x + t).[ holds
diff (f2,x1) <> 0 ; ::_thesis: ex s being Real st
( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) )
consider x0 being Real such that
A7: x0 in ].x,(x + t).[ and
A8: ((f1 . (x + t)) - (f1 . x)) * (diff (f2,x0)) = ((f2 . (x + t)) - (f2 . x)) * (diff (f1,x0)) by A1, A2, A3, A4, A5, Th5, XREAL_1:29;
(diff (f2,x0)) * (((f1 . (x + t)) - (f1 . x)) / (diff (f2,x0))) = (((f2 . (x + t)) - (f2 . x)) * (diff (f1,x0))) / (diff (f2,x0)) by A8, XCMPLX_1:74;
then ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (((f2 . (x + t)) - (f2 . x)) * ((diff (f1,x0)) / (diff (f2,x0)))) / ((f2 . (x + t)) - (f2 . x)) by A6, A7, XCMPLX_1:87;
then A9: ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (((diff (f1,x0)) / (diff (f2,x0))) / ((f2 . (x + t)) - (f2 . x))) * ((f2 . (x + t)) - (f2 . x)) ;
take s = (x0 - x) / t; ::_thesis: ( 0 < s & s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) )
x0 in { r where r is Real : ( x < r & r < x + t ) } by A7, RCOMP_1:def_2;
then A10: ex g being Real st
( g = x0 & x < g & g < x + t ) ;
then 0 < x0 - x by XREAL_1:50;
then 0 / t < (x0 - x) / t by A1, XREAL_1:74;
hence 0 < s ; ::_thesis: ( s < 1 & ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) )
x0 - x < t by A10, XREAL_1:19;
then (x0 - x) / t < t / t by A1, XREAL_1:74;
hence s < 1 by A1, XCMPLX_1:60; ::_thesis: ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t))))
A11: (s * t) + x = (x0 - x) + x by A1, XCMPLX_1:87;
0 <> (f2 . (x + t)) - (f2 . x) by A1, A3, A5, A6, Th1, XREAL_1:29;
hence ((f1 . (x + t)) - (f1 . x)) / ((f2 . (x + t)) - (f2 . x)) = (diff (f1,(x + (s * t)))) / (diff (f2,(x + (s * t)))) by A9, A11, XCMPLX_1:87; ::_thesis: verum
end;
theorem Th7: :: ROLLE:7
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ) holds
f | ].p,g.[ is V8()
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ) holds
f | ].p,g.[ is V8()
let f be PartFunc of REAL,REAL; ::_thesis: ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ) implies f | ].p,g.[ is V8() )
assume that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x being Real st x in ].p,g.[ holds
diff (f,x) = 0 ; ::_thesis: f | ].p,g.[ is V8()
now__::_thesis:_for_x1,_x2_being_Real_st_x1_in_].p,g.[_/\_(dom_f)_&_x2_in_].p,g.[_/\_(dom_f)_holds_
f_._x1_=_f_._x2
let x1, x2 be Real; ::_thesis: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) implies f . x1 = f . x2 )
assume ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) ) ; ::_thesis: f . x1 = f . x2
then A4: ( x1 in ].p,g.[ & x2 in ].p,g.[ ) by XBOOLE_0:def_4;
now__::_thesis:_f_._x1_=_f_._x2
percases ( x1 = x2 or not x1 = x2 ) ;
suppose x1 = x2 ; ::_thesis: f . x1 = f . x2
hence f . x1 = f . x2 ; ::_thesis: verum
end;
supposeA5: not x1 = x2 ; ::_thesis: f . x1 = f . x2
now__::_thesis:_f_._x1_=_f_._x2
percases ( x1 < x2 or x2 < x1 ) by A5, XXREAL_0:1;
supposeA6: x1 < x2 ; ::_thesis: f . x1 = f . x2
then 0 <> x2 - x1 ;
then A7: 0 <> (x2 - x1) " by XCMPLX_1:202;
reconsider Z = ].x1,x2.[ as open Subset of REAL ;
A8: [.x1,x2.] c= ].p,g.[ by A4, XXREAL_2:def_12;
f | ].p,g.[ is continuous by A2, FDIFF_1:25;
then A9: f | [.x1,x2.] is continuous by A8, FCONT_1:16;
A10: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2, A8, FDIFF_1:26, XBOOLE_1:1;
then A11: ex x0 being Real st
( x0 in ].x1,x2.[ & diff (f,x0) = ((f . x2) - (f . x1)) / (x2 - x1) ) by A1, A6, A8, A9, Th3, XBOOLE_1:1;
Z c= ].p,g.[ by A8, A10, XBOOLE_1:1;
then 0 = (f . x2) - (f . x1) by A3, A7, A11, XCMPLX_1:6;
hence f . x1 = f . x2 ; ::_thesis: verum
end;
supposeA12: x2 < x1 ; ::_thesis: f . x1 = f . x2
then 0 <> x1 - x2 ;
then A13: 0 <> (x1 - x2) " by XCMPLX_1:202;
reconsider Z = ].x2,x1.[ as open Subset of REAL ;
A14: [.x2,x1.] c= ].p,g.[ by A4, XXREAL_2:def_12;
f | ].p,g.[ is continuous by A2, FDIFF_1:25;
then A15: f | [.x2,x1.] is continuous by A14, FCONT_1:16;
A16: Z c= [.x2,x1.] by XXREAL_1:25;
then f is_differentiable_on Z by A2, A14, FDIFF_1:26, XBOOLE_1:1;
then A17: ex x0 being Real st
( x0 in ].x2,x1.[ & diff (f,x0) = ((f . x1) - (f . x2)) / (x1 - x2) ) by A1, A12, A14, A15, Th3, XBOOLE_1:1;
Z c= ].p,g.[ by A14, A16, XBOOLE_1:1;
then 0 = (f . x1) - (f . x2) by A3, A13, A17, XCMPLX_1:6;
hence f . x1 = f . x2 ; ::_thesis: verum
end;
end;
end;
hence f . x1 = f . x2 ; ::_thesis: verum
end;
end;
end;
hence f . x1 = f . x2 ; ::_thesis: verum
end;
hence f | ].p,g.[ is V8() by PARTFUN2:58; ::_thesis: verum
end;
theorem :: ROLLE:8
for p, g being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f1,x) = diff (f2,x) ) holds
( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r )
proof
let p, g be Real; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f1,x) = diff (f2,x) ) holds
( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r )
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f1,x) = diff (f2,x) ) implies ( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r ) )
assume that
A1: ( f1 is_differentiable_on ].p,g.[ & f2 is_differentiable_on ].p,g.[ ) and
A2: for x being Real st x in ].p,g.[ holds
diff (f1,x) = diff (f2,x) ; ::_thesis: ( (f1 - f2) | ].p,g.[ is V8() & ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r )
reconsider Z = ].p,g.[ as open Subset of REAL ;
( ].p,g.[ c= dom f1 & ].p,g.[ c= dom f2 ) by A1, FDIFF_1:def_6;
then ].p,g.[ c= (dom f1) /\ (dom f2) by XBOOLE_1:19;
then A3: ].p,g.[ c= dom (f1 - f2) by VALUED_1:12;
then A4: f1 - f2 is_differentiable_on Z by A1, FDIFF_1:19;
now__::_thesis:_for_x_being_Real_st_x_in_].p,g.[_holds_
diff_((f1_-_f2),x)_=_0
let x be Real; ::_thesis: ( x in ].p,g.[ implies diff ((f1 - f2),x) = 0 )
assume A5: x in ].p,g.[ ; ::_thesis: diff ((f1 - f2),x) = 0
hence diff ((f1 - f2),x) = ((f1 - f2) `| Z) . x by A4, FDIFF_1:def_7
.= (diff (f1,x)) - (diff (f2,x)) by A1, A3, A5, FDIFF_1:19
.= (diff (f1,x)) - (diff (f1,x)) by A2, A5
.= 0 ;
::_thesis: verum
end;
hence (f1 - f2) | ].p,g.[ is V8() by A1, A3, Th7, FDIFF_1:19; ::_thesis: ex r being Real st
for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r
then consider r being Real such that
A6: for x being Real st x in ].p,g.[ /\ (dom (f1 - f2)) holds
(f1 - f2) . x = r by PARTFUN2:57;
take r ; ::_thesis: for x being Real st x in ].p,g.[ holds
f1 . x = (f2 . x) + r
let x be Real; ::_thesis: ( x in ].p,g.[ implies f1 . x = (f2 . x) + r )
assume A7: x in ].p,g.[ ; ::_thesis: f1 . x = (f2 . x) + r
then x in ].p,g.[ /\ (dom (f1 - f2)) by A3, XBOOLE_1:28;
then r = (f1 - f2) . x by A6
.= (f1 . x) - (f2 . x) by A3, A7, VALUED_1:13 ;
hence f1 . x = (f2 . x) + r ; ::_thesis: verum
end;
theorem :: ROLLE:9
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 < diff (f,x) ) holds
f | ].p,g.[ is increasing
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 < diff (f,x) ) holds
f | ].p,g.[ is increasing
let f be PartFunc of REAL,REAL; ::_thesis: ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 < diff (f,x) ) implies f | ].p,g.[ is increasing )
assume that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x being Real st x in ].p,g.[ holds
0 < diff (f,x) ; ::_thesis: f | ].p,g.[ is increasing
now__::_thesis:_for_x1,_x2_being_Real_st_x1_in_].p,g.[_/\_(dom_f)_&_x2_in_].p,g.[_/\_(dom_f)_&_x1_<_x2_holds_
f_._x1_<_f_._x2
let x1, x2 be Real; ::_thesis: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 implies f . x1 < f . x2 )
assume that
A4: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) ) and
A5: x1 < x2 ; ::_thesis: f . x1 < f . x2
A6: 0 < x2 - x1 by A5, XREAL_1:50;
reconsider Z = ].x1,x2.[ as open Subset of REAL ;
( x1 in ].p,g.[ & x2 in ].p,g.[ ) by A4, XBOOLE_0:def_4;
then A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def_12;
f | ].p,g.[ is continuous by A2, FDIFF_1:25;
then A8: f | [.x1,x2.] is continuous by A7, FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2, A7, FDIFF_1:26, XBOOLE_1:1;
then A10: ex x0 being Real st
( x0 in ].x1,x2.[ & diff (f,x0) = ((f . x2) - (f . x1)) / (x2 - x1) ) by A1, A5, A7, A8, Th3, XBOOLE_1:1;
Z c= ].p,g.[ by A7, A9, XBOOLE_1:1;
then 0 < (f . x2) - (f . x1) by A3, A6, A10;
then (f . x1) + 0 < f . x2 by XREAL_1:20;
hence f . x1 < f . x2 ; ::_thesis: verum
end;
hence f | ].p,g.[ is increasing by RFUNCT_2:20; ::_thesis: verum
end;
theorem :: ROLLE:10
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) < 0 ) holds
f | ].p,g.[ is decreasing
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) < 0 ) holds
f | ].p,g.[ is decreasing
let f be PartFunc of REAL,REAL; ::_thesis: ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) < 0 ) implies f | ].p,g.[ is decreasing )
assume that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x being Real st x in ].p,g.[ holds
diff (f,x) < 0 ; ::_thesis: f | ].p,g.[ is decreasing
now__::_thesis:_for_x1,_x2_being_Real_st_x1_in_].p,g.[_/\_(dom_f)_&_x2_in_].p,g.[_/\_(dom_f)_&_x1_<_x2_holds_
f_._x2_<_f_._x1
let x1, x2 be Real; ::_thesis: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 implies f . x2 < f . x1 )
assume that
A4: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) ) and
A5: x1 < x2 ; ::_thesis: f . x2 < f . x1
A6: 0 < x2 - x1 by A5, XREAL_1:50;
reconsider Z = ].x1,x2.[ as open Subset of REAL ;
( x1 in ].p,g.[ & x2 in ].p,g.[ ) by A4, XBOOLE_0:def_4;
then A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def_12;
f | ].p,g.[ is continuous by A2, FDIFF_1:25;
then A8: f | [.x1,x2.] is continuous by A7, FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2, A7, FDIFF_1:26, XBOOLE_1:1;
then A10: ex x0 being Real st
( x0 in ].x1,x2.[ & diff (f,x0) = ((f . x2) - (f . x1)) / (x2 - x1) ) by A1, A5, A7, A8, Th3, XBOOLE_1:1;
Z c= ].p,g.[ by A7, A9, XBOOLE_1:1;
then (f . x2) - (f . x1) < 0 by A3, A6, A10;
then f . x2 < (f . x1) + 0 by XREAL_1:19;
hence f . x2 < f . x1 ; ::_thesis: verum
end;
hence f | ].p,g.[ is decreasing by RFUNCT_2:21; ::_thesis: verum
end;
theorem :: ROLLE:11
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 <= diff (f,x) ) holds
f | ].p,g.[ is non-decreasing
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 <= diff (f,x) ) holds
f | ].p,g.[ is non-decreasing
let f be PartFunc of REAL,REAL; ::_thesis: ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
0 <= diff (f,x) ) implies f | ].p,g.[ is non-decreasing )
assume that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x being Real st x in ].p,g.[ holds
0 <= diff (f,x) ; ::_thesis: f | ].p,g.[ is non-decreasing
now__::_thesis:_for_x1,_x2_being_Real_st_x1_in_].p,g.[_/\_(dom_f)_&_x2_in_].p,g.[_/\_(dom_f)_&_x1_<_x2_holds_
f_._x1_<=_f_._x2
let x1, x2 be Real; ::_thesis: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 implies f . x1 <= f . x2 )
assume that
A4: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) ) and
A5: x1 < x2 ; ::_thesis: f . x1 <= f . x2
A6: 0 <> x2 - x1 by A5;
reconsider Z = ].x1,x2.[ as open Subset of REAL ;
( x1 in ].p,g.[ & x2 in ].p,g.[ ) by A4, XBOOLE_0:def_4;
then A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def_12;
f | ].p,g.[ is continuous by A2, FDIFF_1:25;
then A8: f | [.x1,x2.] is continuous by A7, FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then A10: Z c= ].p,g.[ by A7, XBOOLE_1:1;
f is_differentiable_on Z by A2, A7, A9, FDIFF_1:26, XBOOLE_1:1;
then ex x0 being Real st
( x0 in ].x1,x2.[ & diff (f,x0) = ((f . x2) - (f . x1)) / (x2 - x1) ) by A1, A5, A7, A8, Th3, XBOOLE_1:1;
then A11: 0 <= ((f . x2) - (f . x1)) / (x2 - x1) by A3, A10;
0 <= x2 - x1 by A5, XREAL_1:50;
then 0 * (x2 - x1) <= (((f . x2) - (f . x1)) / (x2 - x1)) * (x2 - x1) by A11;
then 0 <= (f . x2) - (f . x1) by A6, XCMPLX_1:87;
then (f . x1) + 0 <= f . x2 by XREAL_1:19;
hence f . x1 <= f . x2 ; ::_thesis: verum
end;
hence f | ].p,g.[ is non-decreasing by RFUNCT_2:22; ::_thesis: verum
end;
theorem :: ROLLE:12
for p, g being Real
for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ) holds
f | ].p,g.[ is non-increasing
proof
let p, g be Real; ::_thesis: for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ) holds
f | ].p,g.[ is non-increasing
let f be PartFunc of REAL,REAL; ::_thesis: ( ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ) implies f | ].p,g.[ is non-increasing )
assume that
A1: ].p,g.[ c= dom f and
A2: f is_differentiable_on ].p,g.[ and
A3: for x being Real st x in ].p,g.[ holds
diff (f,x) <= 0 ; ::_thesis: f | ].p,g.[ is non-increasing
now__::_thesis:_for_x1,_x2_being_Real_st_x1_in_].p,g.[_/\_(dom_f)_&_x2_in_].p,g.[_/\_(dom_f)_&_x1_<_x2_holds_
f_._x2_<=_f_._x1
let x1, x2 be Real; ::_thesis: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) & x1 < x2 implies f . x2 <= f . x1 )
assume that
A4: ( x1 in ].p,g.[ /\ (dom f) & x2 in ].p,g.[ /\ (dom f) ) and
A5: x1 < x2 ; ::_thesis: f . x2 <= f . x1
A6: 0 <= x2 - x1 by A5, XREAL_1:50;
reconsider Z = ].x1,x2.[ as open Subset of REAL ;
( x1 in ].p,g.[ & x2 in ].p,g.[ ) by A4, XBOOLE_0:def_4;
then A7: [.x1,x2.] c= ].p,g.[ by XXREAL_2:def_12;
f | ].p,g.[ is continuous by A2, FDIFF_1:25;
then A8: f | [.x1,x2.] is continuous by A7, FCONT_1:16;
A9: Z c= [.x1,x2.] by XXREAL_1:25;
then f is_differentiable_on Z by A2, A7, FDIFF_1:26, XBOOLE_1:1;
then A10: ex x0 being Real st
( x0 in ].x1,x2.[ & diff (f,x0) = ((f . x2) - (f . x1)) / (x2 - x1) ) by A1, A5, A7, A8, Th3, XBOOLE_1:1;
A11: 0 <> x2 - x1 by A5;
Z c= ].p,g.[ by A7, A9, XBOOLE_1:1;
then (((f . x2) - (f . x1)) / (x2 - x1)) * (x2 - x1) <= 0 * (x2 - x1) by A3, A6, A10, XREAL_1:64;
then (f . x2) - (f . x1) <= 0 by A11, XCMPLX_1:87;
then f . x2 <= (f . x1) + 0 by XREAL_1:20;
hence f . x2 <= f . x1 ; ::_thesis: verum
end;
hence f | ].p,g.[ is non-increasing by RFUNCT_2:23; ::_thesis: verum
end;