let g, p be Real; :: thesis: for f being PartFunc of REAL,REAL st f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing holds

f | [.p,g.] is decreasing

let f be PartFunc of REAL,REAL; :: thesis: ( f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing implies f | [.p,g.] is decreasing )

A0: p is set by TARSKI:1;

assume that

A1: f is one-to-one and

A2: [.p,g.] c= dom f and

A3: p <= g and

A4: f | [.p,g.] is continuous and

A5: not f | [.p,g.] is increasing and

A6: not f | [.p,g.] is decreasing ; :: thesis: contradiction

f | [.p,g.] is decreasing

let f be PartFunc of REAL,REAL; :: thesis: ( f is one-to-one & [.p,g.] c= dom f & p <= g & f | [.p,g.] is continuous & not f | [.p,g.] is increasing implies f | [.p,g.] is decreasing )

A0: p is set by TARSKI:1;

assume that

A1: f is one-to-one and

A2: [.p,g.] c= dom f and

A3: p <= g and

A4: f | [.p,g.] is continuous and

A5: not f | [.p,g.] is increasing and

A6: not f | [.p,g.] is decreasing ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( p = g or p <> g )
;

end;

suppose A7:
p <> g
; :: thesis: contradiction

A8:
g in [.p,g.]
by A3, XXREAL_1:1;

A9: p in [.p,g.] by A3, XXREAL_1:1;

then A10: f . p <> f . g by A1, A2, A7, A8, FUNCT_1:def 4;

end;A9: p in [.p,g.] by A3, XXREAL_1:1;

then A10: f . p <> f . g by A1, A2, A7, A8, FUNCT_1:def 4;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( f . p < f . g or f . p > f . g )
by A10, XXREAL_0:1;

end;

suppose A11:
f . p < f . g
; :: thesis: contradiction

A12:
for x1 being Real st p <= x1 & x1 <= g holds

( f . p <= f . x1 & f . x1 <= f . g )

A31: x1 in [.p,g.] /\ (dom f) and

A32: x2 in [.p,g.] /\ (dom f) and

A33: x1 < x2 and

A34: f . x2 <= f . x1 by A5, RFUNCT_2:20;

A35: x1 in [.p,g.] by A31, XBOOLE_0:def 4;

then A36: [.p,x1.] c= [.p,g.] by A9, XXREAL_2:def 12;

A37: x2 in [.p,g.] by A32, XBOOLE_0:def 4;

then x2 in { r where r is Real : ( p <= r & r <= g ) } by RCOMP_1:def 1;

then ex r being Real st

( r = x2 & p <= r & r <= g ) ;

then f . p <= f . x2 by A12;

then f . x2 in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A34;

then f . x2 in [.(f . p),(f . x1).] by RCOMP_1:def 1;

then A38: f . x2 in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;

x1 in { t where t is Real : ( p <= t & t <= g ) } by A35, RCOMP_1:def 1;

then A39: ex r being Real st

( r = x1 & p <= r & r <= g ) ;

p in [.p,g.] by A3, XXREAL_1:1;

then A40: [.p,x1.] c= [.p,g.] by A35, XXREAL_2:def 12;

