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
now :: thesis: contradiction
per cases ( p = g or p <> g ) ;
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;
now :: thesis: contradiction
per cases ( f . p < f . g or f . p > f . g ) by A10, XXREAL_0:1;
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 )
proof
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
now :: thesis: contradiction
per cases ( f . x1 < f . p or f . g < f . x1 ) by A15;
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;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider x1, x2 being Real such that
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;
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 )
proof
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
now :: thesis: contradiction
per cases ( f . x1 < f . g or f . p < f . x1 ) by A48;
suppose A49: f . x1 < f . g ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( g = x1 or g <> x1 ) ;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A57: f . p < f . x1 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( p = x1 or p <> x1 ) ;
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider x1, x2 being Real such that
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;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum