:: Basic Operations on Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received September 23, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XXREAL_0, ORDINAL1, XREAL_0, SUBSET_1, CARD_1, ARYTM_3,
XCMPLX_0, ARYTM_1, RELAT_1, NAT_1, REAL_1, INT_1;
notations ORDINAL1, SUBSET_1, XCMPLX_0, XXREAL_0, XREAL_0, NUMBERS, INT_1;
constructors XBOOLE_0, ORDINAL1, XXREAL_0, XCMPLX_0, XREAL_0, NUMBERS,
XXREAL_2, INT_1;
registrations XXREAL_0, XREAL_0, ORDINAL1, XCMPLX_0, NAT_1, INT_1;
requirements SUBSET, NUMERALS, ARITHM, REAL;
definitions XXREAL_0;
equalities XCMPLX_0, XXREAL_0;
theorems XXREAL_0, XREAL_0, XCMPLX_1, XREAL_1;
begin
reserve x,y,z,w for ExtReal,
r for Real;
definition
let x,y;
redefine pred x <= y means :: redefines <= (XXREAL_0, definition)
:Def1:
ex p,q being Element of REAL st p = x & q = y & p <= q
if x in REAL & y in REAL otherwise x = -infty or y = +infty;
consistency;
compatibility
proof
thus x in REAL & y in REAL implies (x <= y iff ex p,q being Element of
REAL st p = x & q = y & p <= q);
thus not(x in REAL & y in REAL) implies (x <= y iff x = -infty or y =
+infty)
proof
assume
A1: not(x in REAL & y in REAL);
per cases by A1;
suppose
A2: not x in REAL;
thus x <= y implies x = -infty or y = +infty
proof
assume
A3: x <= y;
assume x <> -infty;
then x = +infty by A2,XXREAL_0:14;
hence thesis by A3,XXREAL_0:4;
end;
thus thesis by XXREAL_0:3,5;
end;
suppose
A4: not y in REAL;
thus x <= y implies x = -infty or y = +infty
proof
assume
A5: x <= y;
assume
A6: x <> -infty;
assume y <> +infty;
then y = -infty by A4,XXREAL_0:14;
hence thesis by A5,A6,XXREAL_0:6;
end;
thus thesis by XXREAL_0:3,5;
end;
end;
end;
end;
registration
cluster non real positive for ExtReal;
existence
proof
take +infty;
thus thesis;
end;
cluster non real negative for ExtReal;
existence
proof
take -infty;
thus thesis;
end;
end;
theorem Th1:
for x being non real positive ExtReal holds x = +infty
proof
let x be non real positive ExtReal;
not x in REAL;
hence thesis by XXREAL_0:14;
end;
theorem Th2:
for x being non real negative ExtReal holds x = -infty
proof
let x be non real negative ExtReal;
not x in REAL;
hence thesis by XXREAL_0:14;
end;
registration
cluster non real non negative -> positive for ExtReal;
coherence;
cluster non real non positive -> negative for ExtReal;
coherence;
end;
theorem Th3:
x < z implies ex y being Real st x < y & y < z
proof
assume
A1: x < z;
per cases by XXREAL_0:14;
suppose x in REAL & z in REAL;
hence thesis by A1,XREAL_1:5;
end;
suppose x = +infty or z = -infty;
hence thesis by A1,XXREAL_0:4,6;
end;
suppose
A2: z = +infty;
per cases by A1,A2,XXREAL_0:14;
suppose x = -infty;
hence thesis by A2;
end;
suppose x in REAL;
then reconsider x1 = x as Real;
take x1+1;
A3: x1+1 in REAL by XREAL_0:def 1;
x1+0 < x1+1 by XREAL_1:8;
hence thesis by A2,A3,XXREAL_0:9;
end;
end;
suppose
A4: x = -infty;
per cases by A1,A4,XXREAL_0:14;
suppose z = +infty;
hence thesis by A4;
end;
suppose z in REAL;
then reconsider z1 = z as Real;
take z1-1;
A5: z1-1 in REAL by XREAL_0:def 1;
z1-1 < z1-0 by XREAL_1:10;
hence thesis by A4,A5,XXREAL_0:12;
end;
end;
end;
begin :: addition
definition
let x,y be ExtReal;
func x + y -> ExtReal means
:Def2:
ex a,b being Complex st x = a & y = b & it = a + b
if x is real & y is real,
it = +infty if x = +infty & y <> -infty or y = +infty & x <> -infty,
it = -infty if x = -infty & y <> +infty or y = -infty & x <> +infty
otherwise it = 0;
existence
proof
thus x is real & y is real implies ex c being ExtReal, a, b being
Complex st x = a & y = b & c = a + b
proof
assume x is real & y is real;
then reconsider a = x, b = y as Real;
take a+b, a, b;
thus thesis;
end;
thus thesis;
end;
uniqueness;
consistency;
commutativity;
end;
definition
let x be ExtReal;
func -x -> ExtReal means
:Def3:
ex a being Complex st x = a & it = -a if x is real,
it = -infty if x = +infty otherwise it = +infty;
existence
proof
thus x is real implies ex c being ExtReal, a being Complex
st x = a & c = -a
proof
assume x is real;
then reconsider a = x as Real;
take -a, a;
thus thesis;
end;
thus thesis;
end;
uniqueness;
consistency;
involutiveness
proof
let y,x be ExtReal such that
A1: x is real implies ex a being Complex st x = a & y = - a and
A2: x = +infty implies y = -infty and
A3: x is not real & x <> +infty implies y = +infty;
thus y is real implies ex a being Complex st y = a & x = - a
proof
assume y is real;
then consider a being Complex such that
A4: x = a & y = - a by A1,A2,A3;
take -a;
thus thesis by A4;
end;
x in REAL implies x is real;
hence y = +infty implies x = -infty by A1,A2,XXREAL_0:14;
thus thesis by A1,A3;
end;
end;
definition
let x,y be ExtReal;
func x - y -> ExtReal equals
x + -y;
coherence;
end;
registration
let x,y be Real, a,b be Complex;
identify x+y with a+b when x = a, y = b;
compatibility by Def2;
end;
registration
let x be Real, a be Complex;
identify -x with -a when x = a;
compatibility by Def3;
end;
:: for ExtReals
registration
let r be Real;
cluster -r -> real;
coherence;
end;
:: for ExtReals
registration
let r,s be Real;
cluster r+s -> real;
coherence;
cluster r-s -> real;
coherence;
end;
registration
let x be Real, y be non real ExtReal;
cluster x+y -> non real for object;
coherence
proof
not y in REAL;
then
A1: y = -infty or y = +infty by XXREAL_0:14;
let z be object;
assume z = x+y;
hence thesis by A1,Def2;
end;
end;
registration
let x,y be non real positive ExtReal;
cluster x+y -> non real;
coherence
proof
x = +infty by Th1;
hence thesis by Def2;
end;
end;
registration
let x,y be non real negative ExtReal;
cluster x+y -> non real;
coherence
proof
x = -infty by Th2;
hence thesis by Def2;
end;
end;
registration
let x be non real negative ExtReal, y be non real positive
ExtReal;
cluster x+y -> zero;
coherence
proof
x = -infty & y = +infty by Th1,Th2;
hence thesis by Def2;
end;
end;
registration
let x,y be Real, a,b be Complex;
identify x-y with a-b when x = a, y = b;
compatibility;
end;
theorem Th4:
x + 0 = x
proof
per cases by XXREAL_0:14;
suppose
x in REAL;
then reconsider r=x as Real;
r + 0 = r;
hence thesis;
end;
suppose
x = -infty or x = +infty;
hence thesis by Def2;
end;
end;
theorem Th5:
--infty = +infty by Def3;
theorem Th6:
-+infty = -infty by Def3;
Lm1: +infty + +infty = +infty by Def2;
Lm2: -infty + -infty = -infty by Def2;
theorem Th7:
x + -x = 0
proof
per cases by XXREAL_0:14;
suppose
x = -infty;
hence thesis by Th5;
end;
suppose
x in REAL;
then reconsider x as Real;
reconsider y=-x as Real;
x + y = 0;
hence thesis;
end;
suppose
x = +infty;
hence thesis by Th6;
end;
end;
theorem
x+y = 0 implies x = -y
proof
assume
A1: x+y = 0;
per cases by XXREAL_0:14;
suppose
x in REAL;
then reconsider x as Real;
x+y is real by A1;
then reconsider y as Real;
x+y = 0 by A1;
then x = -y;
hence thesis;
end;
suppose
A2: x = -infty;
then y = +infty by A1,Def2;
hence thesis by A2,Def3;
end;
suppose
A3: x = +infty;
then y = -infty by A1,Def2;
hence thesis by A3,Def3;
end;
end;
Lm3: for x holds -x in REAL iff x in REAL
proof
let x;
hereby
assume -x in REAL;
then reconsider a = -x as Real;
-a in REAL by XREAL_0:def 1;
hence x in REAL;
end;
assume x in REAL;
then reconsider a = x as Real;
-a is real;
hence thesis by XREAL_0:def 1;
end;
Lm4: -(+infty + -infty) = --infty - +infty
proof
thus -(+infty + -infty) = +infty - +infty by Def3
.= --infty - +infty by Def3;
end;
Lm5: -+infty = -infty by Def3;
Lm6: x in REAL implies -(x + +infty) = -+infty + -x
proof
assume
A1: x in REAL;
then x + +infty = +infty by Def2;
hence thesis by A1,Def2,Th6;
end;
Lm7: x in REAL implies -(x + -infty) = --infty + -x
proof
assume
A1: x in REAL;
then x + -infty = -infty by Def2;
hence thesis by A1,Def2,Th5;
end;
theorem Th9:
-(x+y) = -x + -y
proof
per cases by XXREAL_0:14;
suppose
A1: x = +infty & y = +infty;
hence -(x + y) = -+infty by Def2
.= -x +- y by A1,Def2,Lm5;
end;
suppose
x = +infty & y = -infty;
hence thesis by Lm4;
end;
suppose
x = +infty & y in REAL;
hence thesis by Lm6;
end;
suppose
x = -infty & y = +infty;
hence thesis by Lm4;
end;
suppose
A2: x = -infty & y = -infty;
hence -(x + y) = --infty by Def2
.= -x +- y by A2,Def2,Th5;
end;
suppose
x = -infty & y in REAL;
hence thesis by Lm7;
end;
suppose
x in REAL & y = +infty;
hence thesis by Lm6;
end;
suppose
x in REAL & y = -infty;
hence thesis by Lm7;
end;
suppose
x in REAL & y in REAL;
then reconsider a=x, b=y as Real;
-(x + y) = -(a + b) .= -a + - b;
hence thesis;
end;
end;
reserve f,g for ExtReal;
theorem Th10: :: MEMBER_1:3
-f = -g implies f = g
proof
assume
A1: -f = -g;
per cases by XXREAL_0:14;
suppose
A2: f in REAL;
now
assume not g in REAL;
then g = +infty or g = -infty by XXREAL_0:14;
hence contradiction by A1,A2,Def3;
end;
then
A3: ex a being Complex st g = a & -g = -a by Def3;
ex a being Complex st f = a & -f = -a by A2,Def3;
hence thesis by A1,A3;
end;
suppose
f = +infty;
hence thesis by A1,Th5;
end;
suppose
f = -infty;
then - -g = -infty by A1;
hence thesis by A1;
end;
end;
Lm8: x + y = +infty implies x = +infty or y = +infty
proof
assume
A1: x + y = +infty;
assume ( not x = +infty)& not y = +infty;
then x in REAL & y in REAL or x in REAL & y = -infty or x = -infty & y in
REAL or x = -infty & y = -infty by XXREAL_0:14;
hence thesis by A1,Def2;
end;
Lm9: x + y = -infty implies (x = -infty or y = -infty)
proof
assume
A1: x + y = -infty;
assume ( not x = -infty)& not y = -infty;
then x in REAL & y in REAL or x in REAL & y = +infty or x = +infty & y in
REAL or x = +infty & y = +infty by XXREAL_0:14;
hence thesis by A1,Def2;
end;
theorem Th11: :: MEMBER_1:4
r+f = r+g implies f = g
proof
assume
A1: r+f = r+g;
per cases by XXREAL_0:14;
suppose
A2: f in REAL;
now
assume not g in REAL;
then g = +infty or g = -infty by XXREAL_0:14;
hence contradiction by A1,A2;
end;
then
A3: ex c, d being Complex st r = c & g = d & r+g = c+d by Def2;
ex a, b being Complex st r = a & f = b & r+f = a+ b by A2,Def2;
hence thesis by A1,A3;
end;
suppose
A4: f = +infty;
then r+f = +infty by Def2;
hence thesis by A1,A4,Lm8;
end;
suppose
A5: f = -infty;
then r+f = -infty by Def2;
hence thesis by A1,A5,Lm9;
end;
end;
theorem :: MEMBER_1:5
r-f = r-g implies f = g
proof
assume r-f = r-g;
then -f = -g by Th11;
hence thesis by Th10;
end;
theorem Th13:
x <> +infty implies +infty - x = +infty & x - +infty = -infty
proof
assume
A1: x <> +infty;
then -x <> -infty by Th5;
hence +infty - x = +infty by Def2;
- +infty = -infty by Def3;
hence thesis by A1,Def2;
end;
theorem Th14:
x <> -infty implies -infty - x = -infty & x - -infty = +infty
proof
assume
A1: x <> -infty;
now
assume -x = +infty;
then --x = -infty by Def3;
hence contradiction by A1;
end;
hence -infty - x = -infty by Def2;
thus thesis by A1,Def2,Th5;
end;
theorem Th15:
x - 0 = x
proof
per cases by XXREAL_0:14;
suppose
x in REAL;
then reconsider a = x as Real;
x - 0 = a - 0 .= x;
hence thesis;
end;
suppose
x = -infty;
hence thesis by Th14;
end;
suppose
x = +infty;
hence thesis by Th13;
end;
end;
theorem
x + y = +infty implies x = +infty or y = +infty by Lm8;
theorem
x + y = -infty implies (x = -infty or y = -infty) by Lm9;
theorem Th18:
x - y = +infty implies (x = +infty or y = -infty)
proof
assume
A1: x - y = +infty;
assume ( not x = +infty)& not y = -infty;
then x in REAL & y in REAL or x in REAL & y = +infty or x = -infty & y in
REAL or x = -infty & y = +infty by XXREAL_0:14;
hence thesis by A1,Th13,Th14;
end;
theorem Th19:
x - y = -infty implies (x = -infty or y = +infty)
proof
assume
A1: x - y = -infty;
assume ( not x = -infty)& not y = +infty;
then x in REAL & y in REAL or x in REAL & y = -infty or x = +infty & y in
REAL or x = +infty & y = -infty by XXREAL_0:14;
hence thesis by A1,Th13,Th14;
end;
theorem Th20:
not ( x = +infty & y = -infty or x = -infty & y = +infty ) & x +
y in REAL implies x in REAL & y in REAL
proof
assume
A1: ( not ( x = +infty & y = -infty or x = -infty & y = +infty ))& x + y
in REAL;
A2: x in REAL or x = -infty or x = +infty by XXREAL_0:14;
A3: y in REAL or y = -infty or y = +infty by XXREAL_0:14;
assume not (x in REAL & y in REAL);
hence thesis by A1,A2,A3;
end;
theorem Th21:
not ( x = +infty & y = +infty or x = -infty & y = -infty ) & x -
y in REAL implies x in REAL & y in REAL
proof
assume
A1: ( not ( x = +infty & y = +infty or x = -infty & y = -infty ))& x - y
in REAL;
A2: x in REAL or x = -infty or x = +infty by XXREAL_0:14;
A3: y in REAL or y = -infty or y = +infty by XXREAL_0:14;
assume not (x in REAL & y in REAL);
hence thesis by A1,A2,A3,Th13,Th14;
end;
theorem Th22:
x is real implies y - x + x = y & y + x - x = y
proof
assume
A1: x is real;
per cases by A1,XXREAL_0:14;
suppose
x in REAL & y in REAL;
then reconsider a = x, b = y as Real;
A2: (y + x) - x = b + a - a .= y;
y - x + x = (b - a) + a .= y;
hence thesis by A2;
end;
suppose
A3: x in REAL & y = -infty;
then y - x = -infty by Def2;
hence thesis by A3,Def2;
end;
suppose
A4: x in REAL & y = +infty;
then y - x = +infty by Def2;
hence thesis by A4,Def2;
end;
end;
theorem Th23:
(x = +infty iff -x = -infty) & (x = -infty iff -x = +infty)
proof
-x = +infty implies x = -infty
proof
assume -x = +infty;
then --x = -infty by Def3;
hence thesis;
end;
hence thesis by Th5;
end;
theorem
z is real implies x = x + z - z
proof
assume
A1: z is real;
per cases by XXREAL_0:14;
suppose
A2: x = +infty;
then x + z = +infty by A1,Def2;
hence thesis by A1,A2,Th13;
end;
suppose
A3: x = -infty;
then x + z = -infty by A1,Def2;
hence thesis by A1,A3,Th14;
end;
suppose
x is Element of REAL;
then reconsider a = x, c = z as Real by A1;
x + z - z = a + c - c;
hence thesis;
end;
end;
Lm10: -+infty = -infty by Def3;
Lm11: x in REAL implies -(x + -infty) = --infty + -x
proof
A1: --infty = +infty by Th23;
assume
A2: x in REAL;
then x + -infty = -infty by Def2;
hence thesis by A2,A1,Def2;
end;
theorem Th25:
-(x + y) = -y - x
proof
per cases by XXREAL_0:14;
suppose
A1: x = +infty & y = +infty;
hence -(x + y) = -+infty by Def2
.= -y - x by A1,Def2,Lm10;
end;
suppose
x = +infty & y = -infty;
hence thesis by Lm4;
end;
suppose
x = +infty & y in REAL;
hence thesis by Lm6;
end;
suppose
x = -infty & y = +infty;
hence thesis by Lm4;
end;
suppose
A2: x = -infty & y = -infty;
hence -(x + y) = --infty by Def2
.= -y - x by A2,Def2,Th5;
end;
suppose
x = -infty & y in REAL;
hence thesis by Lm11;
end;
suppose
x in REAL & y = +infty;
hence thesis by Lm6;
end;
suppose
x in REAL & y = -infty;
hence thesis by Lm11;
end;
suppose
x in REAL & y in REAL;
then reconsider a=x, b=y as Real;
-(x + y) = -(a + b) .= -a + - b;
hence thesis;
end;
end;
theorem
-(x - y) = -x + y & -(x - y) = y - x
proof
-(x - y) = -(-y) - x by Th25;
hence thesis;
end;
theorem Th27:
-(-x + y) = x - y & -(-x + y) = x + -y
proof
-(-x + y) = -(-x) - y by Th25
.= x - y;
hence thesis;
end;
theorem
0 <= y & y < +infty implies z = z + y - y
proof
assume 0 <= y & y < +infty;
then y in REAL by XXREAL_0:14;
hence thesis by Th22;
end;
theorem Th29:
not (x = +infty & y = -infty) & not (x = -infty & y = +infty) &
not ( y = +infty & z = -infty or y = -infty & z = +infty ) &
not ( x = +infty & z = -infty or x = -infty & z = +infty ) implies
x + y + z = x + (y + z)
proof
assume
A1: ( not (x = +infty & y = -infty or x = -infty & y = +infty))& not ( y
= +infty & z = -infty or y = -infty & z = +infty ) & not ( x = +infty & z =
-infty or x = -infty & z = +infty );
per cases by A1,XXREAL_0:14;
suppose
x in REAL & y in REAL & z in REAL;
then reconsider A = x, B = y, C = z as Real;
A + B + C = x + y + z & A + (B + C) = x + (y + z);
hence thesis;
end;
suppose
A2: x in REAL & y = +infty & z in REAL;
then x + y = +infty & y + z = +infty by Def2;
hence thesis by A2;
end;
suppose
A3: x in REAL & y = -infty & z in REAL;
then x + y = -infty & y + z = -infty by Def2;
hence thesis by A3;
end;
suppose
A4: x = -infty & y in REAL & z in REAL;
then x + y = -infty by Def2;
then x + y + z = -infty by A4,Def2;
hence thesis by A4,Def2;
end;
suppose
A5: x = +infty & y in REAL & z in REAL;
then x + y = +infty by Def2;
then x + y + z = +infty by A5,Def2;
hence thesis by A5,Def2;
end;
suppose
A6: x in REAL & y in REAL & z = +infty;
then y + z = +infty by Def2;
then x + (y + z) = +infty by A6,Def2;
hence thesis by A6,Def2;
end;
suppose
A7: x in REAL & y in REAL & z = -infty;
then y + z = -infty by Def2;
then x + (y + z) = -infty by A7,Def2;
hence thesis by A7,Def2;
end;
suppose
A8: x = +infty & y = +infty & z in REAL;
then x + y = +infty by Def2;
then
A9: x + y + z = +infty by A8,Def2;
y + z <> -infty by A8,Def2;
hence thesis by A8,A9,Def2;
end;
suppose
A10: x in REAL & y = -infty & z = -infty;
then
A11: x + y = -infty by Def2;
then x + y + z = -infty by A10,Def2;
hence thesis by A10,A11;
end;
suppose
A12: x = -infty & y = -infty & z in REAL;
then
A13: x + y = -infty by Def2;
then x + y + z = -infty by A12,Def2;
hence thesis by A12,A13;
end;
suppose
x = -infty & y in REAL & z = -infty or x = -infty & y = -infty &
z = -infty or x = +infty & y in REAL & z = +infty or x = +infty & y = +infty &
z = +infty;
hence thesis;
end;
suppose
A14: x in REAL & y = +infty & z = +infty;
then x + y = +infty & y + z = +infty by Def2;
hence thesis by A14;
end;
end;
theorem Th30:
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))& not (x = -infty & y = +infty) and
A2: ( not (y = +infty & z = +infty))& not (y = -infty & z = -infty) and
A3: ( not (x = +infty & z = +infty))& not (x = -infty & z = -infty);
A4: ( not (x = +infty & -z = -infty))& not (x = -infty & -z = +infty) by A3
,Th23;
( not (y = +infty & -z = -infty))& not (y = -infty & -z = +infty) by A2,Th23;
hence thesis by A1,A4,Th29;
end;
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,Th13;
then
A8: x - y - z = +infty by A5,A7,Th13;
y + z <> +infty by A1,A5,A7,Lm8;
hence thesis by A7,A8,Th13;
end;
suppose
A9: x = -infty;
then x - y = -infty by A2,Th14;
then
A10: x - y - z = -infty by A6,A9,Th14;
y + z <> -infty by A2,A6,A9,Lm9;
hence thesis by A9,A10,Th14;
end;
suppose
A11: x <> +infty & x <> -infty;
then x in REAL by XXREAL_0:14;
then reconsider a = x as Real;
per cases;
suppose
A12: y = +infty;
then x - y = -infty & y + z = +infty by A3,A11,Def2,Th13;
hence thesis by A3,A12,Th14;
end;
suppose
A13: y = -infty;
then x - y = +infty & y + z = -infty by A4,A11,Def2,Th14;
hence thesis by A4,A13,Th13;
end;
suppose
y <> +infty & y <> -infty;
then y in REAL by XXREAL_0:14;
then reconsider b = y as Real;
A14: x - y = a - b;
per cases;
suppose
z = +infty;
then x - y - z = -infty & y + z = +infty by A14,Def2,Th13;
hence thesis by A11,Th13;
end;
suppose
z = -infty;
then x - y - z = +infty & y + z = -infty by A14,Def2,Th14;
hence thesis by A11,Th14;
end;
suppose
z <> +infty & z <> -infty;
then z in REAL by XXREAL_0:14;
then reconsider c = z as Real;
x - y - z = a - b - c & x - (y + z) = a - (b + c);
hence thesis;
end;
end;
end;
end;
theorem Th32:
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,Th13;
then
A8: x - y + z = +infty by A5,A7,Def2;
y - z <> +infty by A1,A5,A7,Th18;
hence thesis by A7,A8,Th13;
end;
suppose
A9: x = -infty;
then x - y = -infty by A2,Th14;
then
A10: x - y + z = -infty by A6,A9,Def2;
y - z <> -infty by A2,A6,A9,Th19;
hence thesis by A9,A10,Th14;
end;
suppose
A11: x <> +infty & x <> -infty;
then x in REAL by XXREAL_0:14;
then reconsider a = x as Real;
per cases;
suppose
A12: y = +infty;
then x - y = -infty & y - z = +infty by A3,A11,Th13;
hence thesis by A3,A12,Def2;
end;
suppose
A13: y = -infty;
then x - y = +infty & y - z = -infty by A4,A11,Th14;
hence thesis by A4,A13,Def2;
end;
suppose
y <> +infty & y <> -infty;
then y in REAL by XXREAL_0:14;
then reconsider b = y as Real;
A14: x - y = a - b;
per cases;
suppose
z = +infty;
then x - y + z = +infty & y - z = -infty by A14,Def2,Th13;
hence thesis by A11,Th14;
end;
suppose
z = -infty;
then x - y + z = -infty & y - z = +infty by A14,Def2,Th14;
hence thesis by A11,Th13;
end;
suppose
z <> +infty & z <> -infty;
then z in REAL by XXREAL_0:14;
then reconsider c = z as Real;
x - y + z = a - b + c & x - (y - z) = a - (b - c);
hence thesis;
end;
end;
end;
end;
theorem Th33:
z is real implies (z + x) - (z + y) = x - y
proof
assume
A1: z is real;
per cases by A1,XXREAL_0:14;
suppose
A2: x = -infty;
per cases by XXREAL_0:14;
suppose
A3: y = -infty;
(z + -infty) - (z + -infty) = -infty - (z + -infty) by A1,Def2
.= -infty - -infty by A1,Def2;
hence thesis by A2,A3;
end;
suppose
A4: y = +infty;
(z + -infty) - (z + +infty) = -infty - (z + +infty) by A1,Def2
.= -infty - +infty by A1,Def2;
hence thesis by A2,A4;
end;
suppose
A5: y in REAL;
then consider a,b being Complex such that
A6: z = a & y = b and
z+y = a + b by A1,Def2;
reconsider a,b as Real by A1,A5,A6;
A7: a+b in REAL by XREAL_0:def 1;
(z + -infty) - (z + y) = -infty - (z + y) by A1,Def2
.= -infty by A6,A7,Def2
.= -infty - y by A5,Def2;
hence thesis by A2;
end;
end;
suppose
A8: y = +infty;
per cases by XXREAL_0:14;
suppose
A9: x = -infty;
(z + -infty) - (z + +infty) = z + -infty - +infty by A1,Def2
.= -infty - +infty by A1,Def2;
hence thesis by A8,A9;
end;
suppose
A10: x = +infty;
(z + +infty) - (z + +infty) = z + +infty - +infty by A1,Def2
.= +infty - +infty by A1,Def2;
hence thesis by A8,A10;
end;
suppose
A11: x in REAL;
then consider a,b being Complex such that
A12: z = a & x = b and
z+x = a + b by A1,Def2;
reconsider a,b as Real by A1,A11,A12;
A13: a+b in REAL by XREAL_0:def 1;
A14: - +infty = -infty by Def3;
(z + x) - (z + +infty) = z + x - +infty by A1,Def2
.= z + x + -infty by Def3
.= -infty by A12,A13,Def2
.= x + - +infty by A11,A14,Def2;
hence thesis by A8;
end;
end;
suppose
x in REAL & y in REAL & z in REAL;
then reconsider a = x, b = y, c = z as Real;
(z + x) - (z + y) = (a + c) - (c + b) .= a - b
.= x - y;
hence thesis;
end;
suppose
A15: x = +infty & y in REAL & z in REAL;
then reconsider c = z, b = y as Real;
A16: z + y = c + b;
z + x = +infty & x - y = +infty by A15,Def2;
hence thesis by A16,Th13;
end;
suppose
A17: x in REAL & y = -infty & z in REAL;
then reconsider c = z, a = x as Real;
z + x = c + a & z + y = -infty by A17,Def2;
then (z + x) - (z + y) = +infty by Th14
.= x - y by A17,Th14;
hence thesis;
end;
suppose
A18: x = +infty & y = -infty & z in REAL;
then z + y = -infty & not z + x = -infty by Def2;
then (z + x) - (z + y) = +infty by Th14
.= x - y by A18,Th14;
hence thesis;
end;
end;
theorem
y is real implies (z - y) + (y - x) = z - x
proof
assume
A1: y is real;
thus (z - y) + (y - x) = (z - y) - (x - y) by Th27
.= z - x by A1,Th33;
end;
begin :: addition & order
Lm12: x <= y implies x + z <= y + z
proof
assume
A1: x <= y;
per cases by XXREAL_0:14;
suppose
A2: x in REAL & y in REAL;
per cases by XXREAL_0:14;
suppose
A3: z = -infty;
-infty <= y + z by XXREAL_0:5;
hence thesis by A2,A3,Def2;
end;
suppose
z in REAL;
then reconsider x, y, z as Real by A2;
x + z <= y + z by A1,XREAL_1:6;
hence thesis;
end;
suppose
A4: z = +infty;
x + z <= +infty by XXREAL_0:3;
hence thesis by A2,A4,Def2;
end;
end;
suppose
A5: x in REAL & y = +infty;
per cases by XXREAL_0:14;
suppose
A6: z = -infty;
-infty <= y+z by XXREAL_0:5;
hence thesis by A5,A6,Def2;
end;
suppose
A7: z in REAL;
x + z <= +infty by XXREAL_0:3;
hence thesis by A5,A7,Def2;
end;
suppose
z = +infty;
hence thesis by A5,Lm1,XXREAL_0:3;
end;
end;
suppose
A8: x = -infty & y in REAL;
per cases by XXREAL_0:14;
suppose
z = -infty;
hence thesis by A8,Lm2,XXREAL_0:5;
end;
suppose
A9: z in REAL;
-infty <= y + z by XXREAL_0:5;
hence thesis by A8,A9,Def2;
end;
suppose
A10: z = +infty;
x + z <= +infty by XXREAL_0:3;
hence thesis by A8,A10,Def2;
end;
end;
suppose
A11: x = -infty & y = +infty;
per cases by XXREAL_0:14;
suppose
z = -infty;
hence thesis by A11,Lm2;
end;
suppose
A12: z in REAL;
-infty <= y + z by XXREAL_0:5;
hence thesis by A11,A12,Def2;
end;
suppose
z = +infty;
hence thesis by A11,Lm1;
end;
end;
suppose
x = +infty;
hence thesis by A1,XXREAL_0:4;
end;
suppose
y = -infty;
hence thesis by A1,XXREAL_0:6;
end;
end;
Lm13: x >= 0 & y > 0 implies x + y > 0
proof
assume x >= 0;
then x + y >= 0 + y by Lm12;
hence thesis by Th4;
end;
Lm14: x <= 0 & y < 0 implies x + y < 0
proof
assume x <= 0;
then x + y <= 0 + y by Lm12;
hence thesis by Th4;
end;
registration
let x,y be non negative ExtReal;
cluster x + y -> non negative;
coherence
proof
per cases;
suppose
x = 0;
hence x + y >= 0 by Th4;
end;
suppose
x > 0;
hence x+y >= 0 by Lm13;
end;
end;
end;
registration
let x,y be non positive ExtReal;
cluster x + y -> non positive;
coherence
proof
per cases;
suppose
x = 0;
hence x + y <= 0 by Th4;
end;
suppose
x < 0;
hence x + y <= 0 by Lm14;
end;
end;
end;
registration
let x be positive ExtReal;
let y be non negative ExtReal;
cluster x + y -> positive;
coherence by Lm13;
cluster y + x -> positive;
coherence;
end;
registration
let x be negative ExtReal;
let y be non positive ExtReal;
cluster x + y -> negative;
coherence by Lm14;
cluster y + x -> negative;
coherence;
end;
registration
let x be non positive ExtReal;
cluster -x -> non negative;
coherence
proof
assume -x < 0;
then -x - -x < 0;
hence contradiction by Th7;
end;
end;
registration
let x be non negative ExtReal;
cluster -x -> non positive;
coherence
proof
assume -x > 0;
then -x - -x > 0;
hence contradiction by Th7;
end;
end;
registration
let x be positive ExtReal;
cluster -x -> negative;
coherence
proof
assume -x >= 0;
then -x- -x > 0;
hence contradiction by Th7;
end;
end;
registration
let x be negative ExtReal;
cluster -x -> positive;
coherence
proof
assume -x <= 0;
then -x- -x < 0;
hence contradiction by Th7;
end;
end;
registration
let x be non negative ExtReal, y be non positive ExtReal;
cluster x - y -> non negative;
coherence;
cluster y - x -> non positive;
coherence;
end;
registration
let x be positive ExtReal;
let y be non positive ExtReal;
cluster x - y -> positive;
coherence;
cluster y - x -> negative;
coherence;
end;
registration
let x be negative ExtReal;
let y be non negative ExtReal;
cluster x - y -> negative;
coherence;
cluster y - x -> positive;
coherence;
end;
Lm15: for x,y st x <= y holds - y <= - x
proof
let x,y;
assume
A1: x <= y;
per cases;
case that
A2: -y in REAL and
A3: -x in REAL;
x in REAL by A3,Lm3;
then consider a being Complex such that
A4: x = a and
A5: -x = - a by Def3;
y in REAL by A2,Lm3;
then consider b being Complex such that
A6: y = b and
A7: -y = - b by Def3;
x in REAL & y in REAL by A2,A3,Lm3;
then reconsider a,b as Real by A6,A4;
reconsider mb=-b, ma=-a as Element of REAL by XREAL_0:def 1;
take mb,ma;
thus mb = -y & ma = -x by A7,A5;
thus thesis by A1,A6,A4,XREAL_1:24;
end;
case
not(-y in REAL & -x in REAL);
then not(y in REAL & x in REAL) by Lm3;
then x = -infty or y = +infty by A1,Def1;
hence thesis by Def3;
end;
end;
theorem
x <= y implies x + z <= y + z by Lm12;
theorem Th36:
x <= y & z <= w implies x + z <= y + w
proof
assume that
A1: x <= y and
A2: z <= w;
per cases;
suppose
A3: x = +infty & z = -infty;
A4: w <> -infty implies +infty + w = +infty by Def2;
y = +infty by A1,A3,XXREAL_0:4;
hence thesis by A3,A4;
end;
suppose
A5: x = -infty & z = +infty;
A6: y <> -infty implies +infty + y = +infty by Def2;
w = +infty by A2,A5,XXREAL_0:4;
hence thesis by A5,A6;
end;
suppose
A7: y = +infty & w = -infty;
A8: x <> +infty implies -infty + x = -infty by Def2;
z = -infty by A2,A7,XXREAL_0:6;
hence thesis by A7,A8;
end;
suppose
A9: y = -infty & w = +infty;
A10: z <> +infty implies -infty + z = -infty by Def2;
x = -infty by A1,A9,XXREAL_0:6;
hence thesis by A9,A10;
end;
suppose
A11: not ( x = +infty & z = -infty or x = -infty & z = +infty ) & not
( y = +infty & w = -infty or y = -infty & w = +infty );
reconsider a = x + z, b = y + w as Element of ExtREAL by XXREAL_0:def 1;
A12: not(a = +infty & b = -infty)
proof
assume that
A13: a = +infty and
A14: b = -infty;
x = +infty or z = +infty by A13,Lm8;
hence thesis by A1,A2,A11,A14,Lm9,XXREAL_0:4;
end;
A15: a in REAL & b in REAL implies a <= b
proof
assume
A16: a in REAL & b in REAL;
then
A17: z in REAL & w in REAL by A11,Th20;
x in REAL & y in REAL by A11,A16,Th20;
then consider Ox,Oy,Os,Ot being Real such that
A18: Ox = x & Oy = y & Os = z & Ot = w and
A19: Ox <= Oy & Os <= Ot by A1,A2,A17;
Ox + Os <= Os + Oy & Os + Oy <= Ot + Oy by A19,XREAL_1:6;
hence thesis by A18,XXREAL_0:2;
end;
A20: a = +infty & b in REAL implies a <= b
proof
assume that
A21: a = +infty and
b in REAL;
x = +infty or z = +infty by A21,Lm8;
then y = +infty or w = +infty by A1,A2,XXREAL_0:4;
then b = +infty by A11,Def2;
hence thesis by XXREAL_0:4;
end;
A22: a in REAL & b = -infty implies a <= b
proof
assume that
a in REAL and
A23: b = -infty;
y = -infty or w = -infty by A23,Lm9;
then x = -infty or z = -infty by A1,A2,XXREAL_0:6;
then a = -infty by A11,Def2;
hence thesis by XXREAL_0:5;
end;
a in REAL & b in REAL or a in REAL & b = +infty or a in REAL & b =
-infty or a = +infty & b in REAL or a = +infty & b = +infty or a = +infty & b =
-infty or a = -infty & b in REAL or a = -infty & b = +infty or a = -infty & b =
-infty by XXREAL_0:14;
hence thesis by A15,A22,A20,A12,XXREAL_0:4,5;
end;
end;
theorem Th37:
x <= y & z <= w implies x - w <= y - z
proof
assume that
A1: x <= y and
A2: z <= w;
-w <= -z by A2,Lm15;
hence thesis by A1,Th36;
end;
theorem Th38:
x <= y iff - y <= - x
proof
thus x <= y implies - y <= - x by Lm15;
- y <= - x implies --x <= --y by Lm15;
hence thesis;
end;
theorem Th39:
0 <= z implies x <= x + z
proof
assume 0 <= z;
then x + 0 <= x + z by Th36;
hence thesis by Th4;
end;
theorem
x <= y implies y-x >= 0
proof
assume x <= y;
then -y <= -x by Lm15;
then -y +y <= y + -x by Th36;
hence thesis by Th7;
end;
theorem
(z = -infty & y = +infty implies x <= 0) & (z = +infty & y = -infty
implies x <= 0) implies (x - y <= z implies x <= z + y)
proof
assume that
A1: z = -infty & y = +infty implies x <= 0 and
A2: z = +infty & y = -infty implies x <= 0 and
A3: x - y <= z;
per cases by XXREAL_0:14;
suppose
A4: z = -infty;
per cases by A3,A4,Th19,XXREAL_0:6;
suppose
x = -infty;
hence thesis by XXREAL_0:5;
end;
suppose
y = +infty;
hence thesis by A1,A4;
end;
end;
suppose
A5: z = +infty;
per cases;
suppose
y = -infty;
hence thesis by A2,A5;
end;
suppose
y <> -infty;
then z + y = +infty by A5,Def2;
hence thesis by XXREAL_0:3;
end;
end;
suppose
A6: z in REAL;
per cases by A3,A6,XXREAL_0:13;
suppose
A7: x-y in REAL;
per cases by A7,Th21;
suppose
y = +infty;
then z + y = +infty by A6,Def2;
hence thesis by XXREAL_0:3;
end;
suppose
x = -infty;
hence thesis by XXREAL_0:5;
end;
suppose
x in REAL & y in REAL;
then reconsider a = x, b = y, c = z as Element of REAL by A6;
a - b <= c by A3;
then a <= b + c by XREAL_1:20;
hence thesis;
end;
end;
suppose
A8: x-y = -infty;
per cases by A8,Th19;
suppose
x = -infty;
hence thesis by XXREAL_0:5;
end;
suppose
y = +infty;
then z + y = +infty by A6,Def2;
hence thesis by XXREAL_0:3;
end;
end;
end;
end;
theorem
(x = +infty & y = +infty implies 0 <= z) & (x = -infty & y = -infty
implies 0 <= z) implies (x <= z + y implies x - y <= z)
proof
assume that
A1: x = +infty & y = +infty implies 0 <= z and
A2: x = -infty & y = -infty implies 0 <= z and
A3: x <= z + y;
per cases by XXREAL_0:14;
suppose
A4: x = +infty;
per cases by A3,A4,Lm8,XXREAL_0:4;
suppose
z = +infty;
hence thesis by XXREAL_0:3;
end;
suppose
y = +infty;
hence thesis by A1,A4,Th7;
end;
end;
suppose
A5: x = -infty;
per cases;
suppose
y = -infty;
hence thesis by A2,A5,Th7;
end;
suppose
--y <> -infty;
then -y <> +infty by Def3;
then x - y = -infty by A5,Def2;
hence thesis by XXREAL_0:5;
end;
end;
suppose
A6: x in REAL;
per cases by A3,A6,XXREAL_0:10;
suppose
A7: z + y in REAL;
per cases by A7,Th20;
suppose
y = +infty;
then x - y = -infty by A6,Def2,Th5;
hence thesis by XXREAL_0:5;
end;
suppose
z = +infty;
hence thesis by XXREAL_0:3;
end;
suppose
z in REAL & y in REAL;
then reconsider a = x, b = y, c = z as Element of REAL by A6;
a <= b + c by A3;
then a - b <= c by XREAL_1:20;
hence thesis;
end;
end;
suppose
A8: z + y = +infty;
per cases by A8,Lm8;
suppose
z = +infty;
hence thesis by XXREAL_0:3;
end;
suppose
y = +infty;
then x - y = -infty by A6,Def2,Th5;
hence thesis by XXREAL_0:5;
end;
end;
end;
end;
theorem Th43:
z in REAL & x < y implies x + z < y + z & x - z < y - z
proof
assume that
A1: z in REAL and
A2: x < y;
A3: x + z <> y + z
proof
assume x + z = y + z;
then x = (y + z) - z by A1,Th22
.= y by A1,Th22;
hence thesis by A2;
end;
A4: x - z <> y - z
proof
assume x - z = y - z;
then x = (y - z) + z by A1,Th22
.= y by A1,Th22;
hence thesis by A2;
end;
x + z <= y + z & x - z <= y - z by A2,Th36;
hence thesis by A3,A4,XXREAL_0:1;
end;
theorem
0<= x & 0<= y & 0<= z implies (x + y) + z = x + (y + z)
proof
assume that
A1: 0<= x and
A2: 0<= y and
A3: 0<= z;
per cases by A1,A2,A3,XXREAL_0:14;
suppose
x in REAL & y in REAL & z in REAL;
then consider a,b,c,d,e being Real such that
A4: x = a & y = b & z = c and
x + y = d and
y + z = e;
(x + y) + z = (a + b) + c by A4
.= a + (b + c)
.= x + (y + z) by A4;
hence thesis;
end;
suppose
A5: x = +infty;
then (x + y) + z = +infty + z by A2,Def2
.= +infty by A3,Def2
.= +infty + (y + z) by A2,A3,Def2;
hence thesis by A5;
end;
suppose
A6: y = +infty;
then (x + y) + z = +infty + z by A1,Def2
.= +infty by A3,Def2
.= x + (+infty) by A1,Def2
.= x + (+infty + z) by A3,Def2;
hence thesis by A6;
end;
suppose
A7: z = +infty;
then (x + y) + z = +infty by A1,A2,Def2
.= x + (+infty) by A1,Def2
.= x + (y + (+infty)) by A2,Def2;
hence thesis by A7;
end;
end;
theorem Th45:
x is real implies (y + x <= z iff y <= z - x)
proof
assume
A1: x is real;
A2: (z - x) + x = z
proof
per cases by XXREAL_0:14;
suppose
z in REAL;
then reconsider a = x, b = z as Real by A1;
thus (z - x) + x = (b - a) + a .= z;
end;
suppose
A3: z = -infty;
hence (z - x) + x = -infty + x by A1,Th14
.= z by A1,A3,Def2;
end;
suppose
A4: z = +infty;
hence (z - x) + x = +infty + x by A1,Th13
.= z by A1,A4,Def2;
end;
end;
hereby
A5: (y + x) - x = y
proof
per cases by XXREAL_0:14;
suppose
y in REAL;
then reconsider a = x, b = y as Element of REAL by A1,XXREAL_0:14;
(y + x) - x = (b + a) - a .= y;
hence thesis;
end;
suppose
A6: y = -infty or y = +infty;
per cases by A6;
suppose
A7: y = -infty;
hence (y + x) - x = -infty - x by A1,Def2
.= y by A1,A7,Th14;
end;
suppose
A8: y = +infty;
hence (y + x) - x = +infty - x by A1,Def2
.= y by A1,A8,Th13;
end;
end;
end;
assume y + x <= z;
hence y <= z - x by A5,Th37;
end;
assume y <= z - x;
hence thesis by A2,Th36;
end;
theorem Th46:
0 < x & x < y implies 0 < y - x
proof
assume that
A1: 0 < x and
A2: x < y;
A3: x in REAL by A1,A2,XXREAL_0:48;
A4: 0 <> y - x
proof
assume 0= y - x;
then x = (y - x) + x by Th4
.= y by A3,Th22;
hence thesis by A2;
end;
0 + x < y by A2,Th4;
hence thesis by A3,A4,Th45;
end;
Lm16: 0 in REAL by XREAL_0:def 1;
theorem
0 <= x & 0 <= z & z + x < y implies z < y - x
proof
assume that
A1: 0 <= x and
A2: 0 <= z and
A3: z + x < y;
x in REAL
proof
A4: x <> +infty
proof
assume x = +infty;
then +infty < y by A2,A3,Def2;
hence thesis by XXREAL_0:4;
end;
assume not x in REAL;
hence thesis by A1,A4,XXREAL_0:10,Lm16;
end;
then z <= y - x & z <> y - x by A3,Th22,Th45;
hence thesis by XXREAL_0:1;
end;
theorem
0 <= x & 0 <= z & z + x < y implies z <= y
proof
assume that
A1: 0 <= x and
A2: 0 <= z and
A3: z + x < y;
x in REAL
proof
A4: x <> +infty
proof
assume x = +infty;
then +infty < y by A2,A3,Def2;
hence thesis by XXREAL_0:4;
end;
assume not x in REAL;
hence thesis by A1,A4,XXREAL_0:10,Lm16;
end;
then
A5: (z + x) - x = z by Th22;
y - 0 = y by Th15;
hence thesis by A1,A3,A5,Th37;
end;
theorem Th49:
0 <= x & x < z implies ex y being Real st 0 < y & x + y < z
proof
assume that
A1: 0 <= x and
A2: x < z;
per cases by A1;
suppose
A3: 0 < x;
then 0 < z - x by A2,Th46;
then consider y being Real such that
A4: 0 < y and
A5: y < z - x by Th3;
take y;
A6: x + y <= x + (z - x) by A5,Th36;
A7: x in REAL by A2,A3,XXREAL_0:48;
then
A8: x + (z - x) = z by Th22;
x + y <> z by A7,A5,Th22;
hence thesis by A4,A6,A8,XXREAL_0:1;
end;
suppose
A9: 0 = x;
consider y being Real such that
A10: 0 < y & y < z by A1,A2,Th3;
take y;
thus thesis by A9,A10,Th4;
end;
end;
theorem
0 < x implies ex y being Real st 0 < y & y + y < x
proof
assume 0 < x;
then consider x1 being Real such that
A1: 0 < x1 and
A2: x1 < x by Th3;
consider x2 being Real such that
A3: 0 < x2 and
A4: x1 + x2 < x by A1,A2,Th49;
take y = min(x1,x2);
per cases;
suppose
A5: x1 <= x2;
hence 0 < y by A1,XXREAL_0:def 9;
y = x1 by A5,XXREAL_0:def 9;
then y + y <= x1 + x2 by A5,Th36;
hence thesis by A4,XXREAL_0:2;
end;
suppose
A6: x2 <= x1;
hence 0 < y by A3,XXREAL_0:def 9;
y = x2 by A6,XXREAL_0:def 9;
then y + y <= x1 + x2 by A6,Th36;
hence thesis by A4,XXREAL_0:2;
end;
end;
theorem Th51:
x < y & x < +infty & -infty < y implies 0 < y- x
proof
assume that
A1: x < y and
A2: x < +infty and
A3: -infty < y;
per cases;
suppose
y = +infty;
hence thesis by A2,Th13;
end;
suppose
A4: y <> +infty;
per cases;
suppose
x = -infty;
hence thesis by A3,Th14;
end;
suppose
A5: x <> -infty;
A6: y in REAL by A3,A4,XXREAL_0:14;
x in REAL by A2,A5,XXREAL_0:14;
then reconsider a = x, b = y as Real by A6;
b - a > 0 by A1,XREAL_1:50;
hence thesis;
end;
end;
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 x<>+infty by A1,A2,Def2;
then
A4: x < +infty by XXREAL_0:4;
y<>+infty by A1,A2,A3,Def2;
hence thesis by A3,A4,Th13;
end;
suppose
A5: z <> +infty;
A6: -infty <= x + y by XXREAL_0:5;
then z in REAL by A2,A5,XXREAL_0:14;
then reconsider c = z as Real;
A7: x + y < +infty by A2,XXREAL_0:2,4;
then
A8: x <> +infty by A1,Def2;
A9: y <> +infty by A1,A7,Def2;
per cases;
suppose
A10: y = -infty;
then x < +infty by A1,XXREAL_0:4;
hence thesis by A2,A6,A10,Th14;
end;
suppose
y <> -infty;
then y in REAL by A9,XXREAL_0:14;
then reconsider b = y as Real;
per cases;
suppose
A11: x = -infty;
hence x <> +infty;
A12: z - y = c - b;
hence y <> +infty;
thus z <> -infty by A12;
c-b in REAL by XREAL_0:def 1;
hence thesis by A11,XXREAL_0:12;
end;
suppose
x <> -infty;
then x in REAL by A8,XXREAL_0:14;
then reconsider a = x as Real;
x + y = a + b;
then a < c - b by A2,XREAL_1:20;
hence thesis;
end;
end;
end;
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;
A4: -infty <= z by XXREAL_0:5;
z<>-infty by A1,A2,A3,Th14;
then
A5: -infty < z by A4,XXREAL_0:1;
y<>+infty by A1,A2,A3,Th13;
hence thesis by A3,A5,Def2;
end;
suppose
A6: x <> -infty;
A7: z - y <= +infty by XXREAL_0:4;
then x in REAL by A2,A6,XXREAL_0:14;
then reconsider a = x as Real;
A8: -infty <= x by XXREAL_0:5;
then
A9: z <> -infty by A1,A2,Th14;
A10: y <> +infty by A1,A2,A8,Th13;
per cases;
suppose
A11: y = -infty;
-infty <= z by XXREAL_0:5;
then -infty < z by A1,A11,XXREAL_0:1;
hence thesis by A2,A7,A11,Def2;
end;
suppose
y <> -infty;
then y in REAL by A10,XXREAL_0:14;
then reconsider b = y as Real;
per cases;
suppose
A12: z = +infty;
a+b in REAL by XREAL_0:def 1;
hence thesis by A12,XXREAL_0:9;
end;
suppose
z <> +infty;
then z in REAL by A9,XXREAL_0:14;
then reconsider c = z as Real;
z - y = c - b;
then a + b < c by A2,XREAL_1:20;
hence thesis;
end;
end;
end;
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 x<>+infty by A1,A2,Th13;
then
A4: x < +infty by XXREAL_0:4;
y<>-infty by A1,A2,A3,Th14;
hence thesis by A3,A4,Def2;
end;
suppose
A5: z <> +infty;
A6: -infty <= x - y by XXREAL_0:5;
then z in REAL by A2,A5,XXREAL_0:14;
then reconsider c = z as Real;
A7: x - y < +infty by A2,XXREAL_0:2,4;
then
A8: x <> +infty by A1,Th13;
A9: y <> -infty by A1,A7,Th14;
per cases;
suppose
A10: y = +infty;
then x < +infty by A1,XXREAL_0:4;
hence thesis by A2,A6,A10,Def2;
end;
suppose
y <> +infty;
then y in REAL by A9,XXREAL_0:14;
then reconsider b = y as Real;
per cases;
suppose
A11: x = -infty;
c+b in REAL by XREAL_0:def 1;
hence thesis by A11,XXREAL_0:12;
end;
suppose
x <> -infty;
then x in REAL by A8,XXREAL_0:14;
then reconsider a = x as Real;
x - y = a - b;
then a < c + b by A2,XREAL_1:19;
hence thesis;
end;
end;
end;
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;
A4: -infty <= z by XXREAL_0:5;
z<>-infty by A1,A2,A3,Def2;
then
A5: -infty < z by A4,XXREAL_0:1;
y<>-infty by A1,A2,A3,Def2;
hence thesis by A3,A5,Th14;
end;
suppose
A6: x <> -infty;
A7: z + y <= +infty by XXREAL_0:4;
then x in REAL by A2,A6,XXREAL_0:14;
then reconsider a = x as Real;
A8: -infty <= x by XXREAL_0:5;
then
A9: z <> -infty by A1,A2,Def2;
A10: y <> -infty by A1,A2,A8,Def2;
per cases;
suppose
A11: y = +infty;
-infty <= z by XXREAL_0:5;
then -infty < z by A1,A11,XXREAL_0:1;
hence thesis by A2,A7,A11,Th13;
end;
suppose
y <> +infty;
then y in REAL by A10,XXREAL_0:14;
then reconsider b = y as Real;
per cases;
suppose
A12: z = +infty;
a-b in REAL by XREAL_0:def 1;
hence thesis by A12,XXREAL_0:9;
end;
suppose
z <> +infty;
then z in REAL by A9,XXREAL_0:14;
then reconsider c = z as Real;
z + y = c + b;
then a - b < c by A2,XREAL_1:19;
hence thesis;
end;
end;
end;
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,Def2;
hence contradiction by A1,A2,A3,XXREAL_0:4;
end;
per cases;
suppose
z = +infty;
then z - y = +infty by A1,Th13;
hence thesis by XXREAL_0:4;
end;
suppose
A4: z <> +infty;
then
A5: x + y < +infty by A2,XXREAL_0:2,4;
then
A6: x <> +infty by A1,Def2;
A7: y <> +infty by A1,A5,Def2;
per cases;
suppose
x = -infty;
hence thesis by XXREAL_0:5;
end;
suppose
x <> -infty;
then x in REAL by A6,XXREAL_0:14;
then reconsider a = x as Real;
per cases;
suppose
y = -infty;
then z - y = +infty by A1,Th14;
hence thesis by XXREAL_0:4;
end;
suppose
y <> -infty;
then y in REAL by A7,XXREAL_0:14;
then reconsider b = y as Real;
a+b in REAL by XREAL_0:def 1;
then z <> -infty by A2,XXREAL_0:12;
then z in REAL by A4,XXREAL_0:14;
then reconsider c = z as Real;
x + y = a + b;
then a <= c - b by A2,XREAL_1:19;
hence thesis;
end;
end;
end;
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,Th13;
hence contradiction by A2,A4,A6,XXREAL_0:6;
end;
per cases by A5;
suppose
y = -infty;
then x + y = -infty by A1,Def2;
hence thesis by XXREAL_0:5;
end;
suppose
A7: y <> +infty & y <> -infty;
- -infty = +infty by Def3;
then
A8: -y <> -infty by A7;
- +infty = -infty by Def3;
then -y <> +infty by A7;
then z - y + y = z + (-y + y) by A7,A8,Th29
.= z + 0 by Th7
.= z by Th4;
hence thesis by A4,Th36;
end;
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
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;
assume
A3: y = -infty;
then x - y = +infty by A1,Th14;
hence contradiction by A1,A2,A3,XXREAL_0:4;
end;
theorem
not (x = -infty & y = -infty) & not (y = -infty & z = +infty) & x <= z
+ y implies y <> -infty
proof
assume that
A1: not(x=-infty & y=-infty) and
A2: not(y = -infty & z = +infty) and
A3: x <= z + y;
assume
A4: y = -infty;
then z + y = -infty by A2,Def2;
hence contradiction by A1,A3,A4,XXREAL_0:6;
end;
theorem
(x <= -y implies y <= -x) & (-x <= y implies -y <= x)
proof
x <= -y implies --y <= -x by Th38;
hence x <= -y implies y <= -x;
-x <= y implies -y <= --x by Th38;
hence thesis;
end;
theorem
(for e be Real st 0 < e holds x < y + e) implies x <= y
proof
assume
A1: for e be Real st 0 < e holds x < y + e;
per cases;
suppose
A2: y = +infty or y=-infty;
per cases by A2;
suppose
y=+infty;
hence thesis by XXREAL_0:4;
end;
suppose
A3: y=-infty;
x < y + 1 by A1;
hence thesis by A3,Def2;
end;
end;
suppose
A4: y <> +infty & y <>-infty;
per cases;
suppose
A5: x = +infty;
x < y+ 1 by A1;
hence thesis by A5,XXREAL_0:4;
end;
suppose
A6: x <> +infty;
now
assume
A7: x <> -infty;
then x in REAL by A6,XXREAL_0:14;
then reconsider x1=x as Real;
-infty <= x by XXREAL_0:5;
then
A8: -infty < x by A7,XXREAL_0:1;
y in REAL by A4,XXREAL_0:14;
then reconsider y1=y as Real;
assume
A9: not x <= y;
y < +infty by A4,XXREAL_0:4;
then 0 < x- y by A9,A8,Th51;
then x < y + (x1-y1) by A1;
then x < y + x-y by Th30;
then x < x +(y-y) by A4,Th30;
then x < x +0 by Th7;
hence contradiction by Th4;
end;
hence thesis by XXREAL_0:5;
end;
end;
end;
reserve t for ExtReal;
theorem
t <> -infty & t <> +infty & x < y implies x + t < y + t
proof
assume that
A1: t <> -infty & t <> +infty and
A2: x < y;
A3: t-t = 0 by Th7;
A4: now
assume x + t = y + t;
then x + (t -t) = y + t-t by A1,Th30;
then x+ 0 = y + (t-t) by A1,A3,Th30;
then x=y+ 0 by A3,Th4;
hence contradiction by A2,Th4;
end;
x + t <= y + t by A2,Th36;
hence thesis by A4,XXREAL_0:1;
end;
theorem
t <> -infty & t <> +infty & x < y implies x - t < y - t
proof
assume that
A1: t <> -infty & t <> +infty and
A2: x < y;
A3: t-t = 0 by Th7;
A4: now
assume x - t = y - t;
then x - (t -t) = y - t+t by A1,Th32;
then x - 0 = y - (t-t) by A1,A3,Th32;
then x= y+ 0 by A3,Th4;
hence contradiction by A2,Th4;
end;
x - t <= y - t by A2,Th37;
hence thesis by A4,XXREAL_0:1;
end;
theorem
x < y & w < z implies x + w < y + z
proof
assume that
A1: x < y and
A2: w < z;
-infty <= w by XXREAL_0:5;
then per cases by XXREAL_0:1;
suppose
A3: w = -infty;
A4: y <> -infty & z <> -infty by A1,A2,XXREAL_0:5;
x <> +infty by A1,XXREAL_0:3;
then x + w = -infty by A3,Def2;
hence thesis by A4,Lm9,XXREAL_0:6;
end;
suppose
A5: -infty < w;
per cases;
suppose
A6: y = +infty;
A7: z <= +infty by XXREAL_0:4;
y + z = +infty by A5,A2,A6,Def2;
hence thesis by A1,A2,A6,A7,Lm8,XXREAL_0:4;
end;
suppose
A8: y <> +infty;
-infty <= x by XXREAL_0:5;
then y in REAL by A1,A8,XXREAL_0:14;
then
A9: y + w < y + z by A2,Th43;
z <= +infty by XXREAL_0:4;
then w in REAL by A5,A2,XXREAL_0:14;
then x + w < y + w by A1,Th43;
hence thesis by A9,XXREAL_0:2;
end;
end;
end;
theorem
0 <= x & z + x <= y implies z <= y
proof
assume 0 <= x;
then z <= z + x by Th39;
hence thesis by XXREAL_0:2;
end;
begin :: multiplication
definition
let x,y be ExtReal;
func x * y -> ExtReal means
:Def5:
ex a,b being Complex st x = a & y = b & it = a * b
if x is real & y is real,
it = +infty if (x is not real or y is not real) &
(x is positive & y is positive or x is negative & y is negative),
it = -infty if (x is not real or y is not real) &
(x is positive & y is negative or x is negative & y is positive)
otherwise it = 0;
existence
proof
thus x is real & y is real implies ex c being ExtReal, a, b being
Complex st x = a & y = b & c = a * b
proof
assume x is real & y is real;
then reconsider a = x, b = y as Real;
take a*b, a, b;
thus thesis;
end;
thus thesis;
end;
uniqueness;
consistency;
commutativity;
end;
registration
let x,y be Real, a,b be Complex;
identify x*y with a*b when x = a, y = b;
compatibility by Def5;
end;
definition
let x be ExtReal;
func x" -> ExtReal means
:Def6:
ex a being Complex st x = a & it = a" if x is real otherwise it = 0;
existence
proof
thus x is real implies ex c being ExtReal, a being Complex
st x = a & c = a"
proof
assume x is real;
then reconsider a = x as Real;
take a", a;
thus thesis;
end;
thus thesis;
end;
uniqueness;
consistency;
end;
registration
let x be Real, a be Complex;
identify x" with a" when x = a;
compatibility by Def6;
end;
definition
let x,y be ExtReal;
func x / y -> ExtReal equals
x * y";
coherence;
end;
registration
let x,y be Real, a,b be Complex;
identify x/y with a/b when x = a, y = b;
compatibility
proof
reconsider y1=y" as Real;
assume x = a & y = b;
hence a / b = x * y1 .= x / y;
end;
end;
Lm17: x * 0 = 0
proof
per cases by XXREAL_0:14;
suppose
x in REAL;
then ex a,b being Complex st x = a & 0 = b & x * 0 = a * b by Def5;
hence thesis;
end;
suppose
x = +infty;
hence thesis by Def5;
end;
suppose
x = -infty;
hence thesis by Def5;
end;
end;
registration
let x be positive ExtReal, y be negative ExtReal;
cluster x*y -> negative;
coherence
proof
per cases;
suppose
x in REAL & y in REAL;
then reconsider x,y as Real;
x*y < 0;
hence thesis;
end;
suppose
not x in REAL or not y in REAL;
then x is not real or y is not real by XREAL_0:def 1;
hence thesis by Def5;
end;
end;
end;
registration
let x,y be negative ExtReal;
cluster x*y -> positive;
coherence
proof
per cases;
suppose
x in REAL & y in REAL;
then reconsider x,y as Real;
x*y > 0;
hence thesis;
end;
suppose
not x in REAL or not y in REAL;
then x is not real or y is not real by XREAL_0:def 1;
hence thesis by Def5;
end;
end;
end;
registration
let x,y be positive ExtReal;
cluster x*y -> positive;
coherence
proof
per cases;
suppose
x in REAL & y in REAL;
then reconsider x,y as Real;
x*y > 0;
hence thesis;
end;
suppose
not x in REAL or not y in REAL;
then x is not real or y is not real by XREAL_0:def 1;
hence thesis by Def5;
end;
end;
end;
registration
let x be non positive ExtReal, y be non negative ExtReal;
cluster x*y -> non positive;
coherence
proof
per cases;
suppose
x = 0 or y = 0;
hence x * y <= 0 by Lm17;
end;
suppose
x < 0 & y > 0;
hence x * y <= 0;
end;
end;
end;
registration
let x,y be non positive ExtReal;
cluster x*y -> non negative;
coherence
proof
per cases;
suppose
x = 0 or y = 0;
hence x * y >= 0 by Lm17;
end;
suppose
x < 0 & y < 0;
hence x * y >= 0;
end;
end;
end;
registration
let x,y be non negative ExtReal;
cluster x*y -> non negative;
coherence
proof
per cases;
suppose
x = 0 or y = 0;
hence x * y >= 0 by Lm17;
end;
suppose
x > 0 & y > 0;
hence x * y >= 0;
end;
end;
end;
registration
let x be non positive ExtReal;
cluster x" -> non positive;
coherence
proof
per cases;
suppose
x is real;
then reconsider x as Real;
x" is non positive;
hence thesis;
end;
suppose
x is not real;
hence thesis by Def6;
end;
end;
end;
registration
let x be non negative ExtReal;
cluster x" -> non negative;
coherence
proof
per cases;
suppose
x is real;
then reconsider x as Real;
x" is non negative;
hence thesis;
end;
suppose
x is not real;
hence thesis by Def6;
end;
end;
end;
registration
let x be non negative ExtReal, y be non positive ExtReal;
cluster x/y -> non positive;
coherence;
cluster y/x -> non positive;
coherence;
end;
registration
let x,y be non negative ExtReal;
cluster x/y -> non negative;
coherence;
end;
registration
let x,y be non positive ExtReal;
cluster x/y -> non negative;
coherence;
end;
Lm18: x is not real & x*y = 0 implies y = 0
proof
assume that
A1: x is not real and
A2: x*y = 0;
not(x is positive & y is positive or x is negative & y is negative) by A2;
hence thesis by A1,A2;
end;
registration
let x,y be non zero ExtReal;
cluster x*y -> non zero;
coherence
proof
per cases;
suppose x is real & y is real;
then reconsider r=x, s=y as Real;
assume x*y is zero;
then r*s = 0;
hence contradiction;
end;
suppose x is not real or y is not real;
then x*y <> 0 by Lm18;
hence thesis;
end;
end;
end;
registration
let x be zero ExtReal, y be ExtReal;
cluster x*y -> zero for ExtReal;
coherence by Lm17;
end;
Lm19: x = 0 implies x*(y*z) = (x*y)*z
proof
assume
A1: x = 0;
hence x*(y*z) = 0 .= (x*y)*z by A1;
end;
Lm20: y = 0 implies x*(y*z) = (x*y)*z
proof
assume
A1: y = 0;
hence x*(y*z) = 0 .= (x*y)*z by A1;
end;
Lm21: y is not real implies x*(y*z) = (x*y)*z
proof
assume y is not real;
then
A1: not y in REAL;
assume
A2: not thesis;
then
A3: x <> 0 & z <> 0 by Lm19;
per cases by A1,XXREAL_0:14;
suppose
A4: y = -infty;
per cases by A3;
suppose
A5: x is positive & z is positive;
then x*(-infty*z) = x*-infty by Def5
.= -infty by A5,Def5
.= -infty*z by A5,Def5
.= (x*-infty)*z by A5,Def5;
hence thesis by A2,A4;
end;
suppose
A6: x is positive & z is negative;
then x*(-infty*z) = x*+infty by Def5
.= +infty by A6,Def5
.= -infty*z by A6,Def5
.= (x*-infty)*z by A6,Def5;
hence thesis by A2,A4;
end;
suppose
A7: x is negative & z is positive;
then x*(-infty*z) = x*-infty by Def5
.= +infty by A7,Def5
.= +infty*z by A7,Def5
.= (x*-infty)*z by A7,Def5;
hence thesis by A2,A4;
end;
suppose
A8: x is negative & z is negative;
then x*(-infty*z) = x*+infty by Def5
.= -infty by A8,Def5
.= +infty*z by A8,Def5
.= (x*-infty)*z by A8,Def5;
hence thesis by A2,A4;
end;
end;
suppose
A9: y = +infty;
per cases by A3;
suppose
A10: x is positive & z is positive;
then x*(+infty*z) = x*+infty by Def5
.= +infty by A10,Def5
.= +infty*z by A10,Def5
.= (x*+infty)*z by A10,Def5;
hence thesis by A2,A9;
end;
suppose
A11: x is positive & z is negative;
then x*(+infty*z) = x*-infty by Def5
.= -infty by A11,Def5
.= +infty*z by A11,Def5
.= (x*+infty)*z by A11,Def5;
hence thesis by A2,A9;
end;
suppose
A12: x is negative & z is positive;
then x*(+infty*z) = x*+infty by Def5
.= -infty by A12,Def5
.= -infty*z by A12,Def5
.= (x*+infty)*z by A12,Def5;
hence thesis by A2,A9;
end;
suppose
A13: x is negative & z is negative;
then x*(+infty*z) = x*-infty by Def5
.= +infty by A13,Def5
.= -infty*z by A13,Def5
.= (x*+infty)*z by A13,Def5;
hence thesis by A2,A9;
end;
end;
end;
Lm22: x is not real implies x*(y*z) = (x*y)*z
proof
assume x is not real;
then
A1: not x in REAL;
assume
A2: not thesis;
then
A3: y <> 0 & z <> 0 by Lm19,Lm20;
per cases by A1,XXREAL_0:14;
suppose
A4: x = -infty;
per cases by A3;
suppose
A5: y is positive & z is positive;
then -infty*(y*z) = -infty by Def5
.= -infty*z by A5,Def5
.= (-infty*y)*z by A5,Def5;
hence thesis by A2,A4;
end;
suppose
A6: y is positive & z is negative;
then -infty*(y*z) = +infty by Def5
.= -infty*z by A6,Def5
.= (-infty*y)*z by A6,Def5;
hence thesis by A2,A4;
end;
suppose
A7: y is negative & z is positive;
then -infty*(y*z) = +infty by Def5
.= +infty*z by A7,Def5
.= (-infty*y)*z by A7,Def5;
hence thesis by A2,A4;
end;
suppose
A8: y is negative & z is negative;
then -infty*(y*z) = -infty by Def5
.= +infty*z by A8,Def5
.= (-infty*y)*z by A8,Def5;
hence thesis by A2,A4;
end;
end;
suppose
A9: x = +infty;
per cases by A3;
suppose
A10: y is positive & z is positive;
then +infty*(y*z) = +infty by Def5
.= +infty*z by A10,Def5
.= (+infty*y)*z by A10,Def5;
hence thesis by A2,A9;
end;
suppose
A11: y is positive & z is negative;
then +infty*(y*z) = -infty by Def5
.= +infty*z by A11,Def5
.= (+infty*y)*z by A11,Def5;
hence thesis by A2,A9;
end;
suppose
A12: y is negative & z is positive;
then +infty*(y*z) = -infty by Def5
.= -infty*z by A12,Def5
.= (+infty*y)*z by A12,Def5;
hence thesis by A2,A9;
end;
suppose
A13: y is negative & z is negative;
then +infty*(y*z) = +infty by Def5
.= -infty*z by A13,Def5
.= (+infty*y)*z by A13,Def5;
hence thesis by A2,A9;
end;
end;
end;
theorem Th66:
x*(y*z) = (x*y)*z
proof
per cases;
suppose
x is real & y is real & z is real;
then reconsider r=x, s=y, t=z as Real;
reconsider rs = r*s, sx = s*t as Real;
thus x*(y*z) = r*sx .= rs*t
.= (x*y)*z;
end;
suppose
x is not real or z is not real;
hence thesis by Lm22;
end;
suppose
y is not real;
hence thesis by Lm21;
end;
end;
:: for ExtReals
registration
let r be Real;
cluster r" -> real;
coherence;
end;
:: for ExtReals
registration
let r,s be Real;
cluster r*s -> real;
coherence;
cluster r/s -> real;
coherence;
end;
registration
cluster -infty" -> zero;
coherence by Def6;
cluster +infty" -> zero;
coherence by Def6;
end;
theorem :: MEMBER_1:2
(f*g)" = f"*g"
proof
per cases by XXREAL_0:14;
suppose
f in REAL & g in REAL;
then reconsider f1 = f, g1 = g as Real;
A1: (ex a being Complex st f1 = a & f" = a" )& ex b being Complex
st g1 = b & g" = b" by Def6;
then ex a,b being Complex st f" = a & g" = b & f"*g" = a * b by Def5;
then f"*g" = (f1*g1)" by A1,XCMPLX_1:204;
hence thesis;
end;
suppose
A2: f = +infty;
g is positive or g is negative or g = 0;
then (f*g)" = +infty" or (f*g)" = -infty" or (f*g)" = 0" by A2,Def5;
hence thesis by A2;
end;
suppose
A3: f = -infty;
g is positive or g is negative or g = 0;
then (f*g)" = +infty" or (f*g)" = -infty" or (f*g)" = 0" by A3,Def5;
hence thesis by A3;
end;
suppose
A4: g = +infty;
f is positive or f is negative or f = 0;
then (f*g)" = +infty" or (f*g)" = -infty" or (f*g)" = 0" by A4,Def5;
hence thesis by A4;
end;
suppose
A5: g = -infty;
f is positive or f is negative or f = 0;
then (f*g)" = +infty" or (f*g)" = -infty" or (f*g)" = 0" by A5,Def5;
hence thesis by A5;
end;
end;
theorem :: MEMBER_1:6
r <> 0 & r*f = r*g implies f = g
proof
assume that
A1: r <> 0 and
A2: r*f = r*g;
A3: r is positive or r is negative by A1;
per cases by XXREAL_0:14;
suppose
A4: f in REAL;
now
assume not g in REAL;
then g = +infty or g = -infty by XXREAL_0:14;
hence contradiction by A2,A3,A4,Def5;
end;
then
A5: ex c, d being Complex st r = c & g = d & r*g = c*d by Def5;
ex a, b being Complex st r = a & f = b & r*f = a *b by A4,Def5;
hence thesis by A1,A2,A5,XCMPLX_1:5;
end;
suppose
A6: f = +infty;
assume f <> g;
then g in REAL or g = -infty by A6,XXREAL_0:14;
hence thesis by A2,A3,A6,Def5;
end;
suppose
A7: f = -infty;
assume f <> g;
then g in REAL or g = +infty by A7,XXREAL_0:14;
hence thesis by A2,A3,A7,Def5;
end;
end;
theorem Th69:
x <> +infty & x <> -infty & x * y = +infty implies y = +infty or y = -infty
proof
assume that
A1: x <> +infty & x <> -infty and
A2: x * y = +infty;
assume y <> +infty & y <> -infty;
then
A3: y in REAL by XXREAL_0:14;
x in REAL by A1,XXREAL_0:14;
then reconsider a=x, b=y as Real by A3;
x * y = a * b;
hence contradiction by A2;
end;
theorem Th70:
x <> +infty & x <> -infty & x * y = -infty implies y = +infty or y = -infty
proof
assume that
A1: x <> +infty & x <> -infty and
A2: x * y = -infty;
assume y <> +infty & y <> -infty;
then
A3: y in REAL by XXREAL_0:14;
x in REAL by A1,XXREAL_0:14;
then reconsider a=x, b=y as Real by A3;
x * y = a * b;
hence contradiction by A2;
end;
Lm23: x*y in REAL implies x in REAL & y in REAL or x*y = 0
proof
assume
A1: x*y in REAL;
assume not x in REAL or not y in REAL;
then
A2: x is not real or y is not real by XREAL_0:def 1;
assume
A3: x*y <> 0;
per cases by A3;
suppose
x is positive & y is positive or x is negative & y is negative;
hence contradiction by A1,A2,Def5;
end;
suppose
x is positive & y is negative or x is negative & y is positive;
hence contradiction by A1,A2,Def5;
end;
end;
theorem Th71:
x <= y & 0 <= z implies x*z <= y*z
proof
assume that
A1: x <= y and
A2: 0 <= z;
per cases by A2;
suppose
z = 0;
hence thesis;
end;
suppose
A3: z > 0;
per cases;
suppose
A4: x = 0;
then z*y >= 0 by A1,A2;
hence thesis by A4;
end;
suppose
A5: x <> 0;
per cases;
case that
A6: x*z in REAL & y*z in REAL;
y*z = 0 implies y = 0 by A3;
then reconsider x,y,z as Element of REAL by A3,A5,A6,Lm23;
reconsider p = x*z, q = y*z as Element of REAL by XREAL_0:def 1;
take p, q;
thus thesis by A1,A2,XREAL_1:64;
end;
case
A7: not x*z in REAL or not y*z in REAL;
per cases by A7;
suppose
A8: not x*z in REAL;
per cases by A8,XXREAL_0:14;
suppose
x*z = -infty;
hence thesis;
end;
suppose
x*z = +infty;
then
A9: x <> -infty by A3;
A10: not x in REAL or not y in REAL or not z in REAL by A8,XREAL_0:def 1
;
per cases by A9,A10,XXREAL_0:14;
suppose
y = +infty;
hence thesis by A3,Def5;
end;
suppose
x = +infty;
then y = +infty by A1,XXREAL_0:4;
hence thesis by A3,Def5;
end;
suppose
y = -infty;
then x = -infty by A1,XXREAL_0:6;
hence thesis by A3,Def5;
end;
suppose that
A11: not z in REAL and
x in REAL & y in REAL;
A12: z = +infty by A3,A11,XXREAL_0:14;
per cases by A5;
suppose x < 0;
hence thesis by A12,Def5;
end;
suppose 0 < x;
then 0 < y by A1;
hence thesis by A12,Def5;
end;
end;
end;
end;
suppose
not y*z in REAL;
then
A13: not x in REAL or not y in REAL or not z in REAL by XREAL_0:def 1;
per cases by A13,XXREAL_0:14;
suppose
x = -infty;
hence thesis by A3,Def5;
end;
suppose
y = +infty;
hence thesis by A3,Def5;
end;
suppose
x = +infty;
then y = +infty by A1,XXREAL_0:4;
hence thesis by A3,Def5;
end;
suppose
y = -infty;
then x = -infty by A1,XXREAL_0:6;
hence thesis by A3,Def5;
end;
suppose that
A14: not z in REAL and
x in REAL & y in REAL;
A15: z = +infty by A3,A14,XXREAL_0:14;
per cases by A5;
suppose x < 0;
hence thesis by A15,Def5;
end;
suppose 0 < x;
then 0 < y by A1;
hence thesis by A15,Def5;
end;
end;
end;
end;
end;
end;
end;
theorem Th72:
x < y & 0 < z & z <> +infty implies x*z < y*z
proof
assume that
A1: x < y and
A2: 0 < z and
A3: z <> +infty;
A4: now
A5: x <> +infty & y <> -infty by A1,XXREAL_0:3,5;
assume
A6: x*z = y*z;
per cases by A5,XXREAL_0:14;
suppose
A7: x in REAL & y in REAL;
z in REAL by A2,A3,XXREAL_0:14;
then reconsider x,y,z as Real by A7;
x*z < y*z by A1,A2,XREAL_1:68;
hence contradiction by A6;
end;
suppose
A8: y = +infty;
then y*z = +infty by A2,Def5;
then x = +infty or x = -infty by A2,A3,A6,Th69;
hence contradiction by A1,A2,A6,A8;
end;
suppose
A9: x = -infty;
then x*z = -infty by A2,Def5;
then y = +infty or y = -infty by A2,A3,A6,Th70;
hence contradiction by A1,A2,A6,A9;
end;
end;
x*z <= y*z by A1,A2,Th71;
hence thesis by A4,XXREAL_0:1;
end;
theorem
x*y in REAL implies x in REAL & y in REAL or x*y = 0 by Lm23;
theorem
+infty" = 0;
theorem
-infty" = 0;
theorem
x/+infty = 0;
theorem
x/-infty = 0;
theorem Th78:
x <> -infty & x <> +infty & x <> 0 implies x / x = 1
proof
assume x <> -infty & x <> +infty;
then x in REAL by XXREAL_0:14;
then reconsider a=x as Real;
assume x <> 0;
then a/a =1 by XCMPLX_1:60;
hence thesis;
end;
theorem
x <= y & 0 < z implies x/z <= y/z by Th71;
theorem
x < y & 0 < z & z <> +infty implies x/z < y/z
proof
assume that
A1: x < y and
A2: 0 < z and
A3: z <> +infty;
per cases by A3,XXREAL_0:14;
suppose
z = -infty;
hence thesis by A2;
end;
suppose
z in REAL;
then reconsider z as Real;
z" > 0 by A2;
hence thesis by A1,Th72;
end;
end;
theorem Th81:
1*x = x
proof
per cases by XXREAL_0:14;
suppose
x in REAL;
then reconsider x, y=1 as Real;
y*x = x;
hence thesis;
end;
suppose
x = -infty or x = +infty;
hence thesis by Def5;
end;
end;
theorem Th82:
y" = 0 implies y = +infty or y = -infty or y = 0
proof
assume
A1: y" = 0;
assume y <> +infty & y <> -infty;
then y in REAL by XXREAL_0:14;
then reconsider y as Real;
y"" = 0 by A1;
hence thesis;
end;
theorem Th83:
0 < y & y <> +infty implies +infty / y = +infty
proof
assume that
A1: 0<y and
A2: y<>+infty;
y" <> 0 by A1,A2,Th82;
hence thesis by A1,Def5;
end;
theorem Th84:
y < 0 & -infty <> y implies -infty / y = +infty
proof
assume that
A1: y<0 and
A2: -infty<>y;
y" <> 0 by A1,A2,Th82;
hence thesis by A1,Def5;
end;
theorem Th85:
y < 0 & -infty <> y implies +infty / y = -infty
proof
assume that
A1: y<0 and
A2: -infty<>y;
y" <> 0 by A1,A2,Th82;
hence thesis by A1,Def5;
end;
theorem Th86:
0 < y & y <> +infty implies -infty / y = -infty
proof
assume that
A1: 0<y and
A2: y<>+infty;
y" <> 0 by A1,A2,Th82;
hence thesis by A1,Def5;
end;
theorem :: extension of REAL_1:34
x <> +infty & x <> -infty & x <> 0 implies x*(1/x) = 1 & (1/x)*x = 1
proof
assume that
A1: x <> +infty & x <> -infty and
A2: x <> 0;
x in REAL by A1,XXREAL_0:14;
then reconsider a = x as Real;
x * (1 / x) = a * (1/a) .= 1 by A2,XCMPLX_1:106;
hence thesis;
end;
theorem
-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 Element of REAL by A1,A2,XXREAL_0:14;
A4: x * y / y = x
proof
per cases;
suppose
A5: x = +infty;
per cases by A3;
suppose
A6: 0 < y;
then x * y = +infty by A5,Def5;
hence thesis by A2,A5,A6,Th83;
end;
suppose
A7: y < 0;
then x * y = -infty by A5,Def5;
hence thesis by A1,A5,A7,Th84;
end;
end;
suppose
A8: x = -infty;
per cases by A3;
suppose
A9: 0 <y;
then x * y = -infty by A8,Def5;
hence thesis by A2,A8,A9,Th86;
end;
suppose
A10: y < 0;
then x * y = +infty by A8,Def5;
hence thesis by A1,A8,A10,Th85;
end;
end;
suppose
x <> +infty & x <> -infty;
then x in REAL by XXREAL_0:14;
then reconsider a = x as Real;
(x * y)/y = (a * b)/b .= a by A3,XCMPLX_1:89;
hence thesis;
end;
end;
y / y = 1 by A1,A2,A3,Th78;
hence thesis by A4,Th81;
end;
theorem
+infty * y <> 1 & -infty * y <> 1
proof
y = 0 or 0 < y or y < 0;
hence thesis by Def5;
end;
theorem
x * y <> +infty & x * y <> -infty implies x in REAL or y in REAL
proof
assume that
A1: x * y <> +infty and
A2: x * y <> -infty;
assume
A3: ( not x in REAL)& not y in REAL;
per cases by A3,XXREAL_0:14;
suppose
x = +infty & y = +infty;
hence contradiction by A1,Def5;
end;
suppose
x = +infty & y = -infty;
hence contradiction by A2,Def5;
end;
suppose
x = -infty & y = +infty;
hence contradiction by A2,Def5;
end;
suppose
x = -infty & y = -infty;
hence contradiction by A1,Def5;
end;
end;
begin :: distributivity
theorem Th91:
(-1)*x = -x
proof
per cases by XXREAL_0:14;
suppose
x in REAL;
then reconsider x, y=-1 as Real;
y*x = -x;
hence thesis;
end;
suppose
A1: x = -infty;
hence (-1)*x = +infty by Def5
.= -x by A1,Def3;
end;
suppose
A2: x = +infty;
hence (-1)*x = -infty by Def5
.= -x by A2,Def3;
end;
end;
theorem Th92:
- x*y = (-x)*y
proof
thus - x*y = (-1)*(x*y) by Th91
.= (-1)*x*y by Th66
.= (-x)*y by Th91;
end;
theorem Th93:
y = -z implies x*(y+z) = x*y +x*z
proof
assume
A1: y = -z;
hence x*(y+z) = x*0 by Th7
.= x*y - x*y by Th7
.= x*y + x*(-y) by Th92
.= x*y + x*z by A1;
end;
theorem Th94:
2*x = x+x
proof
per cases by XXREAL_0:14;
suppose
x in REAL;
then reconsider x as Real;
2*x = x+x;
hence thesis;
end;
suppose
A1: x = -infty;
hence 2*x = -infty by Def5
.= x+x by A1,Def2;
end;
suppose
A2: x = +infty;
hence 2*x = +infty by Def5
.= x+x by A2,Def2;
end;
end;
Lm24: x*(y+y) = x*y+x*y
proof
thus x*(y+y) = x*(2*y) by Th94
.= 2*(x*y) by Th66
.= x*y+x*y by Th94;
end;
Lm25: x*(0+z) = x*0 +x*z
proof
thus x*(0+z) = x*z by Th4
.= x*0 +x*z by Th4;
end;
Lm26: 0*(y+z) = 0*y +0*z;
Lm27: x is real & y is real implies x*(y+z) = x*y +x*z
proof
assume that
A1: x is real and
A2: y is real;
reconsider r=x, s=y as Real by A1,A2;
A3: x*y = r*s;
per cases by XXREAL_0:14;
suppose
z in REAL;
then reconsider t=z as Real;
reconsider u=s+t, v=r*s, w=r*t as Real;
r*u = v + w;
hence thesis;
end;
suppose
A4: z = -infty;
then
A5: y+z = -infty by A2,Def2;
per cases;
suppose x is zero;
then x = 0;
hence thesis by Lm26;
end;
suppose
A6: x is positive;
hence x*(y+z) = -infty by A5,Def5
.= x*y + -infty by A3,Def2
.= x*y +x*z by A4,A6,Def5;
end;
suppose
A7: x is negative;
hence x*(y+z) = +infty by A5,Def5
.= x*y + +infty by A3,Def2
.= x*y +x*z by A4,A7,Def5;
end;
end;
suppose
A8: z = +infty;
then
A9: y+z = +infty by A2,Def2;
per cases;
suppose x is zero;
then x = 0;
hence thesis by Lm26;
end;
suppose
A10: x is positive;
hence x*(y+z) = +infty by A9,Def5
.= x*y + +infty by A3,Def2
.= x*y +x*z by A8,A10,Def5;
end;
suppose
A11: x is negative;
hence x*(y+z) = -infty by A9,Def5
.= x*y + -infty by A3,Def2
.= x*y +x*z by A8,A11,Def5;
end;
end;
end;
Lm28: x is real & y is not real implies x*(y+z) = x*y +x*z
proof
assume that
A1: x is real and
A2: y is not real;
per cases;
suppose
z is real;
hence thesis by A1,Lm27;
end;
suppose
z is not real;
then
A3: not z in REAL;
A4: not y in REAL by A2;
per cases by A4,A3,XXREAL_0:14;
suppose
y = -infty & z = -infty;
hence thesis by Lm24;
end;
suppose
y = -infty & z = +infty;
hence thesis by Th5,Th93;
end;
suppose
y = +infty & z = -infty;
hence thesis by Th6,Th93;
end;
suppose
y = +infty & z = +infty;
hence thesis by Lm24;
end;
end;
end;
theorem Th95:
x is real implies x*(y+z) = x*y +x*z
proof
assume
A1: x is real;
per cases;
suppose
y is real & z is real;
hence thesis by A1,Lm27;
end;
suppose
y is not real or z is not real;
hence thesis by A1,Lm28;
end;
end;
theorem Th96:
y>=0 & z>=0 implies x*(y+z) = x*y +x*z
proof
assume
A1: y>=0 & z>=0;
per cases by A1;
suppose
y = 0 or z = 0;
hence thesis by Lm25;
end;
suppose
A2: y>0 & z>0;
per cases;
suppose
x is real;
hence thesis by Th95;
end;
suppose
x is not real;
then
A3: not x in REAL;
per cases by A3,XXREAL_0:14;
suppose
A4: x = -infty;
hence x*(y+z) = -infty by A2,Def5
.= -infty + x*z by A2,A4,Def2
.= x*y + x*z by A2,A4,Def5;
end;
suppose
A5: x = +infty;
hence x*(y+z) = +infty by A2,Def5
.= +infty + x*z by A2,A5,Def2
.= x*y + x*z by A2,A5,Def5;
end;
end;
end;
end;
theorem
y<=0 & z<=0 implies x*(y+z) = x*y +x*z
proof
assume
A1: y<=0 & z<=0;
thus x*(y+z) = --(x*(y+z)) .= -(x*-(y+z)) by Th92
.= -(x*(-y+-z)) by Th9
.= -(x*(-y)+x*(-z)) by A1,Th96
.= -(-x*y+x*(-z)) by Th92
.= -(-x*y+-x*z) by Th92
.= --(x*y +x*z) by Th9
.= x*y +x*z;
end;
theorem
x*(0+z) = x*0 +x*z by Lm25;
theorem :: MEMBER_1:1
(-f)" = -f"
proof
per cases by XXREAL_0:14;
suppose
A1: f in REAL;
then reconsider g = f as Real;
A2: -f = -g;
consider a being Complex such that
A3: f = a and
A4: f" = a" by A1,Def6;
A5: (-a)" = -a" by XCMPLX_1:222;
ex m being Complex st -f = m & -f" = m"
proof
take -a;
thus -f = -a by A3,A2;
thus thesis by A4,A5,A2,Def3;
end;
hence thesis by A2,Def6;
end;
suppose
A6: f = +infty;
hence (-f)" = (-infty)" by Def3
.= -f" by A6;
end;
suppose
A7: f = -infty;
hence (-f)" = (+infty)" by Def3
.= -f" by A7;
end;
end;
theorem
x is real implies x * (y - z) = x * y - x * z
proof
assume x is real;
then x * (y - z) = x * y + x * (-z) by Th95
.= x * y + -(x * z) by Th92;
hence thesis;
end;
theorem Th101:
x <= y & z <= 0 implies y*z <= x*z
proof
assume x <= y & z <= 0;
then
A1: x*(-z) <= y*(-z) by Th71;
-x*z = x*(-z) & -y*z = y*(-z) by Th92;
hence thesis by A1,Th38;
end;
theorem Th102:
x < y & z < 0 & z <> -infty implies y*z < x*z
proof
assume x < y & z < 0 & z <> -infty;
then
A1: x*(-z) < y*(-z) by Th5,Th10,Th72;
-x*z = x*(-z) & -y*z = y*(-z) by Th92;
hence thesis by A1,Th38;
end;
theorem
x <= y & z < 0 implies y/z <= x/z by Th101;
theorem
x < y & z < 0 & z <> -infty implies y/z < x/z
proof
assume that
A1: x < y and
A2: 0 > z and
A3: z <> -infty;
per cases by A3,XXREAL_0:14;
suppose
z = +infty;
hence thesis by A2;
end;
suppose
z in REAL;
then reconsider z as Real;
z" < 0 by A2;
hence thesis by A1,Th102;
end;
end;
theorem
x/2 + x/2 = x
proof
x/2 + x/2 = (x+x)/2 by Th95
.= 2*x/2 by Th94
.= x*(2/2) by Th66
.= x by Th81;
hence thesis;
end;
registration let x,y be Nat;
cluster x+y -> natural;
coherence;
cluster x*y -> natural;
coherence;
end;
registration
cluster -1 -> dim-like;
coherence;
let n be dim-like number;
cluster n+1 -> natural;
coherence;
end;
definition
let x be Element of ExtREAL;
redefine func -x -> Element of ExtREAL; :: redefines - (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
redefine func x" -> Element of ExtREAL; :: redefines " (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
let y be Element of ExtREAL;
redefine func x + y -> Element of ExtREAL; :: redefines + (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
redefine func x - y -> Element of ExtREAL; :: redefines - (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
redefine func x * y -> Element of ExtREAL; :: redefines * (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
redefine func x / y -> Element of ExtREAL; :: redefines / (XXREAL_3, definition)
coherence by XXREAL_0:def 1;
end;