let g, p be Real; 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; ( 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
; contradiction
now contradictionper cases
( p = g or p <> g )
;
suppose A7:
p <> g
;
contradictionA8:
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 contradictionper cases
( f . p < f . g or f . p > f . g )
by A10, XXREAL_0:1;
suppose A11:
f . p < f . g
;
contradictionA12:
for
x1 being
Real st
p <= x1 &
x1 <= g holds
(
f . p <= f . x1 &
f . x1 <= f . g )
proof
let x1 be
Real;
( 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 )
;
contradiction
now contradictionper cases
( f . x1 < f . p or f . g < f . x1 )
by A15;
suppose A16:
f . x1 < f . p
;
contradictionthen
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;
verum end; suppose A24:
f . g < f . x1
;
contradictionthen
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;
verum end; end; end;
hence
contradiction
;
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;
verum end; suppose A44:
f . p > f . g
;
contradictionA45:
for
x1 being
Real st
p <= x1 &
x1 <= g holds
(
f . g <= f . x1 &
f . x1 <= f . p )
proof
let x1 be
Real;
( 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 )
;
contradiction
now contradictionper cases
( f . x1 < f . g or f . p < f . x1 )
by A48;
suppose A49:
f . x1 < f . g
;
contradictionnow contradictionper cases
( g = x1 or g <> x1 )
;
suppose
g = x1
;
contradictionhence
contradiction
by A49;
verum end; suppose A50:
g <> x1
;
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;
verum end; end; end; hence
contradiction
;
verum end; suppose A57:
f . p < f . x1
;
contradictionnow contradictionper cases
( p = x1 or p <> x1 )
;
suppose
p = x1
;
contradictionhence
contradiction
by A57;
verum end; suppose A58:
p <> x1
;
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;
verum end; end; end; hence
contradiction
;
verum end; end; end;
hence
contradiction
;
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;
verum end; end; end; hence
contradiction
;
verum end; end; end;
hence
contradiction
; verum