then f | [.p,x1.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A41: s in [.p,x1.] and

A42: f . s = f . x2 by A2, A39, A38, A36, Th15, XBOOLE_1:1;

s in { t where t is Real : ( p <= t & t <= x1 ) } by A41, RCOMP_1:def 1;

then A43: ex r being Real st

( r = s & p <= r & r <= x1 ) ;

s in [.p,g.] by A40, A41;

hence contradiction by A1, A2, A33, A37, A42, A43, FUNCT_1:def 4; :: thesis: verum

end;( f . p <= f . x1 & f . x1 <= f . g )

proof

consider x1, x2 being Real such that
let x1 be Real; :: thesis: ( p <= x1 & x1 <= g implies ( f . p <= f . x1 & f . x1 <= f . g ) )

assume that

A13: p <= x1 and

A14: x1 <= g and

A15: ( not f . p <= f . x1 or not f . x1 <= f . g ) ; :: thesis: contradiction

end;assume that

A13: p <= x1 and

A14: x1 <= g and

A15: ( not f . p <= f . x1 or not f . x1 <= f . g ) ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( f . x1 < f . p or f . g < f . x1 )
by A15;

end;

suppose A16:
f . x1 < f . p
; :: thesis: contradiction

then
f . p in { r where r is Real : ( f . x1 <= r & r <= f . g ) }
by A11;

then f . p in [.(f . x1),(f . g).] by RCOMP_1:def 1;

then A17: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def 3;

x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14;

then A18: x1 in [.p,g.] by RCOMP_1:def 1;

g in [.p,g.] by A3, XXREAL_1:1;

then A19: [.x1,g.] c= [.p,g.] by A18, XXREAL_2:def 12;

then f | [.x1,g.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A20: s in [.x1,g.] and

A21: f . s = f . p by A2, A14, A19, A17, Th15, XBOOLE_1:1;

s in { t where t is Real : ( x1 <= t & t <= g ) } by A20, RCOMP_1:def 1;

then A22: ex r being Real st

( r = s & x1 <= r & r <= g ) ;

A23: x1 > p by A13, A16, XXREAL_0:1;

s in [.p,g.] by A19, A20;

hence contradiction by A1, A2, A9, A23, A21, A22, FUNCT_1:def 4; :: thesis: verum

end;then f . p in [.(f . x1),(f . g).] by RCOMP_1:def 1;

then A17: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def 3;

x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14;

then A18: x1 in [.p,g.] by RCOMP_1:def 1;

g in [.p,g.] by A3, XXREAL_1:1;

then A19: [.x1,g.] c= [.p,g.] by A18, XXREAL_2:def 12;

then f | [.x1,g.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A20: s in [.x1,g.] and

A21: f . s = f . p by A2, A14, A19, A17, Th15, XBOOLE_1:1;

s in { t where t is Real : ( x1 <= t & t <= g ) } by A20, RCOMP_1:def 1;

then A22: ex r being Real st

( r = s & x1 <= r & r <= g ) ;

A23: x1 > p by A13, A16, XXREAL_0:1;

s in [.p,g.] by A19, A20;

hence contradiction by A1, A2, A9, A23, A21, A22, FUNCT_1:def 4; :: thesis: verum

suppose A24:
f . g < f . x1
; :: thesis: contradiction

then
f . g in { r where r is Real : ( f . p <= r & r <= f . x1 ) }
by A11;

then f . g in [.(f . p),(f . x1).] by RCOMP_1:def 1;

then A25: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;

x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14;

then A26: x1 in [.p,g.] by RCOMP_1:def 1;

p in [.p,g.] by A3, XXREAL_1:1;

then A27: [.p,x1.] c= [.p,g.] by A26, XXREAL_2:def 12;

then f | [.p,x1.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A28: s in [.p,x1.] and

A29: f . s = f . g by A2, A13, A27, A25, Th15, XBOOLE_1:1;

s in { t where t is Real : ( p <= t & t <= x1 ) } by A28, RCOMP_1:def 1;

then A30: ex r being Real st

( r = s & p <= r & r <= x1 ) ;

s in [.p,g.] by A27, A28;

then s = g by A1, A2, A8, A29, FUNCT_1:def 4;

hence contradiction by A14, A24, A30, XXREAL_0:1; :: thesis: verum

end;then f . g in [.(f . p),(f . x1).] by RCOMP_1:def 1;

then A25: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;

x1 in { r where r is Real : ( p <= r & r <= g ) } by A13, A14;

then A26: x1 in [.p,g.] by RCOMP_1:def 1;

p in [.p,g.] by A3, XXREAL_1:1;

then A27: [.p,x1.] c= [.p,g.] by A26, XXREAL_2:def 12;

then f | [.p,x1.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A28: s in [.p,x1.] and

A29: f . s = f . g by A2, A13, A27, A25, Th15, XBOOLE_1:1;

s in { t where t is Real : ( p <= t & t <= x1 ) } by A28, RCOMP_1:def 1;

then A30: ex r being Real st

( r = s & p <= r & r <= x1 ) ;

s in [.p,g.] by A27, A28;

then s = g by A1, A2, A8, A29, FUNCT_1:def 4;

hence contradiction by A14, A24, A30, XXREAL_0:1; :: thesis: verum

A31: x1 in [.p,g.] /\ (dom f) and

A32: x2 in [.p,g.] /\ (dom f) and

A33: x1 < x2 and

A34: f . x2 <= f . x1 by A5, RFUNCT_2:20;

A35: x1 in [.p,g.] by A31, XBOOLE_0:def 4;

then A36: [.p,x1.] c= [.p,g.] by A9, XXREAL_2:def 12;

A37: x2 in [.p,g.] by A32, XBOOLE_0:def 4;

then x2 in { r where r is Real : ( p <= r & r <= g ) } by RCOMP_1:def 1;

then ex r being Real st

( r = x2 & p <= r & r <= g ) ;

then f . p <= f . x2 by A12;

then f . x2 in { r where r is Real : ( f . p <= r & r <= f . x1 ) } by A34;

then f . x2 in [.(f . p),(f . x1).] by RCOMP_1:def 1;

then A38: f . x2 in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;

x1 in { t where t is Real : ( p <= t & t <= g ) } by A35, RCOMP_1:def 1;

then A39: ex r being Real st

( r = x1 & p <= r & r <= g ) ;

p in [.p,g.] by A3, XXREAL_1:1;

then A40: [.p,x1.] c= [.p,g.] by A35, XXREAL_2:def 12;

then f | [.p,x1.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A41: s in [.p,x1.] and

A42: f . s = f . x2 by A2, A39, A38, A36, Th15, XBOOLE_1:1;

s in { t where t is Real : ( p <= t & t <= x1 ) } by A41, RCOMP_1:def 1;

then A43: ex r being Real st

( r = s & p <= r & r <= x1 ) ;

s in [.p,g.] by A40, A41;

hence contradiction by A1, A2, A33, A37, A42, A43, FUNCT_1:def 4; :: thesis: verum

suppose A44:
f . p > f . g
; :: thesis: contradiction

A45:
for x1 being Real st p <= x1 & x1 <= g holds

( f . g <= f . x1 & f . x1 <= f . p )

A65: x1 in [.p,g.] /\ (dom f) and

A66: x2 in [.p,g.] /\ (dom f) and

A67: x1 < x2 and

A68: f . x1 <= f . x2 by A6, RFUNCT_2:21;

A69: x2 in [.p,g.] by A66, XBOOLE_0:def 4;

then A70: [.x2,g.] c= [.p,g.] by A8, XXREAL_2:def 12;

A71: x1 in [.p,g.] by A65, XBOOLE_0:def 4;

then x1 in { t where t is Real : ( p <= t & t <= g ) } by RCOMP_1:def 1;

then ex r being Real st

( r = x1 & p <= r & r <= g ) ;

then f . g <= f . x1 by A45;

then f . x1 in { r where r is Real : ( f . g <= r & r <= f . x2 ) } by A68;

then f . x1 in [.(f . g),(f . x2).] by RCOMP_1:def 1;

then A72: f . x1 in [.(f . x2),(f . g).] \/ [.(f . g),(f . x2).] by XBOOLE_0:def 3;

x2 in { r where r is Real : ( p <= r & r <= g ) } by A69, RCOMP_1:def 1;

then A73: ex r being Real st

( r = x2 & p <= r & r <= g ) ;

g in [.p,g.] by A3, XXREAL_1:1;

then A74: [.x2,g.] c= [.p,g.] by A69, XXREAL_2:def 12;

then f | [.x2,g.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A75: s in [.x2,g.] and

A76: f . s = f . x1 by A2, A73, A72, A70, Th15, XBOOLE_1:1;

s in { t where t is Real : ( x2 <= t & t <= g ) } by A75, RCOMP_1:def 1;

then A77: ex r being Real st

( r = s & x2 <= r & r <= g ) ;

s in [.p,g.] by A74, A75;

hence contradiction by A1, A2, A67, A71, A76, A77, FUNCT_1:def 4; :: thesis: verum

end;( f . g <= f . x1 & f . x1 <= f . p )

proof

consider x1, x2 being Real such that
let x1 be Real; :: thesis: ( p <= x1 & x1 <= g implies ( f . g <= f . x1 & f . x1 <= f . p ) )

assume that

A46: p <= x1 and

A47: x1 <= g and

A48: ( not f . g <= f . x1 or not f . x1 <= f . p ) ; :: thesis: contradiction

end;assume that

A46: p <= x1 and

A47: x1 <= g and

A48: ( not f . g <= f . x1 or not f . x1 <= f . p ) ; :: thesis: contradiction

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( f . x1 < f . g or f . p < f . x1 )
by A48;

end;

suppose A49:
f . x1 < f . g
; :: thesis: contradiction

end;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( g = x1 or g <> x1 )
;

end;

suppose A50:
g <> x1
; :: thesis: contradiction

x1 in { r where r is Real : ( p <= r & r <= g ) }
by A46, A47;

then A51: x1 in [.p,g.] by RCOMP_1:def 1;

f . g in { r where r is Real : ( f . x1 <= r & r <= f . p ) } by A44, A49;

then f . g in [.(f . x1),(f . p).] by RCOMP_1:def 1;

then A52: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;

p in [.p,g.] by A3, XXREAL_1:1;

then A53: [.p,x1.] c= [.p,g.] by A51, XXREAL_2:def 12;

then f | [.p,x1.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A54: s in [.p,x1.] and

A55: f . s = f . g by A2, A46, A53, A52, Th15, XBOOLE_1:1;

s in { t where t is Real : ( p <= t & t <= x1 ) } by A54, RCOMP_1:def 1;

then A56: ex r being Real st

( r = s & p <= r & r <= x1 ) ;

s in [.p,g.] by A53, A54;

then s = g by A1, A2, A8, A55, FUNCT_1:def 4;

hence contradiction by A47, A50, A56, XXREAL_0:1; :: thesis: verum

end;then A51: x1 in [.p,g.] by RCOMP_1:def 1;

f . g in { r where r is Real : ( f . x1 <= r & r <= f . p ) } by A44, A49;

then f . g in [.(f . x1),(f . p).] by RCOMP_1:def 1;

then A52: f . g in [.(f . p),(f . x1).] \/ [.(f . x1),(f . p).] by XBOOLE_0:def 3;

p in [.p,g.] by A3, XXREAL_1:1;

then A53: [.p,x1.] c= [.p,g.] by A51, XXREAL_2:def 12;

then f | [.p,x1.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A54: s in [.p,x1.] and

A55: f . s = f . g by A2, A46, A53, A52, Th15, XBOOLE_1:1;

s in { t where t is Real : ( p <= t & t <= x1 ) } by A54, RCOMP_1:def 1;

then A56: ex r being Real st

( r = s & p <= r & r <= x1 ) ;

s in [.p,g.] by A53, A54;

then s = g by A1, A2, A8, A55, FUNCT_1:def 4;

hence contradiction by A47, A50, A56, XXREAL_0:1; :: thesis: verum

suppose A57:
f . p < f . x1
; :: thesis: contradiction

end;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( p = x1 or p <> x1 )
;

end;

suppose A58:
p <> x1
; :: thesis: contradiction

x1 in { r where r is Real : ( p <= r & r <= g ) }
by A46, A47;

then A59: x1 in [.p,g.] by RCOMP_1:def 1;

f . p in { r where r is Real : ( f . g <= r & r <= f . x1 ) } by A44, A57;

then f . p in [.(f . g),(f . x1).] by RCOMP_1:def 1;

then A60: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def 3;

g in [.p,g.] by A3, XXREAL_1:1;

then A61: [.x1,g.] c= [.p,g.] by A59, XXREAL_2:def 12;

then f | [.x1,g.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A62: s in [.x1,g.] and

A63: f . s = f . p by A2, A47, A61, A60, Th15, XBOOLE_1:1;

s in { t where t is Real : ( x1 <= t & t <= g ) } by A62, RCOMP_1:def 1;

then A64: ex r being Real st

( r = s & x1 <= r & r <= g ) ;

s in [.p,g.] by A61, A62;

then s = p by A1, A2, A9, A63, FUNCT_1:def 4;

hence contradiction by A46, A58, A64, XXREAL_0:1; :: thesis: verum

end;then A59: x1 in [.p,g.] by RCOMP_1:def 1;

f . p in { r where r is Real : ( f . g <= r & r <= f . x1 ) } by A44, A57;

then f . p in [.(f . g),(f . x1).] by RCOMP_1:def 1;

then A60: f . p in [.(f . x1),(f . g).] \/ [.(f . g),(f . x1).] by XBOOLE_0:def 3;

g in [.p,g.] by A3, XXREAL_1:1;

then A61: [.x1,g.] c= [.p,g.] by A59, XXREAL_2:def 12;

then f | [.x1,g.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A62: s in [.x1,g.] and

A63: f . s = f . p by A2, A47, A61, A60, Th15, XBOOLE_1:1;

s in { t where t is Real : ( x1 <= t & t <= g ) } by A62, RCOMP_1:def 1;

then A64: ex r being Real st

( r = s & x1 <= r & r <= g ) ;

s in [.p,g.] by A61, A62;

then s = p by A1, A2, A9, A63, FUNCT_1:def 4;

hence contradiction by A46, A58, A64, XXREAL_0:1; :: thesis: verum

A65: x1 in [.p,g.] /\ (dom f) and

A66: x2 in [.p,g.] /\ (dom f) and

A67: x1 < x2 and

A68: f . x1 <= f . x2 by A6, RFUNCT_2:21;

A69: x2 in [.p,g.] by A66, XBOOLE_0:def 4;

then A70: [.x2,g.] c= [.p,g.] by A8, XXREAL_2:def 12;

A71: x1 in [.p,g.] by A65, XBOOLE_0:def 4;

then x1 in { t where t is Real : ( p <= t & t <= g ) } by RCOMP_1:def 1;

then ex r being Real st

( r = x1 & p <= r & r <= g ) ;

then f . g <= f . x1 by A45;

then f . x1 in { r where r is Real : ( f . g <= r & r <= f . x2 ) } by A68;

then f . x1 in [.(f . g),(f . x2).] by RCOMP_1:def 1;

then A72: f . x1 in [.(f . x2),(f . g).] \/ [.(f . g),(f . x2).] by XBOOLE_0:def 3;

x2 in { r where r is Real : ( p <= r & r <= g ) } by A69, RCOMP_1:def 1;

then A73: ex r being Real st

( r = x2 & p <= r & r <= g ) ;

g in [.p,g.] by A3, XXREAL_1:1;

then A74: [.x2,g.] c= [.p,g.] by A69, XXREAL_2:def 12;

then f | [.x2,g.] is continuous by A4, FCONT_1:16;

then consider s being Real such that

A75: s in [.x2,g.] and

A76: f . s = f . x1 by A2, A73, A72, A70, Th15, XBOOLE_1:1;

s in { t where t is Real : ( x2 <= t & t <= g ) } by A75, RCOMP_1:def 1;

then A77: ex r being Real st

( r = s & x2 <= r & r <= g ) ;

s in [.p,g.] by A74, A75;

hence contradiction by A1, A2, A67, A71, A76, A77, FUNCT_1:def 4; :: thesis: verum