Copyright (c) 2000 Association of Mizar Users
environ
vocabulary SUPINF_1, RLVECT_1, ARYTM, MEASURE6, GROUP_1, ARYTM_1, ARYTM_3,
COMPLEX1, ABSVALUE, SQUARE_1;
notation ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, ABSVALUE, SQUARE_1, SUPINF_1,
SUPINF_2, MEASURE6, EXTREAL1, MESFUNC1;
constructors SQUARE_1, MESFUNC1, SUPINF_2, MEASURE6, EXTREAL1, REAL_1,
MEMBERED, ABSVALUE;
clusters XREAL_0, MEMBERED;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
theorems SUPINF_1, MEASURE6, REAL_1, REAL_2, SUPINF_2, AXIOMS, XREAL_0,
SQUARE_1, EXTREAL1, MESFUNC1, ABSVALUE, HAHNBAN, XCMPLX_0, XCMPLX_1;
begin :: Preliminaries
reserve x,y,w,z for R_eal;
reserve a,b for Real;
canceled;
theorem :: extension of AXIOMS:19
x <> +infty & x <> -infty implies ex y st x + y = 0.
proof
assume x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
reconsider b = -a as Real;
A1:a + b = 0 by XCMPLX_0:def 6;
A2: R_EAL b = b by MEASURE6:def 1;
take R_EAL b;
thus thesis by A1,A2,SUPINF_2:1,def 1;
end;
theorem :: extension of AXIOMS:20
x <> +infty & x <> -infty & x <> 0. implies ex y st x*y = 1.
proof
assume A1:x <> +infty & x <> -infty & x <> 0.;
then reconsider a = x as Real by EXTREAL1:1;
consider b being real number such that
A2:a * b = 1 by A1,AXIOMS:20,SUPINF_2:def 1;
reconsider b as Real by XREAL_0:def 1;
A3: R_EAL b = b by MEASURE6:def 1;
take R_EAL b;
thus thesis by A2,A3,EXTREAL1:13,MESFUNC1:def 8;
end;
theorem Th4:
1. * x = x & x * 1. = x & R_EAL 1 * x = x & x * R_EAL 1 = x
proof
A1:R_EAL 1 = 1. by MEASURE6:def 1,MESFUNC1:def 8;
A2:0. <' 1. by EXTREAL1:18,MESFUNC1:def 8;
per cases by EXTREAL1:1;
suppose x is Real;
then reconsider a = x as Real;
1. * x = 1 * a by EXTREAL1:13,MESFUNC1:def 8;
hence thesis by MEASURE6:def 1,MESFUNC1:def 8;
suppose x = +infty;
hence thesis by A1,A2,EXTREAL1:def 1;
suppose x = -infty;
hence thesis by A1,A2,EXTREAL1:def 1;
end;
theorem :: extension of REAL_1:25
0. - x = -x
proof
per cases;
suppose A1:x = +infty;
then 0. - x = -infty by SUPINF_2:6,19;
hence thesis by A1,SUPINF_2:def 3;
suppose x = -infty;
hence thesis by SUPINF_2:4,7,19;
suppose x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
0. - x = 0 - a by SUPINF_2:5,def 1 .= -a by XCMPLX_1:150;
hence thesis by SUPINF_2:3;
end;
canceled;
theorem Th7:
0. <=' x & 0. <=' y implies 0. <=' x + y
proof
assume A1:(0. <=' x & 0. <=' y);
per cases;
suppose x = +infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose x <> +infty;
then reconsider a = x as Real by A1,EXTREAL1:1,SUPINF_2:19;
now per cases;
suppose y = +infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose y <> +infty;
then reconsider b = y as Real by A1,EXTREAL1:1,SUPINF_2:19;
A2: x + y = a + b by SUPINF_2:1;
0 <= a & 0 <= b by A1,EXTREAL1:19;
then 0 + 0 <= a + b by REAL_1:55;
hence thesis by A2,EXTREAL1:19;
end;
hence thesis;
end;
theorem
(0. <=' x & 0. <' y) or (0. <' x & 0. <=' y) implies 0. <' x + y
proof
assume A1:(0. <=' x & 0. <' y) or (0. <' x & 0. <=' y);
per cases;
suppose x = +infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose x <> +infty;
then reconsider a = x as Real by A1,EXTREAL1:1,SUPINF_2:19;
now per cases;
suppose y = +infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose y <> +infty;
then reconsider b = y as Real by A1,EXTREAL1:1,SUPINF_2:19;
A2: x + y = a + b by SUPINF_2:1;
(0 <= a & 0 < b) or (0 < a & 0 <= b)
proof
now per cases by A1;
suppose 0. <=' x & 0. <' y;
hence thesis by EXTREAL1:18,19;
suppose 0. <' x & 0. <=' y;
hence thesis by EXTREAL1:18,19;
end;
hence thesis;
end;
then 0 + 0 < a + b by REAL_1:67;
hence thesis by A2,EXTREAL1:18;
end;
hence thesis;
end;
theorem Th9:
x <=' 0. & y <=' 0. implies x + y <=' 0.
proof
assume A1:x <=' 0. & y <=' 0.;
per cases;
suppose x = -infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose x <> -infty;
then reconsider a = x as Real by A1,EXTREAL1:1,SUPINF_2:19;
now per cases;
suppose y = -infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose y <> -infty;
then reconsider b = y as Real by A1,EXTREAL1:1,SUPINF_2:19;
A2: x + y = a + b by SUPINF_2:1;
a <= 0 & b <= 0 by A1,EXTREAL1:18;
then a + b <= 0 + 0 by REAL_1:55;
hence thesis by A2,EXTREAL1:18;
end;
hence thesis;
end;
theorem
(x <=' 0. & y <' 0.) or (x <' 0. & y <=' 0.) implies x + y <' 0.
proof
assume A1:(x <=' 0. & y <' 0.) or (x <' 0. & y <=' 0.);
per cases;
suppose x = -infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose x <> -infty;
then reconsider a = x as Real by A1,EXTREAL1:1,SUPINF_2:19;
now per cases;
suppose y = -infty;
hence thesis by A1,SUPINF_2:19,def 2;
suppose y <> -infty;
then reconsider b = y as Real by A1,EXTREAL1:1,SUPINF_2:19;
A2: x + y = a + b by SUPINF_2:1;
(a <= 0 & b < 0) or (a < 0 & b <= 0)
proof
now per cases by A1;
suppose x <=' 0. & y <' 0.;
hence thesis by EXTREAL1:18,19;
suppose x <' 0. & y <=' 0.;
hence thesis by EXTREAL1:18,19;
end;
hence thesis;
end;
then a + b < 0 + 0 by REAL_1:67;
hence thesis by A2,EXTREAL1:19;
end;
hence thesis;
end;
theorem
z <> +infty & z <> -infty & x + z = y implies x = y - z
proof
assume that A1:z <> +infty and A2:z <> -infty and A3:x + z = y;
per cases;
suppose A4:x = +infty;
then x + z = +infty by A2,SUPINF_2:def 2;
hence thesis by A1,A3,A4,SUPINF_2:6;
suppose A5:x = -infty;
then x + z = -infty by A1,SUPINF_2:def 2;
hence thesis by A2,A3,A5,SUPINF_2:7;
suppose x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
reconsider c = z as Real by A1,A2,EXTREAL1:1;
y = a + c by A3,SUPINF_2:1;
then y - z = a + c - c by SUPINF_2:5;
hence thesis by XCMPLX_1:26;
end;
theorem :: extension of REAL_1:34
x <> +infty & x <> -infty & x <> 0. implies x*(1./x) = 1. & (1./x)*x = 1.
proof
assume A1:x <> +infty & x <> -infty & x <> 0.;
then reconsider a = x as Real by EXTREAL1:1;
1./x = 1/a by A1,EXTREAL1:32,MESFUNC1:def 8;
then x * (1. / x) = a * (1/a) by EXTREAL1:13
.= 1 by A1,SUPINF_2:def 1,XCMPLX_1:107;
hence thesis by MESFUNC1:def 8;
end;
theorem :: extension of REAL_1:36
x <> +infty & x <> -infty implies x - x = 0.
proof
assume x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
x - x = a - a by SUPINF_2:5 .= 0 by XCMPLX_1:14;
hence thesis by SUPINF_2:def 1;
end;
theorem Th14: :: extension of REAL_2:6
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) implies
-(x + y) = -x + -y & -(x + y) = -y - x & -(x + y) = -x - y
proof
assume A1:not ((x = +infty & y = -infty) or (x = -infty & y = +infty));
per cases;
suppose A2:x = +infty;
then A3: -x = -infty & y <> -infty by A1,SUPINF_2:def 3;
A4: -y <> +infty by A1,A2,EXTREAL1:4;
-(x + y) = -infty by A2,A3,SUPINF_2:def 2;
hence thesis by A2,A3,A4,SUPINF_2:6,7,def 2;
suppose A5:x = -infty;
then A6:-y <> -infty by A1,EXTREAL1:4;
-(x + y) = +infty by A1,A5,SUPINF_2:4,def 2;
hence thesis by A1,A5,A6,SUPINF_2:4,6,7,def 2;
suppose A7:x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
now per cases;
suppose A8:y = +infty;
then A9: -y = -infty by EXTREAL1:4;
A10: x + y = +infty by A7,A8,SUPINF_2:def 2;
-x <> +infty & -x <> -infty by A7,EXTREAL1:4;
hence thesis by A7,A8,A9,A10,SUPINF_2:6,7,def 2;
suppose A11:y = -infty;
then A12: -y = +infty by EXTREAL1:4;
A13: x + y = -infty by A7,A11,SUPINF_2:def 2;
-x <> +infty & -x <> -infty by A7,EXTREAL1:4;
hence thesis by A7,A11,A12,A13,SUPINF_2:6,7,def 2;
suppose y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
A14: x + y = a + b & -x = -a & -y = -b by SUPINF_2:1,3;
then A15: -(x + y) = -(a + b) by SUPINF_2:3 .= -a + - b by XCMPLX_1:140;
A16: -(x + y) = -(a + b) by A14,SUPINF_2:3 .= -b - a by XCMPLX_1:161;
-(x + y) = -(a + b) by A14,SUPINF_2:3 .= -a - b by XCMPLX_1:161;
hence thesis by A14,A15,A16,SUPINF_2:1,5;
end;
hence thesis;
end;
theorem Th15: :: extension of REAL_2:8
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) implies
-(x - y) = -x + y & -(x - y) = y - x
proof
assume not ((x= +infty & y = +infty) or (x= -infty & y = -infty));
then A1:not((x=+infty & -y =-infty) or (x=-infty & -y =+infty)) by EXTREAL1:4;
A2:-(x - y) = -(x + -y) by SUPINF_2:def 4;
then A3:-(x - y) = -x + -(-y) by A1,Th14 .= -x + y;
-(x - y) = -(-y) - x by A1,A2,Th14;
hence thesis by A3;
end;
theorem :: extension of REAL_2:9
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) implies
-(-x + y) = x - y & -(-x + y) = x + -y
proof
assume not ((x=+infty & y=+infty) or (x=-infty & y=-infty));
then A1:not ((-x=-infty & y=+infty) or (-x=+infty & y=-infty)) by EXTREAL1:4;
then A2:-(-x + y) = -(-x) + -y by Th14;
-(-x + y) = -(-x) - y by A1,Th14 .= x - y;
hence thesis by A2;
end;
theorem Th17:
(x = +infty & 0. <' y & y <' +infty) or (x = -infty & y <' 0. & -infty <' y)
implies x / y = +infty
proof
assume A1:(x=+infty & 0.<'y & y<'+infty) or (x=-infty & y<'0. & -infty<'y);
per cases by A1;
suppose x=+infty & 0.<'y & y<'+infty;
hence thesis by EXTREAL1:def 2,SUPINF_2:19;
suppose x=-infty & y<'0. & -infty<'y;
hence thesis by EXTREAL1:def 2,SUPINF_2:19;
end;
theorem Th18:
(x = +infty & y <' 0. & -infty <' y) or (x = -infty & 0. <' y & y <' +infty)
implies x / y = -infty
proof
assume A1:(x=+infty & y<'0. & -infty<'y) or (x=-infty & 0.<'y & y<'+infty);
per cases by A1;
suppose x=+infty & y<'0. & -infty<'y;
hence thesis by EXTREAL1:def 2,SUPINF_2:19;
suppose x=-infty & 0.<'y & y<'+infty;
hence thesis by EXTREAL1:def 2,SUPINF_2:19;
end;
theorem Th19: :: extension of REAL_2:62
-infty <' y & y <' +infty & y <> 0. implies x * y / y = x & x * (y / y) = x
proof
assume that A1:-infty <' y and A2:y <' +infty and A3:y <> 0.;
reconsider b = y as Real by A1,A2,EXTREAL1:1;
A4:x * y / y = x
proof
per cases;
suppose A5:x = +infty;
now per cases by A3,SUPINF_1:22;
suppose A6:0. <' y;
then x * y = +infty by A5,EXTREAL1:def 1;
hence thesis by A2,A5,A6,Th17;
suppose A7:y <' 0.;
then x * y = -infty by A5,EXTREAL1:def 1;
hence thesis by A1,A5,A7,Th17;
end;
hence thesis;
suppose A8:x = -infty;
now per cases by A3,SUPINF_1:22;
suppose A9:0. <'y;
then x * y = -infty by A8,EXTREAL1:def 1;
hence thesis by A2,A8,A9,Th18;
suppose A10:y <' 0.;
then x * y = +infty by A8,EXTREAL1:def 1;
hence thesis by A1,A8,A10,Th18;
end;
hence thesis;
suppose x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
x * y = a * b by EXTREAL1:13;
then (x * y)/y = (a * b)/b by A3,EXTREAL1:32
.= a by A3,SUPINF_2:def 1,XCMPLX_1:90;
hence thesis;
end;
y / y = 1. by A1,A2,A3,EXTREAL1:34,MESFUNC1:def 8;
hence thesis by A4,Th4;
end;
theorem Th20:
1. <' +infty & -infty <' 1. by MESFUNC1:def 8,SUPINF_1:31;
theorem
x = +infty or x = -infty implies
(for y st y in REAL holds x + y <> 0.)
proof
assume A1:x = +infty or x = -infty;
given y such that
A2:y in REAL & x + y = 0.;
A3:y <> -infty & y <> +infty by A2,SUPINF_1:31;
per cases by A1;
suppose x = +infty;
hence contradiction by A2,A3,SUPINF_2:19,def 2;
suppose x = -infty;
hence contradiction by A2,A3,SUPINF_2:19,def 2;
end;
theorem
x = +infty or x = -infty implies
for y holds x * y <> 1.
proof
assume A1:x = +infty or x = -infty;
given y such that
A2:x * y = 1.;
per cases by SUPINF_1:22;
suppose y = 0.;
then x * y = 0. by EXTREAL1:def 1;
hence contradiction by A2,EXTREAL1:18,MESFUNC1:def 8;
suppose A3:0. <' y;
now per cases by A1;
suppose x = +infty;
hence contradiction by A2,A3,Th20,EXTREAL1:def 1;
suppose x = -infty;
hence contradiction by A2,A3,Th20,EXTREAL1:def 1;
end;
hence thesis;
suppose A4:y <' 0.;
now per cases by A1;
suppose x = +infty;
hence contradiction by A2,A4,Th20,EXTREAL1:def 1;
suppose x = -infty;
hence contradiction by A2,A4,Th20,EXTREAL1:def 1;
end;
hence thesis;
end;
theorem Th23:
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
x + y <' +infty implies x <> +infty & y <> +infty
proof
assume that A1:not ((x=+infty & y=-infty) or (x=-infty & y=+infty)) and
A2:x + y <' +infty;
assume A3:x = +infty or y = +infty;
per cases by A3;
suppose x = +infty;
hence contradiction by A1,A2,SUPINF_2:def 2;
suppose y = +infty;
hence contradiction by A1,A2,SUPINF_2:def 2;
end;
theorem Th24:
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
-infty <' x + y implies x <> -infty & y <> -infty
proof
assume that A1:not ((x=+infty & y=-infty) or (x=-infty & y=+infty)) and
A2:-infty <' x + y;
assume A3:x = -infty or y = -infty;
per cases by A3;
suppose x = -infty;
hence contradiction by A1,A2,SUPINF_2:def 2;
suppose y = -infty;
hence contradiction by A1,A2,SUPINF_2:def 2;
end;
theorem Th25:
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) &
x - y <' +infty implies x <> +infty & y <> -infty
proof
assume that A1:not ((x=+infty & y=+infty) or (x=-infty & y=-infty)) and
A2:x - y <' +infty;
assume A3:x = +infty or y = -infty;
per cases by A3;
suppose x = +infty;
hence contradiction by A1,A2,SUPINF_2:6;
suppose y = -infty;
hence contradiction by A1,A2,SUPINF_2:7;
end;
theorem Th26:
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) &
-infty <' x - y implies x <> -infty & y <> +infty
proof
assume that A1:not ((x=+infty & y=+infty) or (x=-infty & y=-infty)) and
A2:-infty <' x - y;
assume A3:x = -infty or y = +infty;
per cases by A3;
suppose x = -infty;
hence contradiction by A1,A2,SUPINF_2:7;
suppose y = +infty;
hence contradiction by A1,A2,SUPINF_2:6;
end;
theorem
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
x + y <' z implies x <> +infty & y <> +infty & z <> -infty & x <' z - y
proof
assume that A1:not ((x=+infty & y=-infty) or (x=-infty & y=+infty)) and
A2:x + y <' z;
per cases;
suppose A3:z = +infty;
then A4: x<>+infty & y<>+infty & z<>-infty by A1,A2,Th23,SUPINF_1:14;
x <=' +infty by SUPINF_1:20;
then x <' +infty & z - y = +infty by A3,A4,SUPINF_1:22,SUPINF_2:6;
hence thesis by A1,A2,A3,Th23,SUPINF_1:14;
suppose A5:z <> +infty;
A6: z <=' +infty by SUPINF_1:20;
then A7: x + y <' +infty by A2,SUPINF_1:29;
then A8: x <> +infty & y <> +infty by A1,Th23;
A9: -infty <=' x + y by SUPINF_1:21;
then reconsider c = z as Real by A2,A5,EXTREAL1:1;
now per cases;
suppose A10:y = -infty;
then x <> +infty & x <=' +infty by A1,SUPINF_1:20;
then x <' +infty by SUPINF_1:22;
hence thesis by A2,A6,A9,A10,SUPINF_1:29,SUPINF_2:7;
suppose y <> -infty;
then reconsider b = y as Real by A8,EXTREAL1:1;
now per cases;
suppose A11:x = -infty;
z - y = c - b by SUPINF_2:5;
hence thesis by A6,A11,SUPINF_1:31;
suppose x <> -infty;
then reconsider a = x as Real by A8,EXTREAL1:1;
A12: x + y = a + b & z = c by SUPINF_2:1;
then consider p,q being Real such that
A13: p = x + y & q = z & p <= q by A2,SUPINF_1:16;
a + b < c by A2,A12,A13,REAL_1:def 5;
then A14: a < c - b by REAL_1:86;
x = a & z - y = c - b by SUPINF_2:5;
hence thesis by A1,A2,A7,A14,Th23,HAHNBAN:12,SUPINF_1:21;
end;
hence thesis;
end;
hence thesis;
end;
theorem
not ((z = +infty & y = +infty) or (z = -infty & y = -infty)) &
x <' z - y implies x <> +infty & y <> +infty & z <> -infty & x + y <' z
proof
assume that A1:not ((z=+infty & y=+infty) or (z=-infty & y=-infty)) and
A2:x <' z - y;
per cases;
suppose A3:x = -infty;
then A4: x<>+infty & y<>+infty & z<>-infty by A1,A2,Th26,SUPINF_1:14;
-infty <=' z by SUPINF_1:21;
then -infty <' z & x + y = -infty by A3,A4,SUPINF_1:22,SUPINF_2:def 2;
hence thesis by A1,A2,A3,Th26,SUPINF_1:14;
suppose A5:x <> -infty;
A6: -infty <=' x by SUPINF_1:21;
then A7: -infty <' z - y by A2,SUPINF_1:29;
then A8: z <> -infty & y <> +infty by A1,Th26;
A9: z - y <=' +infty by SUPINF_1:20;
then reconsider a = x as Real by A2,A5,EXTREAL1:1;
now per cases;
suppose A10:y = -infty;
then z <> -infty & -infty <=' z by A1,SUPINF_1:21;
then -infty <' z by SUPINF_1:22;
hence thesis by A2,A6,A9,A10,SUPINF_1:29,SUPINF_2:def 2;
suppose y <> -infty;
then reconsider b = y as Real by A8,EXTREAL1:1;
now per cases;
suppose A11:z = +infty;
x + y = a + b by SUPINF_2:1;
hence thesis by A6,A11,SUPINF_1:31;
suppose z <> +infty;
then reconsider c = z as Real by A8,EXTREAL1:1;
A12: x = a & z - y = c - b by SUPINF_2:5;
then consider p,q being Real such that
A13: p = x & q = z - y & p <= q by A2,SUPINF_1:16;
a < c - b by A2,A12,A13,REAL_1:def 5;
then A14: a + b < c by REAL_1:86;
x + y = a + b & z = c by SUPINF_2:1;
hence thesis by A1,A2,A7,A14,Th26,HAHNBAN:12,SUPINF_1:20;
end;
hence thesis;
end;
hence thesis;
end;
theorem
not ((x = +infty & y = +infty) or (x = -infty & y = -infty)) &
x - y <' z implies x <> +infty & y <> -infty & z <> -infty & x <' z + y
proof
assume that A1:not ((x=+infty & y=+infty) or (x=-infty & y=-infty)) and
A2:x - y <' z;
per cases;
suppose A3:z = +infty;
then A4: x<>+infty & y<>-infty & z<>-infty by A1,A2,Th25,SUPINF_1:14;
x <=' +infty by SUPINF_1:20;
then x <' +infty & z + y = +infty by A3,A4,SUPINF_1:22,SUPINF_2:def 2;
hence thesis by A1,A2,A3,Th25,SUPINF_1:14;
suppose A5:z <> +infty;
A6: z <=' +infty by SUPINF_1:20;
then A7: x - y <' +infty by A2,SUPINF_1:29;
then A8: x <> +infty & y <> -infty by A1,Th25;
A9: -infty <=' x - y by SUPINF_1:21;
then reconsider c = z as Real by A2,A5,EXTREAL1:1;
now per cases;
suppose A10:y = +infty;
then x <> +infty & x <=' +infty by A1,SUPINF_1:20;
then x <' +infty by SUPINF_1:22;
hence thesis by A2,A6,A9,A10,SUPINF_1:29,SUPINF_2:def 2;
suppose y <> +infty;
then reconsider b = y as Real by A8,EXTREAL1:1;
now per cases;
suppose A11:x = -infty;
z + y = c + b by SUPINF_2:1;
hence thesis by A6,A11,SUPINF_1:31;
suppose x <> -infty;
then reconsider a = x as Real by A8,EXTREAL1:1;
A12: x - y = a - b & z = c by SUPINF_2:5;
then consider p,q being Real such that
A13: p = x - y & q = z & p <= q by A2,SUPINF_1:16;
a - b < c by A2,A12,A13,REAL_1:def 5;
then A14: a < c + b by REAL_1:84;
x = a & z + y = c + b by SUPINF_2:1;
hence thesis by A1,A2,A7,A14,Th25,HAHNBAN:12,SUPINF_1:21;
end;
hence thesis;
end;
hence thesis;
end;
theorem
not ((z = +infty & y = -infty) or (z = -infty & y = +infty)) &
x <' z + y implies x <> +infty & y <> -infty & z <> -infty & x - y <' z
proof
assume that A1:not ((z=+infty & y=-infty) or (z=-infty & y=+infty)) and
A2:x <' z + y;
per cases;
suppose A3:x = -infty;
then A4: x<>+infty & y<>-infty & z<>-infty by A1,A2,Th24,SUPINF_1:14;
-infty <=' z by SUPINF_1:21;
then -infty <' z & x - y = -infty by A3,A4,SUPINF_1:22,SUPINF_2:7;
hence thesis by A1,A2,A3,Th24,SUPINF_1:14;
suppose A5:x <> -infty;
A6: -infty <=' x by SUPINF_1:21;
then A7: -infty <' z + y by A2,SUPINF_1:29;
then A8: z <> -infty & y <> -infty by A1,Th24;
A9: z + y <=' +infty by SUPINF_1:20;
then reconsider a = x as Real by A2,A5,EXTREAL1:1;
now per cases;
suppose A10:y = +infty;
then z <> -infty & -infty <=' z by A1,SUPINF_1:21;
then -infty <' z by SUPINF_1:22;
hence thesis by A2,A6,A9,A10,SUPINF_1:29,SUPINF_2:6;
suppose y <> +infty;
then reconsider b = y as Real by A8,EXTREAL1:1;
now per cases;
suppose A11:z = +infty;
x - y = a - b by SUPINF_2:5;
hence thesis by A6,A11,SUPINF_1:31;
suppose z <> +infty;
then reconsider c = z as Real by A8,EXTREAL1:1;
A12: x = a & z + y = c + b by SUPINF_2:1;
then consider p,q being Real such that
A13: p = x & q = z + y & p <= q by A2,SUPINF_1:16;
a < c + b by A2,A12,A13,REAL_1:def 5;
then A14: a - b < c by REAL_1:84;
x - y = a - b & z = c by SUPINF_2:5;
hence thesis by A1,A2,A7,A14,Th24,HAHNBAN:12,SUPINF_1:20;
end;
hence thesis;
end;
hence thesis;
end;
theorem
not ((x = +infty & y = -infty) or (x = -infty & y = +infty) or
(y = +infty & z = +infty) or (y = -infty & z = -infty)) &
x + y <=' z implies y <> +infty & x <=' z - y
proof
assume that A1:not ((x=+infty & y=-infty) or (x=-infty & y=+infty) or
(y = +infty & z = +infty) or (y = -infty & z = -infty)) and
A2:x + y <=' z;
thus y <> +infty
proof
assume A3:y = +infty;
then x + y = +infty by A1,SUPINF_2:def 2;
hence contradiction by A1,A2,A3,SUPINF_1:24;
end;
per cases;
suppose z = +infty;
then z - y = +infty by A1,SUPINF_2:6;
hence thesis by SUPINF_1:20;
suppose A4:z <> +infty;
z <=' +infty by SUPINF_1:20;
then z <' +infty by A4,SUPINF_1:22;
then x + y <' +infty by A2,SUPINF_1:29;
then A5: x <> +infty & y <> +infty by A1,Th23;
now per cases;
suppose x = -infty;
hence thesis by SUPINF_1:21;
suppose x <> -infty;
then reconsider a = x as Real by A5,EXTREAL1:1;
now per cases;
suppose y = -infty;
then z - y = +infty by A1,SUPINF_2:7;
hence thesis by SUPINF_1:20;
suppose y <> -infty;
then reconsider b = y as Real by A5,EXTREAL1:1;
A6: x + y = a + b by SUPINF_2:1;
then z <> -infty by A2,SUPINF_1:31;
then reconsider c = z as Real by A4,EXTREAL1:1;
z = c;
then consider p,q being Real such that
A7: p = x + y & q = z & p <= q by A2,A6,SUPINF_1:16;
A8: a <= c - b by A6,A7,REAL_1:84;
x = a & z - y = c - b by SUPINF_2:5;
hence thesis by A8,SUPINF_1:16;
end;
hence thesis;
end;
hence thesis;
end;
theorem
not (x = +infty & y = -infty) & not (x = -infty & y = +infty) &
not (y = +infty & z = +infty) &
x <=' z - y implies y <> +infty & x + y <=' z
proof
assume that
A1:not (x = +infty & y = -infty) and
A2:not (x = -infty & y = +infty) and
A3:not (y = +infty & z = +infty) and
A4:x <=' z - y;
thus A5:y <> +infty
proof
assume A6:y = +infty;
then z - y = -infty by A3,SUPINF_2:6;
hence contradiction by A2,A4,A6,SUPINF_1:23;
end;
per cases by A5;
suppose y = -infty;
then x + y = -infty by A1,SUPINF_2:def 2;
hence thesis by SUPINF_1:21;
suppose A7:y <> +infty & y <> -infty;
then A8: y is Real by EXTREAL1:1;
- +infty = -infty & - -infty = +infty by SUPINF_2:4;
then A9: -y <> -infty & -y <> +infty by A7;
z - y + y = z + -y + y by SUPINF_2:def 4
.= z + (-y + y) by A7,A9,EXTREAL1:8
.= z + 0. by EXTREAL1:9 .= z by SUPINF_2:18;
hence thesis by A4,A8,MEASURE6:11;
end;
theorem
not ((x = +infty & y = +infty) or (x = -infty & y = -infty) or
(y = +infty & z = -infty) or (y = -infty & z = +infty)) &
x - y <=' z implies y <> -infty & x <=' z + y
proof
assume that A1:not ((x=+infty & y=+infty) or (x=-infty & y=-infty) or
(y = +infty & z = -infty) or (y = -infty & z = +infty)) and
A2:x - y <=' z;
thus y <> -infty
proof
assume A3:y = -infty;
then x - y = +infty by A1,SUPINF_2:7;
hence contradiction by A1,A2,A3,SUPINF_1:24;
end;
per cases;
suppose z = +infty;
then z + y = +infty by A1,SUPINF_2:def 2;
hence thesis by SUPINF_1:20;
suppose A4:z <> +infty;
z <=' +infty by SUPINF_1:20;
then z <' +infty by A4,SUPINF_1:22;
then x - y <' +infty by A2,SUPINF_1:29;
then A5: x <> +infty & y <> -infty by A1,Th25;
now per cases;
suppose x = -infty;
hence thesis by SUPINF_1:21;
suppose x <> -infty;
then reconsider a = x as Real by A5,EXTREAL1:1;
now per cases;
suppose y = +infty;
then z + y = +infty by A1,SUPINF_2:def 2;
hence thesis by SUPINF_1:20;
suppose y <> +infty;
then reconsider b = y as Real by A5,EXTREAL1:1;
A6: x - y = a - b by SUPINF_2:5;
then z <> -infty by A2,SUPINF_1:31;
then reconsider c = z as Real by A4,EXTREAL1:1;
z = c;
then consider p,q being Real such that
A7: p = x - y & q = z & p <= q by A2,A6,SUPINF_1:16;
A8: a <= c + b by A6,A7,REAL_1:86;
x = a & z + y = c + b by SUPINF_2:1;
hence thesis by A8,SUPINF_1:16;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th34:
not (x = +infty & y = +infty) & not (x = -infty & y = -infty) &
not (y = -infty & z = +infty) &
x <=' z + y implies y <> -infty & x - y <=' z
proof
assume that A1:not(x=+infty & y=+infty) and A2:not(x=-infty & y=-infty) and
A3:not(y = -infty & z = +infty) and
A4:x <=' z + y;
thus A5:y <> -infty
proof
assume A6:y = -infty;
then z + y = -infty by A3,SUPINF_2:def 2;
hence contradiction by A2,A4,A6,SUPINF_1:23;
end;
per cases by A5;
suppose y = +infty;
then x - y = -infty by A1,SUPINF_2:6;
hence thesis by SUPINF_1:21;
suppose A7:y <> +infty & y <> -infty;
then A8:y is Real by EXTREAL1:1;
y - y = y + (-y) by SUPINF_2:def 4 .= 0. by EXTREAL1:9;
then z + y - y = z + 0. by A7,EXTREAL1:11 .= z by SUPINF_2:18;
hence thesis by A4,A8,MEASURE6:11;
end;
canceled 5;
theorem :: extension of REAL_1:27
not (x = +infty & y = +infty) & not (x = -infty & y = -infty) &
not (y = +infty & z = -infty) & not (y = -infty & z = +infty) &
not (x = +infty & z = +infty) & not (x = -infty & z = -infty)
implies x - y - z = x - (y + z)
proof
assume that A1:not(x=+infty & y=+infty) and A2: not(x=-infty & y=-infty) and
A3:not (y = +infty & z = -infty) and A4: not (y = -infty & z = +infty) and
A5:not (x = +infty & z = +infty) and A6: not (x = -infty & z = -infty);
per cases;
suppose A7:x = +infty;
then x - y = +infty by A1,SUPINF_2:6;
then A8: x - y - z = +infty by A5,A7,SUPINF_2:6;
y + z <> +infty by A1,A5,A7,SUPINF_2:8;
hence thesis by A7,A8,SUPINF_2:6;
suppose A9:x = -infty;
then x - y = -infty by A2,SUPINF_2:7;
then A10:x - y - z = -infty by A6,A9,SUPINF_2:7;
y + z <> -infty by A2,A6,A9,SUPINF_2:9;
hence thesis by A9,A10,SUPINF_2:7;
suppose A11:x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
now per cases;
suppose A12:y = +infty;
then x - y = -infty & y + z = +infty by A3,A11,SUPINF_2:6,def 2;
hence thesis by A3,A12,SUPINF_2:7;
suppose A13:y = -infty;
then x - y = +infty & y + z = -infty by A4,A11,SUPINF_2:7,def 2;
hence thesis by A4,A13,SUPINF_2:6;
suppose A14:y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
A15: x - y = a - b by SUPINF_2:5;
then A16: x - y <> +infty & x - y <> -infty by SUPINF_1:31;
now per cases;
suppose z = +infty;
then x - y - z = -infty & y + z = +infty by A14,A16,SUPINF_2:6,def 2;
hence thesis by A11,SUPINF_2:6;
suppose z = -infty;
then x - y - z = +infty & y + z = -infty by A14,A16,SUPINF_2:7,def 2;
hence thesis by A11,SUPINF_2:7;
suppose z <> +infty & z <> -infty;
then reconsider c = z as Real by EXTREAL1:1;
A17: x - y - z = a - b - c & y + z = b + c by A15,SUPINF_2:1,5;
then x - (y + z) = a - (b + c) by SUPINF_2:5;
hence thesis by A17,XCMPLX_1:36;
end;
hence thesis;
end;
hence thesis;
end;
theorem :: extension of REAL_1:28
not (x = +infty & y = +infty) & not (x = -infty & y = -infty) &
not (y = +infty & z = +infty) & not (y = -infty & z = -infty) &
not (x = +infty & z = -infty) & not (x = -infty & z = +infty)
implies x - y + z = x - (y - z)
proof
assume that A1:not(x=+infty & y=+infty) and A2: not(x=-infty & y=-infty) and
A3:not (y = +infty & z = +infty) and A4: not (y = -infty & z = -infty) and
A5:not (x = +infty & z = -infty) and A6: not (x = -infty & z = +infty);
per cases;
suppose A7:x = +infty;
then x - y = +infty by A1,SUPINF_2:6;
then A8: x - y + z = +infty by A5,A7,SUPINF_2:def 2;
y - z <> +infty by A1,A5,A7,SUPINF_2:10;
hence thesis by A7,A8,SUPINF_2:6;
suppose A9:x = -infty;
then x - y = -infty by A2,SUPINF_2:7;
then A10:x - y + z = -infty by A6,A9,SUPINF_2:def 2;
y - z <> -infty by A2,A6,A9,SUPINF_2:11;
hence thesis by A9,A10,SUPINF_2:7;
suppose A11:x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
now per cases;
suppose A12:y = +infty;
then x - y = -infty & y - z = +infty by A3,A11,SUPINF_2:6;
hence thesis by A3,A12,SUPINF_2:def 2;
suppose A13:y = -infty;
then x - y = +infty & y - z = -infty by A4,A11,SUPINF_2:7;
hence thesis by A4,A13,SUPINF_2:def 2;
suppose A14:y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
A15: x - y = a - b by SUPINF_2:5;
then A16: x - y <> +infty & x - y <> -infty by SUPINF_1:31;
now per cases;
suppose z = +infty;
then x - y + z = +infty & y - z = -infty by A14,A16,SUPINF_2:6,def 2;
hence thesis by A11,SUPINF_2:7;
suppose z = -infty;
then x - y + z = -infty & y - z = +infty by A14,A16,SUPINF_2:7,def 2;
hence thesis by A11,SUPINF_2:6;
suppose z <> +infty & z <> -infty;
then reconsider c = z as Real by EXTREAL1:1;
A17: x - y + z = a - b + c & y - z = b - c by A15,SUPINF_2:1,5;
then x - (y - z) = a - (b - c) by SUPINF_2:5;
hence thesis by A17,XCMPLX_1:37;
end;
hence thesis;
end;
hence thesis;
end;
theorem
x * y <> +infty & x * y <> -infty implies x is Real or y is Real
proof
assume A1:x * y <> +infty & x * y <> -infty;
assume A2:not (x is Real or y is Real);
per cases by A2,EXTREAL1:1;
suppose x = +infty & y = +infty;
hence contradiction by A1,EXTREAL1:def 1,SUPINF_2:19;
suppose x = +infty & y = -infty;
hence contradiction by A1,EXTREAL1:def 1,SUPINF_2:19;
suppose x = -infty & y = +infty;
hence contradiction by A1,EXTREAL1:def 1,SUPINF_2:19;
suppose x = -infty & y = -infty;
hence contradiction by A1,EXTREAL1:def 1,SUPINF_2:19;
end;
theorem Th43: :: extension of EXTREAL1:21
(0. <' x & 0. <' y) or (x <' 0. & y <' 0.) iff 0. <' x * y
proof
0. <' x * y implies (0. <' x & 0. <' y) or (x <' 0. & y <' 0.)
proof
assume A1:0. <' x * y;
assume A2:not ((0. <' x & 0. <' y) or (x <' 0. & y <' 0.));
per cases by A2;
suppose x <=' 0. & 0. <=' x;
then x = 0. by SUPINF_1:22;
hence contradiction by A1,EXTREAL1:def 1;
suppose A3:x <=' 0. & 0. <=' y;
now per cases by A3,SUPINF_1:22;
suppose x = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose A4:x <' 0.;
now per cases by A3,SUPINF_1:22;
suppose y = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose 0. <' y;
hence contradiction by A1,A4,EXTREAL1:21;
end;
hence thesis;
end;
hence thesis;
suppose A5:0. <=' x & y <=' 0.;
now per cases by A5,SUPINF_1:22;
suppose x = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose A6:0. <' x;
now per cases by A5,SUPINF_1:22;
suppose y = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose y <' 0.;
hence contradiction by A1,A6,EXTREAL1:21;
end;
hence thesis;
end;
hence thesis;
suppose y <=' 0. & 0. <=' y;
then y = 0. by SUPINF_1:22;
hence contradiction by A1,EXTREAL1:def 1;
end;
hence thesis by EXTREAL1:20;
end;
theorem Th44: :: extension of EXTREAL1:22
(0. <' x & y <' 0.) or (x <' 0. & 0. <' y) iff x * y <' 0.
proof
x * y <' 0. implies (0. <' x & y <' 0.) or (x <' 0. & 0. <' y)
proof
assume A1:x * y <' 0.;
assume A2:not ((0. <' x & y <' 0.) or (x <' 0. & 0. <' y));
per cases by A2;
suppose x <=' 0. & 0. <=' x;
then x = 0. by SUPINF_1:22;
hence contradiction by A1,EXTREAL1:def 1;
suppose A3:x <=' 0. & y <=' 0.;
now per cases by A3,SUPINF_1:22;
suppose x = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose A4:x <' 0.;
now per cases by A3,SUPINF_1:22;
suppose y = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose y <' 0.;
hence contradiction by A1,A4,EXTREAL1:20;
end;
hence thesis;
end;
hence thesis;
suppose A5:0. <=' x & 0. <=' y;
now per cases by A5,SUPINF_1:22;
suppose x = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose A6:0. <' x;
now per cases by A5,SUPINF_1:22;
suppose y = 0.;
hence contradiction by A1,EXTREAL1:def 1;
suppose 0. <' y;
hence contradiction by A1,A6,EXTREAL1:20;
end;
hence thesis;
end;
hence thesis;
suppose y <=' 0. & 0. <=' y;
then y = 0. by SUPINF_1:22;
hence contradiction by A1,EXTREAL1:def 1;
end;
hence thesis by EXTREAL1:21;
end;
theorem :: extension of REAL_2:121
((0. <=' x or 0. <' x) & (0. <=' y or 0. <' y)) or
((x <=' 0. or x <' 0.) & (y <=' 0. or y <' 0.))
iff 0. <=' x * y by Th44;
theorem :: extension of REAL_2:123
((x <=' 0. or x <' 0.) & (0. <=' y or 0. <' y)) or
((0. <=' x or 0. <' x) & (y <=' 0. or y <' 0.))
iff x * y <=' 0. by Th43;
theorem Th47:
(x <=' -y iff y <=' -x) & (-x <=' y iff -y <=' x)
proof
x <=' -y iff -(-y) <=' -x by SUPINF_2:16;
hence x <=' -y iff y <=' -x;
-x <=' y iff -y <=' -(-x) by SUPINF_2:16;
hence thesis;
end;
theorem Th48:
(x <' -y iff y <' -x) & (-x <' y iff -y <' x)
proof
x <' -y iff -(-y) <' -x by SUPINF_2:17;
hence x <' -y iff y <' -x;
-x <' y iff -y <' -(-x) by SUPINF_2:17;
hence thesis;
end;
begin :: Basic properties of absolute value for extended real numbers
theorem Th49:
x = a implies |.x.| = abs(a)
proof
assume A1:x = a;
per cases;
suppose A2:0. <=' x;
then A3: |.x.| = a by A1,EXTREAL1:def 3;
0 <= a by A1,A2,EXTREAL1:19;
hence thesis by A3,ABSVALUE:def 1;
suppose A4:not 0. <=' x;
then A5: |.x.| = -x by EXTREAL1:37 .= -a by A1,SUPINF_2:3;
a < 0 by A1,A4,EXTREAL1:19;
hence thesis by A5,ABSVALUE:def 1;
end;
theorem Th50:
|.x.| = x or |.x.| = -x
proof
per cases;
suppose 0. <=' x;
hence thesis by EXTREAL1:def 3;
suppose not 0. <=' x;
hence thesis by EXTREAL1:def 3;
end;
theorem Th51: :: extension of ABSVALUE:5
0. <=' |.x.|
proof
per cases;
suppose 0. <=' x;
hence thesis by EXTREAL1:def 3;
suppose A1:not (0. <=' x);
then |.x.| = -x by EXTREAL1:def 3;
hence thesis by A1,EXTREAL1:25;
end;
theorem Th52: :: extension of ABSVALUE:6
x <> 0. implies 0. <' |.x.|
proof
assume A1:x <> 0.;
per cases;
suppose 0. <=' x;
then 0. <' x by A1,SUPINF_1:22;
hence thesis by EXTREAL1:def 3;
suppose A2:not (0. <=' x);
then 0. <' -x by EXTREAL1:25;
hence thesis by A2,EXTREAL1:def 3;
end;
theorem :: extension of ABSVALUE:7
x = 0. iff |.x.| = 0. by Th52,EXTREAL1:def 3;
theorem :: extension of ABSVALUE:9
|.x.| = -x & x <> 0. implies x <' 0.
proof
assume A1:|.x.| = -x & x <> 0.;
assume A2: not x <' 0.;
then A3:-x = x by A1,EXTREAL1:def 3;
0. <' x by A1,A2,SUPINF_1:22;
hence contradiction by A3,EXTREAL1:25;
end;
theorem Th55:
x <=' 0. implies |.x.| = -x
proof
assume A1:x <=' 0.;
per cases by A1,SUPINF_1:22;
suppose x <' 0.;
hence thesis by EXTREAL1:def 3;
suppose x = 0.;
hence thesis by EXTREAL1:24,def 3;
end;
theorem :: extension of ABSVALUE:10
|.x * y.| = |.x.| * |.y.|
proof
per cases by SUPINF_1:22;
suppose x = 0.;
then x * y = 0. & |.x.| = 0. by EXTREAL1:22,def 3;
then |.x * y.| = 0. & |.x.| * |.y.| = 0. by EXTREAL1:22,def 3;
hence thesis;
suppose A1:0. <' x;
now per cases by SUPINF_1:22;
suppose y = 0.;
then x * y = 0. & |.y.| = 0. by EXTREAL1:22,def 3;
then |.x * y.| = 0. & |.x.| * |.y.| = 0. by EXTREAL1:22,def 3;
hence thesis;
suppose 0. <' y;
then 0. <=' x * y & |.x.| = x & |.y.| = y by A1,EXTREAL1:20,def 3;
hence thesis by EXTREAL1:def 3;
suppose A2:y <' 0.;
then |.x.| = x & |.y.| = -y by A1,EXTREAL1:def 3;
then A3: |.x.| * |.y.| = -(x * y) by EXTREAL1:26;
x * y <' 0. by A1,A2,EXTREAL1:21;
hence thesis by A3,EXTREAL1:def 3;
end;
hence thesis;
suppose A4:x <' 0.;
now per cases by SUPINF_1:22;
suppose y = 0.;
then x * y = 0. & |.y.| = 0. by EXTREAL1:22,def 3;
then |.x * y.| = 0. & |.x.| * |.y.| = 0. by EXTREAL1:22,def 3;
hence thesis;
suppose 0. <' y;
then not 0. <=' x * y & |.y.| = y by A4,EXTREAL1:21,def 3;
then |.x * y.| = -(x * y) & |.x.| * |.y.| = (-x) * y by A4,EXTREAL1:def 3
;
hence thesis by EXTREAL1:26;
suppose y <' 0.;
then A5: 0. <=' x * y & |.y.| = -y by A4,EXTREAL1:20,def 3;
then |.x * y.| = x * y & |.x.| * |.y.| = (-x) * (-y) by A4,EXTREAL1:def 3;
then |.x.| * |.y.| = -(x * (-y)) by EXTREAL1:26 .= -(-(x * y)) by EXTREAL1
:26;
hence thesis by A5,EXTREAL1:def 3;
end;
hence thesis;
end;
theorem Th57: :: extension of ABSVALUE:11
-|.x.| <=' x & x <=' |.x.|
proof
per cases;
suppose A1:0. <=' x;
0. <=' |.x.| by Th51;
then -|.x.| <=' 0. by EXTREAL1:24,SUPINF_2:16;
hence thesis by A1,EXTREAL1:def 3,SUPINF_1:29;
suppose A2:not 0. <=' x;
then A3: |.x.|=-x by EXTREAL1:def 3;
0. <' -x by A2,EXTREAL1:25;
hence thesis by A2,A3,SUPINF_1:29;
end;
theorem Th58:
|.x.| <' y implies -y <' x & x <' y
proof
assume A1:|.x.| <' y;
per cases;
suppose A2:0. <=' x;
then A3: x <' y by A1,EXTREAL1:def 3;
-x <=' -0. by A2,SUPINF_2:16;
then -x <=' x by A2,EXTREAL1:24,SUPINF_1:29;
then -x <' y by A3,SUPINF_1:29;
hence thesis by A1,A2,Th48,EXTREAL1:def 3;
suppose A4:not 0. <=' x;
then A5: |.x.|=-x by EXTREAL1:def 3;
0. <' -x by A4,EXTREAL1:25;
then 0. <' y by A1,A5,SUPINF_1:29;
hence thesis by A1,A4,A5,Th48,SUPINF_1:29;
end;
theorem Th59:
-y <' x & x <' y implies 0. <' y & |.x.| <' y
proof
assume A1:-y <' x & x <' y;
per cases;
suppose 0. <=' x;
hence thesis by A1,EXTREAL1:def 3,SUPINF_1:29;
suppose A2:not 0. <=' x;
then 0. <' -x & -x <' y by A1,Th48,EXTREAL1:25;
hence thesis by A2,EXTREAL1:def 3,SUPINF_1:29;
end;
theorem Th60: :: extension of ABSVALUE:12
-y <=' x & x <=' y iff |.x.| <=' y
proof
A1:-y <=' x & x <=' y implies |.x.| <=' y
proof
assume A2:-y <=' x & x <=' y;
per cases;
suppose 0. <=' x;
hence thesis by A2,EXTREAL1:def 3;
suppose A3:not 0. <=' x;
then 0. <' -x & -x <=' y by A2,Th47,EXTREAL1:25;
hence thesis by A3,EXTREAL1:def 3;
end;
|.x.| <=' y implies -y <=' x & x <=' y
proof
assume A4:|.x.| <=' y;
per cases by A4,SUPINF_1:22;
suppose |.x.| = y;
hence thesis by Th57;
suppose |.x.| <' y;
hence thesis by Th58;
end;
hence thesis by A1;
end;
theorem Th61: :: extension of ABSVALUE:13
not ((x = +infty & y = -infty) or (x = -infty & y = +infty)) implies
|.x + y.| <=' |.x.| + |.y.|
proof
assume A1:not ((x = +infty & y = -infty) or (x = -infty & y = +infty));
A2:-|.x.| <=' x & x <=' |.x.| & -|.y.| <=' y & y <=' |.y.| by Th57;
per cases;
suppose A3:x = +infty;
then +infty <=' |.x.| & y <> -infty & -infty <=' y by A1,Th57,SUPINF_1:21;
then A4: |.x.| = +infty & -infty <' y by SUPINF_1:22,24;
now per cases;
suppose A5:y = +infty;
then |.y.| = +infty by A2,SUPINF_1:24;
then -|.y.| <> +infty by SUPINF_1:14,SUPINF_2:def 3;
then A6: -|.x.|+(-|.y.|) <=' x + y by A2,A3,A5,SUPINF_1:14,SUPINF_2:14;
-|.x.|+(-|.y.|) = -(|.x.|+|.y.|) by A2,A4,A5,Th14;
hence thesis by A3,A4,A5,A6,Th60;
suppose A7:y <> +infty;
then A8: x + y <=' |.x.| + |.y.| by A2,A4,SUPINF_1:14,SUPINF_2:14;
A9: -|.x.| <> +infty by A4,SUPINF_1:14,SUPINF_2:def 3;
y <=' +infty by SUPINF_1:20;
then -|.y.| <> +infty by A2,A7,SUPINF_1:22;
then A10: -|.x.|+(-|.y.|) <=' x + y by A1,A2,A9,SUPINF_2:14;
-|.x.|+(-|.y.|) = -(|.x.|+|.y.|) by A2,A4,Th14,SUPINF_1:14;
hence thesis by A8,A10,Th60;
end;
hence thesis;
suppose A11:x = -infty;
then A12:-|.x.| = -infty by A2,SUPINF_1:23;
A13:|.x.| <> -infty by A2,A11,SUPINF_1:14,23,SUPINF_2:4;
now per cases;
suppose A14:y = -infty;
then A15: -|.y.| <=' -infty by Th57;
then A16: -|.y.| = -infty by SUPINF_1:23;
A17: |.y.| <> -infty by A15,SUPINF_1:14,23,SUPINF_2:4;
A18: x + y <=' |.x.| + |.y.| by A2,A11,A12,A14,SUPINF_1:14,SUPINF_2:4,14;
-|.x.|+(-|.y.|) = -(|.x.|+|.y.|) by A12,A17,Th14,SUPINF_1:14,SUPINF_2:4;
hence thesis by A11,A14,A16,A18,Th60;
suppose A19:y <> -infty;
-infty <=' y by SUPINF_1:21;
then A20: -infty <' y by A19,SUPINF_1:22;
then A21: -infty <' |.y.| by A2,SUPINF_1:29;
A22: x + y <=' |.x.| + |.y.| by A1,A2,A13,A20,SUPINF_2:14;
-|.y.| <> +infty by A21,SUPINF_2:4,17;
then A23: -|.x.|+(-|.y.|) <=' x + y by A1,A2,A12,SUPINF_1:14,SUPINF_2:14;
-|.x.|+(-|.y.|) = -(|.x.|+|.y.|) by A2,A12,A20,Th14,SUPINF_1:14,SUPINF_2
:4;
hence thesis by A22,A23,Th60;
end;
hence thesis;
suppose A24:x <> +infty & x <> -infty;
then -x <> +infty & -x <> -infty by EXTREAL1:4;
then A25:|.x.| <> +infty & |.x.| <> -infty by A24,Th50;
then A26: x + y <=' |.x.| + |.y.| by A2,A24,SUPINF_2:14;
-|.x.| <> +infty & -|.x.| <> -infty by A25,EXTREAL1:4;
then A27:-|.x.|+(-|.y.|) <=' x + y by A2,A24,SUPINF_2:14;
-|.x.|+(-|.y.|) = -(|.x.|+|.y.|) by A25,Th14;
hence thesis by A26,A27,Th60;
end;
theorem Th62: :: extension of ABSVALUE:14
-infty <' x & x <' +infty & x <> 0. implies |.x.|*|. 1./x .| = 1.
proof
assume that A1:-infty <' x and A2:x <' +infty and A3:x <> 0.;
reconsider a = x as Real by A1,A2,EXTREAL1:1;
A4:1./x = 1/a by A3,EXTREAL1:32,MESFUNC1:def 8;
per cases;
suppose A5:0. <=' x;
then A6: |.x.| = a by EXTREAL1:def 3;
0. <' x by A3,A5,SUPINF_1:22;
then A7: 0 < a by EXTREAL1:18;
then 0 < 1/a by REAL_2:127;
then 0. <' 1./x by A4,EXTREAL1:18;
then |. 1./x .| = 1/a by A4,EXTREAL1:36;
then |.x.|*|. 1./x .| = a * (1/a) by A6,EXTREAL1:13;
hence thesis by A7,MESFUNC1:def 8,XCMPLX_1:107;
suppose A8:not 0. <=' x;
then A9:|.x.| = -x by EXTREAL1:def 3 .= -a by SUPINF_2:3;
A10:a < 0 by A8,EXTREAL1:19;
then 1/a < 0 by REAL_2:149;
then 1./x <' 0. by A4,EXTREAL1:19;
then |. 1./x .| = -(1./x) by EXTREAL1:37 .= -(1/a) by A4,SUPINF_2:3;
then |.x.|*|. 1./x .| = (-a) * (-(1/a)) by A9,EXTREAL1:13
.= a * (1/a) by XCMPLX_1:177;
hence thesis by A10,MESFUNC1:def 8,XCMPLX_1:107;
end;
theorem
x = +infty or x = -infty implies |.x.|*|. 1./x .| = 0.
proof
assume A1:x = +infty or x = -infty;
-infty <' 1. & 1. <' +infty by MESFUNC1:def 8,SUPINF_1:31;
then 1./x = 0. by A1,EXTREAL1:33;
then |. 1./x .| = 0. by EXTREAL1:def 3;
hence thesis by EXTREAL1:22;
end;
theorem :: extension of ABSVALUE:15
x <> 0. implies |. 1./x .| = 1./|.x.|
proof
assume A1:x <> 0.;
A2:-infty <' 1. & 1. <' +infty by MESFUNC1:def 8,SUPINF_1:31;
per cases;
suppose A3:x = +infty;
then 1./x = 0. by A2,EXTREAL1:33;
then A4: |. 1./x .| = 0. by EXTREAL1:def 3;
|.x.| = +infty by A3,EXTREAL1:36,SUPINF_2:19;
hence thesis by A2,A4,EXTREAL1:33;
suppose A5:x = -infty;
then 1./x = 0. by A2,EXTREAL1:33;
then A6: |. 1./x .| = 0. by EXTREAL1:def 3;
|.x.| = +infty by A5,EXTREAL1:37,SUPINF_2:4,19;
hence thesis by A2,A6,EXTREAL1:33;
suppose A7:x <> +infty & x <> -infty;
-infty <=' x & x <=' +infty by SUPINF_1:20,21;
then A8: -infty <' x & x <' +infty by A7,SUPINF_1:22;
then A9: |. 1./x .|*|.x.| = 1. by A1,Th62;
-(+infty) <' x & 0. <' |.x.| by A1,A8,Th52,SUPINF_2:def 3;
then |.x.| <> 0. & -infty <' |.x.| & |.x.| <' +infty
by A8,Th59,SUPINF_1:29,SUPINF_2:19;
hence thesis by A9,Th19;
end;
theorem :: extension of ABSVALUE:16
not((x=-infty or x=+infty) & (y=-infty or y=+infty)) & y<>0. implies
|.x/y.| = |.x.|/|.y.|
proof
assume that A1:not((x=-infty or x=+infty) & (y=-infty or y=+infty))
and A2:y<>0.;
per cases;
suppose A3:x = +infty;
then y is Real by A1,EXTREAL1:1;
then A4: -infty <' y & y <' +infty by SUPINF_1:31;
A5: |.x.| = +infty by A3,EXTREAL1:36,SUPINF_2:19;
now per cases by A2,SUPINF_1:22;
suppose A6:0. <' y;
then A7: |.y.| = y by EXTREAL1:36;
x / y = +infty by A3,A4,A6,Th17;
then |.x/y.| = +infty by EXTREAL1:36,SUPINF_2:19;
hence thesis by A4,A5,A6,A7,Th17;
suppose A8:y <' 0.;
then |.y.| = -y by EXTREAL1:37;
then A9: |.y.| <' +infty by A4,SUPINF_2:4,17;
A10: 0. <' |.y.| by A2,Th52;
x / y = -infty by A3,A4,A8,Th18;
then |.x/y.| = +infty by EXTREAL1:37,SUPINF_2:4,19;
hence thesis by A5,A9,A10,Th17;
end;
hence thesis;
suppose A11:x = -infty;
then y is Real by A1,EXTREAL1:1;
then A12:-infty <' y & y <' +infty by SUPINF_1:31;
A13:|.x.| = +infty by A11,EXTREAL1:37,SUPINF_2:4,19;
now per cases by A2,SUPINF_1:22;
suppose A14:0. <' y;
then A15: |.y.| = y by EXTREAL1:36;
x / y = -infty by A11,A12,A14,Th18;
then |.x/y.| = +infty by EXTREAL1:37,SUPINF_2:4,19;
hence thesis by A12,A13,A14,A15,Th17;
suppose A16:y <' 0.;
then |.y.| = -y by EXTREAL1:37;
then A17: |.y.| <' +infty by A12,SUPINF_2:4,17;
A18: 0. <' |.y.| by A2,Th52;
x / y = +infty by A11,A12,A16,Th17;
then |.x/y.| = +infty by EXTREAL1:36,SUPINF_2:19;
hence thesis by A13,A17,A18,Th17;
end;
hence thesis;
suppose A19:x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
x is Real by A19,EXTREAL1:1;
then -infty <' x & x <' +infty by SUPINF_1:31;
then -(+infty) <' x & x <' +infty by EXTREAL1:4;
then A20:|.x.| <' +infty by Th59;
A21: -infty <' 0. & 0. <=' |.x.| by Th51,SUPINF_2:19;
now per cases;
suppose A22:y = +infty;
then x / y = 0. by A19,EXTREAL1:33;
then A23: |.x/y.| = 0. by EXTREAL1:def 3;
|.y.| = +infty by A22,EXTREAL1:36,SUPINF_2:19;
hence thesis by A20,A21,A23,EXTREAL1:33;
suppose A24:y = -infty;
then x / y = 0. by A19,EXTREAL1:33;
then A25: |.x/y.| = 0. by EXTREAL1:def 3;
|.y.| = +infty by A24,EXTREAL1:37,SUPINF_2:4,19;
hence thesis by A20,A21,A25,EXTREAL1:33;
suppose y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
x / y = a / b by A2,EXTREAL1:32;
then A26: |.x/y.| = abs(a/b) by Th49;
A27: 0. <> |.y.| by A2,Th52;
|.x.| = abs(a) & |.y.| = abs b by Th49;
then |.x.|/|.y.| = abs(a)/abs(b) by A27,EXTREAL1:32;
hence thesis by A26,ABSVALUE:16;
end;
hence thesis;
end;
theorem Th66: :: extension of ABSVALUE:17
|.x.| = |.-x.|
proof
per cases by SUPINF_1:22;
suppose A1:0. <' x;
then -x <' 0. by EXTREAL1:25;
then |.-x.| = -(-x) by EXTREAL1:37 .= x;
hence thesis by A1,EXTREAL1:36;
suppose A2:x <' 0.;
then A3: |.x.| = -x by EXTREAL1:37;
0. <' -x by A2,EXTREAL1:25;
hence thesis by A3,EXTREAL1:36;
suppose x = 0.;
hence thesis by EXTREAL1:24;
end;
theorem Th67:
x = +infty or x = -infty implies |.x.| = +infty
proof
assume A1:x = +infty or x = -infty;
per cases by A1;
suppose x = +infty;
hence thesis by EXTREAL1:36,SUPINF_2:19;
suppose A2:x = -infty;
then -x = +infty by EXTREAL1:4;
hence thesis by A2,EXTREAL1:37,SUPINF_2:19;
end;
theorem Th68: :: extension of ABSVALUE:18
x is Real or y is Real implies |.x.|-|.y.| <=' |.x-y.|
proof
assume A1:x is Real or y is Real;
per cases by A1;
suppose A2:y is Real;
then A3: y <> +infty & y <> -infty by SUPINF_1:31;
reconsider b = y as Real by A2;
|.y.| = abs b by Th49;
then A4: |.y.| <> +infty & |.y.| <> -infty by SUPINF_1:31;
(x - y) + y = x by A2,MEASURE6:8;
then |.x.| <=' |.x-y.| + |.y.| by A3,Th61;
hence thesis by A4,Th34;
suppose x is Real;
then reconsider a = x as Real;
A5: |.x.| = abs a by Th49;
then A6: |.x.| <> +infty & |.x.| <> -infty by SUPINF_1:31;
now per cases;
suppose y = +infty or y = -infty;
then |.y.| = +infty by Th67;
then |.x.|-|.y.| <' 0. & 0. <=' |.x-y.| by A6,Th51,SUPINF_2:6,19;
hence thesis by SUPINF_1:29;
suppose y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
x - y = a - b by SUPINF_2:5;
then A7: |.y.| = abs b & |.x-y.| = abs(a-b) by Th49;
then A8: |.x.|-|.y.| = abs(a)-abs(b) by A5,SUPINF_2:5;
abs(a)-abs(b) <= abs(a-b) by ABSVALUE:18;
hence thesis by A7,A8,SUPINF_1:def 7;
end;
hence thesis;
end;
theorem :: extension of ABSVALUE:19
not((x = +infty & y = +infty) or (x = -infty & y = -infty)) implies
|.x-y.| <=' |.x.| + |.y.|
proof
assume A1:not((x = +infty & y = +infty) or (x = -infty & y = -infty));
per cases;
suppose A2:x = +infty;
then x - y = +infty by A1,SUPINF_2:6;
then A3: |.x-y.| = +infty & |.x.| = +infty by A2,Th67;
-infty <' 0. & 0. <=' |.y.| by Th51,SUPINF_2:19;
hence thesis by A3,SUPINF_2:def 2;
suppose A4:x = -infty;
then x - y = -infty by A1,SUPINF_2:7;
then A5: |.x-y.| = +infty & |.x.| = +infty by A4,Th67;
-infty <' 0. & 0. <=' |.y.| by Th51,SUPINF_2:19;
hence thesis by A5,SUPINF_2:def 2;
suppose A6:x <> +infty & x <> -infty;
then reconsider a = x as Real by EXTREAL1:1;
now per cases;
suppose A7:y = +infty;
then x - y = -infty by A6,SUPINF_2:6;
then A8: |.x-y.| = +infty & |.y.| = +infty by A7,Th67;
-infty <' 0. & 0. <=' |.x.| by Th51,SUPINF_2:19;
hence thesis by A8,SUPINF_2:def 2;
suppose A9:y = -infty;
then x - y = +infty by A6,SUPINF_2:7;
then A10: |.x-y.| = +infty & |.y.| = +infty by A9,Th67;
-infty <' 0. & 0. <=' |.x.| by Th51,SUPINF_2:19;
hence thesis by A10,SUPINF_2:def 2;
suppose y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
x - y = a - b by SUPINF_2:5;
then A11: |.x-y.| = abs(a-b) & |.x.|=abs a & |.y.|=abs b by Th49;
then A12: |.x.|+|.y.|=abs(a)+abs(b) by SUPINF_2:1;
abs(a-b) <= abs(a)+abs(b) by ABSVALUE:19;
hence thesis by A11,A12,SUPINF_1:def 7;
end;
hence thesis;
end;
theorem :: extension of ABSVALUE:20
|.|.x.|.| = |.x.|
proof
0. <=' |.x.| by Th51;
hence thesis by EXTREAL1:def 3;
end;
theorem :: extension of ABSVALUE:21
not((x = +infty & y = -infty) or (x = -infty & y = +infty)) &
|.x.| <=' z & |.y.| <=' w implies |.x+y.| <=' z + w
proof
assume that A1:not((x=+infty & y=-infty) or (x=-infty & y=+infty)) and
A2:|.x.| <=' z and A3:|.y.| <=' w;
0. <=' |.x.| & 0. <=' |.y.| by Th51;
then A4: 0. <=' z & 0. <=' w & -infty <' 0. by A2,A3,SUPINF_1:29,SUPINF_2:19
;
then -infty <' z & -infty <' w by SUPINF_1:29;
then -z <' -(-infty) & -w <' -(-infty) by SUPINF_2:17;
then A5:-z <' +infty & -w <' +infty by EXTREAL1:4;
A6:-z <=' x & x <=' z & -w <=' y & y <=' w by A2,A3,Th60;
then A7:x + y <=' z + w by A1,A4,SUPINF_2:14;
A8:-z + -w <=' x + y by A1,A5,A6,SUPINF_2:14;
-z + -w = -(z + w) by A4,Th14;
hence thesis by A7,A8,Th60;
end;
theorem :: extension of ABSVALUE:22
x is Real or y is Real implies |.|.x.|-|.y.|.| <=' |.x-y.|
proof
assume A1:x is Real or y is Real;
then A2:(-infty <' x & x <' +infty) or (-infty <' y & y <' +infty) by SUPINF_1:
31;
A3:|.x.|-|.y.| <=' |.x-y.| by A1,Th68;
A4:|.y.|-|.x.| <=' |.y-x.| by A1,Th68;
y - x = -(x - y) by A2,Th15;
then A5:|.y-x.| = |.x-y.| by Th66;
(-infty<'|.x.| & |.x.|<'+infty) or (-infty<'|.y.| & |.y.|<'+infty)
proof
per cases by A1;
suppose x is Real;
then reconsider a = x as Real;
|.x.| = abs a by Th49;
hence thesis by SUPINF_1:31;
suppose y is Real;
then reconsider b = y as Real;
|.y.| = abs b by Th49;
hence thesis by SUPINF_1:31;
end;
then |.y.|-|.x.| = -(|.x.|-|.y.|) by Th15;
then -|.x-y.| <=' -(-(|.x.|-|.y.|)) by A4,A5,SUPINF_2:16;
hence thesis by A3,Th60;
end;
theorem :: extension of ABSVALUE:24
0. <=' x * y implies |.x+y.| = |.x.|+|.y.|
proof
assume A1:0. <=' x * y;
per cases by A1,Th44;
suppose A2: (0. <=' x or 0. <' x) & (0. <=' y or 0. <' y);
then A3: |.x.| = x & |.y.| = y by EXTREAL1:def 3;
0. <=' x + y by A2,Th7;
hence thesis by A3,EXTREAL1:def 3;
suppose A4:(x <=' 0. or x <' 0.) & (y <=' 0. or y <' 0.);
then A5: |.x.| = -x & |.y.| = -y by Th55;
x + y <=' 0. by A4,Th9;
then |.x+y.| = -(x + y) by Th55 .= -x + (-y) by A4,Th14,SUPINF_2:19;
hence thesis by A5;
end;
begin
:: Definitions of MIN,MAX for extended real numbers and their basic properties
theorem Th74:
x = a & y = b implies (b < a iff y <' x) & (b <= a iff y <=' x)
proof
assume A1:x = a & y = b;
R_EAL a = a & R_EAL b = b by MEASURE6:def 1;
hence thesis by A1,MEASURE6:14;
end;
definition let x,y;
func min(x,y) -> R_eal equals
:Def1: x if x <=' y otherwise y;
correctness;
func max(x,y) -> R_eal equals
:Def2: x if y <=' x otherwise y;
correctness;
end;
theorem Th75:
x = -infty or y = -infty implies min(x,y) = -infty
proof
assume A1:x = -infty or y = -infty;
per cases by A1;
suppose A2:x = -infty;
then x <=' y by SUPINF_1:21;
hence thesis by A2,Def1;
suppose A3:y = -infty;
then A4: y <=' x by SUPINF_1:21;
now per cases by A4,SUPINF_1:22;
suppose x = y;
hence thesis by A3,Def1;
suppose y <' x;
hence thesis by A3,Def1;
end;
hence thesis;
end;
theorem Th76:
x = +infty or y = +infty implies max(x,y) = +infty
proof
assume A1:x = +infty or y = +infty;
per cases by A1;
suppose A2:x = +infty;
then y <=' x by SUPINF_1:20;
hence thesis by A2,Def2;
suppose A3:y = +infty;
then A4: x <=' y by SUPINF_1:20;
now per cases by A4,SUPINF_1:22;
suppose x = y;
hence thesis by A3,Def2;
suppose x <' y;
hence thesis by A3,Def2;
end;
hence thesis;
end;
theorem Th77:
for x,y being R_eal holds
for a,b being Real holds
(x = a & y = b) implies min(x,y) = min(a,b) & max(x,y) = max(a,b)
proof
let x,y being R_eal;
let a,b being Real;
assume A1:x = a & y = b;
A2:min(x,y) = min(a,b)
proof
per cases;
suppose A3:x <=' y;
then a <= b by A1,Th74;
then min(x,y) = x & min(a,b) = a by A3,Def1,SQUARE_1:def 1;
hence thesis by A1;
suppose A4:not (x <=' y);
then b < a by A1,Th74;
then min(x,y) = y & min(a,b) = b by A4,Def1,SQUARE_1:def 1;
hence thesis by A1;
end;
max(x,y) = max(a,b)
proof
per cases;
suppose A5:y <=' x;
then b <= a by A1,Th74;
then max(x,y) = x & max(a,b) = a by A5,Def2,SQUARE_1:def 2;
hence thesis by A1;
suppose A6:not (y <=' x);
then a < b by A1,Th74;
then max(x,y) = y & max(a,b) = b by A6,Def2,SQUARE_1:def 2;
hence thesis by A1;
end;
hence thesis by A2;
end;
theorem Th78: :: extension of SQUARE_1:32
y <=' x implies min(x,y) = y
proof
assume A1:y <=' x;
per cases by A1,SUPINF_1:22;
suppose y <' x;
hence thesis by Def1;
suppose y = x;
hence thesis by Def1;
end;
theorem :: extension of SQUARE_1:33
not y <=' x implies min(x,y) = x by Def1;
theorem :: extension of SQUARE_1:34
x <> +infty & y <> +infty &
not ((x = +infty & y = +infty) or (x = -infty & y = -infty))
implies min(x,y) = (x + y - |.x - y.|) / R_EAL 2
proof
assume that A1:x <> +infty & y <> +infty and
A2:not ((x = +infty & y = +infty) or (x = -infty & y = -infty));
per cases;
suppose A3:x = -infty;
then A4: min(x,y) = -infty by Th75;
A5: x + y = -infty by A1,A3,SUPINF_2:def 2;
x - y = -infty by A2,A3,SUPINF_2:7;
then |.x - y.| = +infty by Th67;
then A6: x + y - |.x - y.| = -infty by A5,SUPINF_1:14,SUPINF_2:7;
0 < 2 & R_EAL 2 = 2 by MEASURE6:def 1;
then 0. <' R_EAL 2 & R_EAL 2 <' +infty by EXTREAL1:18,SUPINF_1:31;
hence thesis by A4,A6,Th18;
suppose x <> -infty;
then reconsider a = x as Real by A1,EXTREAL1:1;
now per cases;
suppose A7:y = -infty;
then A8: min(x,y) = -infty by Th75;
A9: x + y = -infty by A1,A7,SUPINF_2:def 2;
x - y = +infty by A2,A7,SUPINF_2:7;
then |.x - y.| = +infty by Th67;
then A10: x + y - |.x - y.| = -infty by A9,SUPINF_1:14,SUPINF_2:7;
0 < 2 & R_EAL 2 = 2 by MEASURE6:def 1;
then 0. <' R_EAL 2 & R_EAL 2 <' +infty by EXTREAL1:18,SUPINF_1:31;
hence thesis by A8,A10,Th18;
suppose y <> -infty;
then reconsider b = y as Real by A1,EXTREAL1:1;
A11: min(x,y)=min(a,b) by Th77;
A12: x + y = a + b by SUPINF_2:1;
x - y = a - b by SUPINF_2:5;
then |.x - y.| = abs(a - b) by Th49;
then A13: x + y - |.x - y.| = a + b - abs(a - b) by A12,SUPINF_2:5;
A14: 0 < 2 & R_EAL 2 = 2 by MEASURE6:def 1;
then 0. <' R_EAL 2 by EXTREAL1:18;
then (x + y - |.x - y.|) / R_EAL 2 = (a+b-abs(a-b))/2
by A13,A14,EXTREAL1:32;
hence thesis by A11,SQUARE_1:34;
end;
hence thesis;
end;
theorem Th81: :: extension of SQUARE_1:35
min(x,y) <=' x & min(y,x) <=' x
proof
per cases;
suppose x = -infty;
hence thesis by Th75;
suppose x = +infty;
hence thesis by SUPINF_1:20;
suppose x <> -infty & x <> +infty;
then reconsider a = x as Real by EXTREAL1:1;
now per cases;
suppose y = -infty;
then min(x,y) = -infty & min(y,x) = -infty by Th75;
hence thesis by SUPINF_1:21;
suppose y = +infty;
then x <=' y by SUPINF_1:20;
hence thesis by Def1,Th78;
suppose y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
A1: min(x,y) = min(a,b) & min(y,x) = min(b,a) by Th77;
min(a,b) <= a & min(b,a) <= a by SQUARE_1:35;
hence thesis by A1,Th74;
end;
hence thesis;
end;
canceled;
theorem Th83: :: extension of SQUARE_1:37
min(x,y) = min(y,x)
proof
per cases;
suppose x <=' y;
then min(x,y) = x & min(y,x) = x by Def1,Th78;
hence thesis;
suppose not x <=' y;
then min(x,y) = y & min(y,x) = y by Def1;
hence thesis;
end;
theorem Th84: :: extension of SQUARE_1:38
min(x,y) = x or min(x,y) = y
proof
per cases;
suppose x <=' y;
hence thesis by Def1;
suppose not x <=' y;
hence thesis by Def1;
end;
theorem Th85: :: extension of SQUARE_1:39
x <=' y & x <=' z iff x <=' min(y,z)
proof
x <=' min(y,z) implies x <=' y & x <=' z
proof
assume A1:x <=' min(y,z);
min(y,z) <=' y & min(y,z) <=' z by Th81;
hence thesis by A1,SUPINF_1:29;
end;
hence thesis by Th84;
end;
canceled;
theorem
min(x,y) = y implies y <=' x by Def1;
theorem :: extension of SQUARE_1:40
min(x,min(y,z)) = min(min(x,y),z)
proof
per cases by Th84;
suppose A1:min(x,min(y,z)) = x;
then x <=' min(y,z) by Def1;
then A2: x <=' y & x <=' z by Th85;
then min(x,y) = x by Def1;
hence thesis by A1,A2,Def1;
suppose A3:min(x,min(y,z)) = min(y,z);
now per cases by Th84;
suppose min(y,z) = y;
hence thesis by A3;
suppose A4:min(y,z) = z;
then z <=' x & z <=' y by A3,Def1;
then z <=' min(x,y) by Th85;
hence thesis by A3,A4,Th78;
end;
hence thesis;
end;
theorem Th89: :: extension of SQUARE_1:43
x <=' y implies max(x,y) = y
proof
assume A1:x <=' y;
per cases by A1,SUPINF_1:22;
suppose x <' y;
hence thesis by Def2;
suppose x = y;
hence thesis by Def2;
end;
theorem :: extension of SQUARE_1:44
not x <=' y implies max(x,y) = x by Def2;
theorem :: extension of SQUARE_1:45
x <> -infty & y <> -infty &
not ((x = +infty & y = +infty) or (x = -infty & y = -infty))
implies max(x,y) = (x + y + |.x - y.|) / R_EAL 2
proof
assume that A1:x <> -infty & y <> -infty and
A2:not ((x = +infty & y = +infty) or (x = -infty & y = -infty));
per cases;
suppose A3:x = +infty;
then A4: max(x,y) = +infty by Th76;
A5: x + y = +infty by A1,A3,SUPINF_2:def 2;
x - y = +infty by A2,A3,SUPINF_2:6;
then |.x - y.| = +infty by Th67;
then A6: x + y + |.x - y.| = +infty by A5,SUPINF_1:14,SUPINF_2:def 2;
0 < 2 & R_EAL 2 = 2 by MEASURE6:def 1;
then 0. <' R_EAL 2 & R_EAL 2 <' +infty by EXTREAL1:18,SUPINF_1:31;
hence thesis by A4,A6,Th17;
suppose x <> +infty;
then reconsider a = x as Real by A1,EXTREAL1:1;
now per cases;
suppose A7:y = +infty;
then A8: max(x,y) = +infty by Th76;
A9: x + y = +infty by A1,A7,SUPINF_2:def 2;
x - y = -infty by A2,A7,SUPINF_2:6;
then |.x - y.| = +infty by Th67;
then A10: x + y + |.x - y.| = +infty by A9,SUPINF_1:14,SUPINF_2:def 2;
0 < 2 & R_EAL 2 = 2 by MEASURE6:def 1;
then 0. <' R_EAL 2 & R_EAL 2 <' +infty by EXTREAL1:18,SUPINF_1:31;
hence thesis by A8,A10,Th17;
suppose y <> +infty;
then reconsider b = y as Real by A1,EXTREAL1:1;
A11: max(x,y)=max(a,b) by Th77;
A12: x + y = a + b by SUPINF_2:1;
x - y = a - b by SUPINF_2:5;
then |.x - y.| = abs(a - b) by Th49;
then A13: x + y + |.x - y.| = a + b + abs(a - b) by A12,SUPINF_2:1;
A14: 0 < 2 & R_EAL 2 = 2 by MEASURE6:def 1;
then 0. <' R_EAL 2 by EXTREAL1:18;
then (x + y + |.x - y.|) / R_EAL 2 = (a+b+abs(a-b))/2
by A13,A14,EXTREAL1:32;
hence thesis by A11,SQUARE_1:45;
end;
hence thesis;
end;
theorem Th92: :: extension of SQUARE_1:46
x <=' max(x,y) & x <=' max(y,x)
proof
per cases;
suppose x = +infty;
hence thesis by Th76;
suppose x = -infty;
hence thesis by SUPINF_1:21;
suppose x <> -infty & x <> +infty;
then reconsider a = x as Real by EXTREAL1:1;
now per cases;
suppose y = +infty;
then max(x,y) = +infty & max(y,x) = +infty by Th76;
hence thesis by SUPINF_1:20;
suppose y = -infty;
then y <=' x by SUPINF_1:21;
hence thesis by Def2,Th89;
suppose y <> +infty & y <> -infty;
then reconsider b = y as Real by EXTREAL1:1;
A1: max(x,y) = max(a,b) & max(y,x) = max(b,a) by Th77;
a <= max(a,b) & a <= max(b,a) by SQUARE_1:46;
hence thesis by A1,Th74;
end;
hence thesis;
end;
canceled;
theorem Th94: :: extension of SQUARE_1:48
max(x,y) = max(y,x)
proof
per cases;
suppose y <=' x;
then max(x,y) = x & max(y,x) = x by Def2,Th89;
hence thesis;
suppose not y <=' x;
then max(x,y) = y & max(y,x) = y by Def2;
hence thesis;
end;
theorem Th95: :: extension of SQUARE_1:49
max(x,y) = x or max(x,y) = y
proof
per cases;
suppose y <=' x;
hence thesis by Def2;
suppose not y <=' x;
hence thesis by Def2;
end;
theorem Th96: :: extension of SQUARE_1:50
y <=' x & z <=' x iff max(y,z) <=' x
proof
A1:y <=' x & z <=' x implies max(y,z) <=' x
proof
assume A2:y <=' x & z <=' x;
now per cases by Th95;
suppose max(y,z) = y;
hence thesis by A2;
suppose max(y,z) = z;
hence thesis by A2;
end;
hence thesis;
end;
max(y,z) <=' x implies y <=' x & z <=' x
proof
assume A3:max(y,z) <=' x;
y <=' max(y,z) & z <=' max(y,z) by Th92;
hence thesis by A3,SUPINF_1:29;
end;
hence thesis by A1;
end;
canceled;
theorem
max(x,y) = y implies x <=' y by Def2;
theorem :: extension of SQUARE_1:51
max(x,max(y,z)) = max(max(x,y),z)
proof
per cases by Th95;
suppose A1:max(x,max(y,z)) = x;
then max(y,z) <=' x by Def2;
then A2: y <=' x & z <=' x by Th96;
then max(x,y) = x by Def2;
hence thesis by A1,A2,Def2;
suppose A3:max(x,max(y,z)) = max(y,z);
now per cases by Th95;
suppose max(y,z) = y;
hence thesis by A3;
suppose A4:max(y,z) = z;
then x <=' z & y <=' z by A3,Def2;
then max(x,y) <=' z by Th96;
hence thesis by A3,A4,Th89;
end;
hence thesis;
end;
theorem :: extension of SQUARE_1:53
min(x,y) + max(x,y) = x + y
proof
per cases;
suppose x <=' y;
then min(x,y) = x & max(x,y) = y by Def1,Th89;
hence thesis;
suppose not (x <=' y);
then min(x,y) = y & max(x,y) = x by Def1,Def2;
hence thesis;
end;
theorem Th101: :: extension of SQUARE_1:54
max(x,min(x,y)) = x & max(min(x,y),x) = x &
max(min(y,x),x) = x & max(x,min(y,x)) = x
proof
per cases by Th84;
suppose min(x,y) = x;
then max(x,min(x,y)) = x & max(min(x,y),x) = x by Def2;
hence thesis by Th83;
suppose A1:min(x,y) = y;
then y <=' x by Def1;
then max(x,min(x,y)) = x & max(min(x,y),x) = x by A1,Def2,Th89;
hence thesis by Th83;
end;
theorem Th102: :: extension of SQUARE_1:55
min(x,max(x,y)) = x & min(max(x,y),x) = x &
min(max(y,x),x) = x & min(x,max(y,x)) = x
proof
per cases by Th95;
suppose max(x,y) = x;
then min(x,max(x,y)) = x & min(max(x,y),x) = x by Def1;
hence thesis by Th94;
suppose A1:max(x,y) = y;
then x <=' y by Def2;
then min(x,max(x,y)) = x & min(max(x,y),x) = x by A1,Def1,Th78;
hence thesis by Th94;
end;
theorem :: extension of SQUARE_1:56
min(x,max(y,z)) = max(min(x,y),min(x,z)) &
min(max(y,z),x) = max(min(y,x),min(z,x))
proof
per cases by Th84;
suppose A1:min(x,max(y,z)) = x;
then A2: min(max(y,z),x) = x by Th83;
A3: x <=' max(y,z) by A1,Def1;
now per cases by A3,Th95;
suppose x <=' y;
then min(x,y) = x by Def1;
then A4: max(min(x,y),min(x,z)) = x by Th101;
then max(min(y,x),min(x,z)) = x by Th83;
hence thesis by A2,A4,Th83;
suppose x <=' z;
then min(x,z) = x by Def1;
then max(min(x,y),min(x,z)) = x & max(min(y,x),min(x,z)) = x by Th101;
hence thesis by A2,Th83;
end;
hence thesis;
suppose A5:min(x,max(y,z)) = max(y,z);
then max(y,z) <=' x by Def1;
then y <=' x & z <=' x by Th96;
then A6: min(y,x) = y & min(z,x) = z by Def1;
then min(x,y) = y & min(x,z) = z by Th83;
hence thesis by A5,A6,Th83;
end;
theorem :: extension of SQUARE_1:57
max(x,min(y,z)) = min(max(x,y),max(x,z)) &
max(min(y,z),x) = min(max(y,x),max(z,x))
proof
per cases by Th95;
suppose A1:max(x,min(y,z)) = x;
then A2: max(min(y,z),x) = x by Th94;
A3: min(y,z) <=' x by A1,Def2;
now per cases by A3,Th84;
suppose y <=' x;
then max(x,y) = x by Def2;
then A4: min(max(x,y),max(x,z)) = x by Th102;
then min(max(y,x),max(x,z)) = x by Th94;
hence thesis by A2,A4,Th94;
suppose z <=' x;
then max(x,z) = x by Def2;
then min(max(x,y),max(x,z)) = x & min(max(y,x),max(x,z)) = x by Th102;
hence thesis by A2,Th94;
end;
hence thesis;
suppose A5:max(x,min(y,z)) = min(y,z);
then x <=' min(y,z) by Def2;
then x <=' y & x <=' z by Th85;
then A6: max(y,x) = y & max(z,x) = z by Def2;
then max(x,y) = y & max(x,z) = z by Th94;
hence thesis by A5,A6,Th94;
end;