:: 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;