:: Basic Operations on Extended Real Numbers
:: by Andrzej Trybulec
::
:: Received September 23, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

definition
let x, y be ext-real number ;
redefine pred x <= y means :Def1: :: XXREAL_3:def 1
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
verum
;
compatibility
( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st
( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) )
proof end;
end;

:: deftheorem Def1 defines <= XXREAL_3:def 1 :
for x, y being ext-real number holds
( ( x in REAL & y in REAL implies ( x <= y iff ex p, q being Element of REAL st
( p = x & q = y & p <= q ) ) ) & ( ( not x in REAL or not y in REAL ) implies ( x <= y iff ( x = -infty or y = +infty ) ) ) );

registration
cluster ext-real positive non real for set ;
existence
ex b1 being ext-real number st
( not b1 is real & b1 is positive )
proof end;
cluster ext-real negative non real for set ;
existence
ex b1 being ext-real number st
( not b1 is real & b1 is negative )
proof end;
end;

theorem Th1: :: XXREAL_3:1
for x being ext-real positive non real number holds x = +infty
proof end;

theorem Th2: :: XXREAL_3:2
for x being ext-real negative non real number holds x = -infty
proof end;

registration
cluster ext-real non negative non real -> ext-real positive for set ;
coherence
for b1 being ext-real number st not b1 is real & not b1 is negative holds
b1 is positive
;
cluster ext-real non positive non real -> ext-real negative for set ;
coherence
for b1 being ext-real number st not b1 is real & not b1 is positive holds
b1 is negative
;
end;

theorem Th3: :: XXREAL_3:3
for x, z being ext-real number st x < z holds
ex y being real number st
( x < y & y < z )
proof end;

begin

definition
let x, y be ext-real number ;
func x + y -> ext-real number means :Def2: :: XXREAL_3:def 2
ex a, b being complex number 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
( ( x is real & y is real implies ex b1 being ext-real number ex a, b being complex number st
( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ex b1 being ext-real number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b1 = a + b ) & ex a, b being complex number st
( x = a & y = b & b2 = a + b ) implies b1 = b2 ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or not b1 = 0 or not b2 = 0 or b1 = b2 ) )
;
consistency
for b1 being ext-real number holds
( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a + b ) iff b1 = +infty ) ) & ( x is real & y is real & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a + b ) iff b1 = -infty ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) & ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b1 = +infty iff b1 = -infty ) ) )
;
commutativity
for b1, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st
( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies b1 = -infty ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or b1 = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b1 = a + b ) ) & ( ( ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) ) implies b1 = +infty ) & ( ( ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) ) implies b1 = -infty ) & ( ( y is real & x is real ) or ( y = +infty & x <> -infty ) or ( x = +infty & y <> -infty ) or ( y = -infty & x <> +infty ) or ( x = -infty & y <> +infty ) or b1 = 0 ) )
;
end;

:: deftheorem Def2 defines + XXREAL_3:def 2 :
for x, y, b3 being ext-real number holds
( ( x is real & y is real implies ( b3 = x + y iff ex a, b being complex number st
( x = a & y = b & b3 = a + b ) ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( b3 = x + y iff b3 = +infty ) ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ( b3 = x + y iff b3 = -infty ) ) & ( ( x is real & y is real ) or ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) or ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) or ( b3 = x + y iff b3 = 0 ) ) );

definition
let x be ext-real number ;
func - x -> ext-real number means :Def3: :: XXREAL_3:def 3
ex a being complex number st
( x = a & it = - a ) if x is real
it = -infty if x = +infty
otherwise it = +infty ;
existence
( ( x is real implies ex b1 being ext-real number ex a being complex number st
( x = a & b1 = - a ) ) & ( x = +infty implies ex b1 being ext-real number st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ext-real number st b1 = +infty ) )
proof end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b1 = - a ) & ex a being complex number st
( x = a & b2 = - a ) implies b1 = b2 ) & ( x = +infty & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( not x is real & not x = +infty & b1 = +infty & b2 = +infty implies b1 = b2 ) )
;
consistency
for b1 being ext-real number st x is real & x = +infty holds
( ex a being complex number st
( x = a & b1 = - a ) iff b1 = -infty )
;
involutiveness
for b1, b2 being ext-real number st ( b2 is real implies ex a being complex number st
( b2 = a & b1 = - a ) ) & ( b2 = +infty implies b1 = -infty ) & ( not b2 is real & not b2 = +infty implies b1 = +infty ) holds
( ( b1 is real implies ex a being complex number st
( b1 = a & b2 = - a ) ) & ( b1 = +infty implies b2 = -infty ) & ( not b1 is real & not b1 = +infty implies b2 = +infty ) )
proof end;
end;

:: deftheorem Def3 defines - XXREAL_3:def 3 :
for x, b2 being ext-real number holds
( ( x is real implies ( b2 = - x iff ex a being complex number st
( x = a & b2 = - a ) ) ) & ( x = +infty implies ( b2 = - x iff b2 = -infty ) ) & ( not x is real & not x = +infty implies ( b2 = - x iff b2 = +infty ) ) );

definition
let x, y be ext-real number ;
func x - y -> ext-real number equals :: XXREAL_3:def 4
x + (- y);
coherence
x + (- y) is ext-real number
;
end;

:: deftheorem defines - XXREAL_3:def 4 :
for x, y being ext-real number holds x - y = x + (- y);

registration
let x, y be real number ;
let a, b be complex number ;
identify x + y with a + b when x = a, y = b;
compatibility
( x = a & y = b implies x + y = a + b )
by Def2;
end;

registration
let x be real number ;
let a be complex number ;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )
by Def3;
end;

:: for ext-real numbers
registration
let r be real number ;
cluster - r -> ext-real real ;
coherence
- r is real
;
end;

:: for ext-real numbers
registration
let r, s be real number ;
cluster r + s -> ext-real real ;
coherence
r + s is real
;
cluster r - s -> ext-real real ;
coherence
r - s is real
;
end;

registration
let x be real number ;
let y be ext-real non real number ;
cluster x + y -> non real for number ;
coherence
for b1 being number st b1 = x + y holds
not b1 is real
proof end;
end;

registration
let x, y be ext-real positive non real number ;
cluster x + y -> ext-real non real ;
coherence
not x + y is real
proof end;
end;

registration
let x, y be ext-real negative non real number ;
cluster x + y -> ext-real non real ;
coherence
not x + y is real
proof end;
end;

registration
let x be ext-real negative non real number ;
let y be ext-real positive non real number ;
cluster x + y -> zero ext-real ;
coherence
x + y is zero
proof end;
end;

registration
let x, y be real number ;
let a, b be complex number ;
identify x - y with a - b when x = a, y = b;
compatibility
( x = a & y = b implies x - y = a - b )
;
end;

theorem Th4: :: XXREAL_3:4
for x being ext-real number holds x + 0 = x
proof end;

theorem Th5: :: XXREAL_3:5
- -infty = +infty by Def3;

theorem Th6: :: XXREAL_3:6
- +infty = -infty by Def3;

Lm1: +infty + +infty = +infty
by Def2;

Lm2: -infty + -infty = -infty
by Def2;

theorem Th7: :: XXREAL_3:7
for x being ext-real number holds x + (- x) = 0
proof end;

theorem :: XXREAL_3:8
for x, y being ext-real number st x + y = 0 holds
x = - y
proof end;

Lm3: for x being ext-real number holds
( - x in REAL iff x in REAL )

proof end;

Lm4: - (+infty + -infty) = +infty - +infty by Def3
.= (- -infty) - +infty by Def3 ;

Lm5: - +infty = -infty
by Def3;

Lm6: for x being ext-real number st x in REAL holds
- (x + +infty) = (- +infty) + (- x)

proof end;

Lm7: for x being ext-real number st x in REAL holds
- (x + -infty) = (- -infty) + (- x)

proof end;

theorem Th9: :: XXREAL_3:9
for x, y being ext-real number holds - (x + y) = (- x) + (- y)
proof end;

theorem Th10: :: XXREAL_3:10
for f, g being ext-real number st - f = - g holds
f = g
proof end;

Lm8: for x, y being ext-real number holds
( not x + y = +infty or x = +infty or y = +infty )

proof end;

Lm9: for x, y being ext-real number holds
( not x + y = -infty or x = -infty or y = -infty )

proof end;

theorem Th11: :: XXREAL_3:11
for r being real number
for f, g being ext-real number st r + f = r + g holds
f = g
proof end;

theorem :: XXREAL_3:12
for r being real number
for f, g being ext-real number st r - f = r - g holds
f = g
proof end;

theorem Th13: :: XXREAL_3:13
for x being ext-real number st x <> +infty holds
( +infty - x = +infty & x - +infty = -infty )
proof end;

theorem Th14: :: XXREAL_3:14
for x being ext-real number st x <> -infty holds
( -infty - x = -infty & x - -infty = +infty )
proof end;

theorem Th15: :: XXREAL_3:15
for x being ext-real number holds x - 0 = x
proof end;

theorem :: XXREAL_3:16
for x, y being ext-real number holds
( not x + y = +infty or x = +infty or y = +infty ) by Lm8;

theorem :: XXREAL_3:17
for x, y being ext-real number holds
( not x + y = -infty or x = -infty or y = -infty ) by Lm9;

theorem Th18: :: XXREAL_3:18
for x, y being ext-real number holds
( not x - y = +infty or x = +infty or y = -infty )
proof end;

theorem Th19: :: XXREAL_3:19
for x, y being ext-real number holds
( not x - y = -infty or x = -infty or y = +infty )
proof end;

theorem Th20: :: XXREAL_3:20
for x, y being ext-real number holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y in REAL or ( x in REAL & y in REAL ) )
proof end;

theorem Th21: :: XXREAL_3:21
for x, y being ext-real number holds
( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y in REAL or ( x in REAL & y in REAL ) )
proof end;

theorem Th22: :: XXREAL_3:22
for x, y being ext-real number st x is real holds
( (y - x) + x = y & (y + x) - x = y )
proof end;

theorem Th23: :: XXREAL_3:23
for x being ext-real number holds
( ( x = +infty implies - x = -infty ) & ( - x = -infty implies x = +infty ) & ( x = -infty implies - x = +infty ) & ( - x = +infty implies x = -infty ) )
proof end;

theorem :: XXREAL_3:24
for z, x being ext-real number st z is real holds
x = (x + z) - z
proof end;

Lm10: - +infty = -infty
by Def3;

Lm11: for x being ext-real number st x in REAL holds
- (x + -infty) = (- -infty) + (- x)

proof end;

theorem Th25: :: XXREAL_3:25
for x, y being ext-real number holds - (x + y) = (- y) - x
proof end;

theorem :: XXREAL_3:26
for x, y being ext-real number holds
( - (x - y) = (- x) + y & - (x - y) = y - x )
proof end;

theorem Th27: :: XXREAL_3:27
for x, y being ext-real number holds
( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) )
proof end;

theorem :: XXREAL_3:28
for y, z being ext-real number st 0 <= y & y < +infty holds
z = (z + y) - y
proof end;

theorem Th29: :: XXREAL_3:29
for x, y, z being ext-real number st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & not ( y = +infty & z = -infty ) & not ( y = -infty & z = +infty ) & not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) holds
(x + y) + z = x + (y + z)
proof end;

theorem Th30: :: XXREAL_3:30
for x, y, z being ext-real number st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds
(x + y) - z = x + (y - z)
proof end;

theorem :: XXREAL_3:31
for x, y, z being ext-real number st ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = -infty ) & ( not y = -infty or not z = +infty ) & ( not x = +infty or not z = +infty ) & ( not x = -infty or not z = -infty ) holds
(x - y) - z = x - (y + z)
proof end;

theorem Th32: :: XXREAL_3:32
for x, y, z being ext-real number st ( not x = +infty or not y = +infty ) & ( not x = -infty or not y = -infty ) & ( not y = +infty or not z = +infty ) & ( not y = -infty or not z = -infty ) & ( not x = +infty or not z = -infty ) & ( not x = -infty or not z = +infty ) holds
(x - y) + z = x - (y - z)
proof end;

theorem Th33: :: XXREAL_3:33
for z, x, y being ext-real number st z is real holds
(z + x) - (z + y) = x - y
proof end;

theorem :: XXREAL_3:34
for y, z, x being ext-real number st y is real holds
(z - y) + (y - x) = z - x
proof end;

begin

Lm12: for x, y, z being ext-real number st x <= y holds
x + z <= y + z

proof end;

Lm13: for x, y being ext-real number st x >= 0 & y > 0 holds
x + y > 0

proof end;

Lm14: for x, y being ext-real number st x <= 0 & y < 0 holds
x + y < 0

proof end;

registration
let x, y be ext-real non negative number ;
cluster x + y -> ext-real non negative ;
coherence
not x + y is negative
proof end;
end;

registration
let x, y be ext-real non positive number ;
cluster x + y -> ext-real non positive ;
coherence
not x + y is positive
proof end;
end;

registration
let x be ext-real positive number ;
let y be ext-real non negative number ;
cluster x + y -> ext-real positive ;
coherence
x + y is positive
by Lm13;
cluster y + x -> ext-real positive ;
coherence
y + x is positive
;
end;

registration
let x be ext-real negative number ;
let y be ext-real non positive number ;
cluster x + y -> ext-real negative ;
coherence
x + y is negative
by Lm14;
cluster y + x -> ext-real negative ;
coherence
y + x is negative
;
end;

registration
let x be ext-real non positive number ;
cluster - x -> ext-real non negative ;
coherence
not - x is negative
proof end;
end;

registration
let x be ext-real non negative number ;
cluster - x -> ext-real non positive ;
coherence
not - x is positive
proof end;
end;

registration
let x be ext-real positive number ;
cluster - x -> ext-real negative ;
coherence
- x is negative
proof end;
end;

registration
let x be ext-real negative number ;
cluster - x -> ext-real positive ;
coherence
- x is positive
proof end;
end;

registration
let x be ext-real non negative number ;
let y be ext-real non positive number ;
cluster x - y -> ext-real non negative ;
coherence
not x - y is negative
;
cluster y - x -> ext-real non positive ;
coherence
not y - x is positive
;
end;

registration
let x be ext-real positive number ;
let y be ext-real non positive number ;
cluster x - y -> ext-real positive ;
coherence
x - y is positive
;
cluster y - x -> ext-real negative ;
coherence
y - x is negative
;
end;

registration
let x be ext-real negative number ;
let y be ext-real non negative number ;
cluster x - y -> ext-real negative ;
coherence
x - y is negative
;
cluster y - x -> ext-real positive ;
coherence
y - x is positive
;
end;

Lm15: for x, y being ext-real number st x <= y holds
- y <= - x

proof end;

theorem :: XXREAL_3:35
for x, y, z being ext-real number st x <= y holds
x + z <= y + z by Lm12;

theorem Th36: :: XXREAL_3:36
for x, y, z, w being ext-real number st x <= y & z <= w holds
x + z <= y + w
proof end;

theorem Th37: :: XXREAL_3:37
for x, y, z, w being ext-real number st x <= y & z <= w holds
x - w <= y - z
proof end;

theorem Th38: :: XXREAL_3:38
for x, y being ext-real number holds
( x <= y iff - y <= - x )
proof end;

theorem Th39: :: XXREAL_3:39
for z, x being ext-real number st 0 <= z holds
x <= x + z
proof end;

theorem :: XXREAL_3:40
for x, y being ext-real number st x <= y holds
y - x >= 0
proof end;

theorem :: XXREAL_3:41
for z, y, x being ext-real number st ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z holds
x <= z + y
proof end;

theorem :: XXREAL_3:42
for x, y, z being ext-real number st ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y holds
x - y <= z
proof end;

theorem Th43: :: XXREAL_3:43
for z, x, y being ext-real number st z in REAL & x < y holds
( x + z < y + z & x - z < y - z )
proof end;

theorem :: XXREAL_3:44
for x, y, z being ext-real number st 0 <= x & 0 <= y & 0 <= z holds
(x + y) + z = x + (y + z)
proof end;

theorem Th45: :: XXREAL_3:45
for x, y, z being ext-real number st x is real holds
( y + x <= z iff y <= z - x )
proof end;

theorem Th46: :: XXREAL_3:46
for x, y being ext-real number st 0 < x & x < y holds
0 < y - x
proof end;

theorem :: XXREAL_3:47
for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds
z < y - x
proof end;

theorem :: XXREAL_3:48
for x, z, y being ext-real number st 0 <= x & 0 <= z & z + x < y holds
z <= y
proof end;

theorem Th49: :: XXREAL_3:49
for x, z being ext-real number st 0 <= x & x < z holds
ex y being real number st
( 0 < y & x + y < z )
proof end;

theorem :: XXREAL_3:50
for x being ext-real number st 0 < x holds
ex y being real number st
( 0 < y & y + y < x )
proof end;

theorem Th51: :: XXREAL_3:51
for x, y being ext-real number st x < y & x < +infty & -infty < y holds
0 < y - x
proof end;

theorem :: XXREAL_3:52
for x, y, z being ext-real number holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or not x + y < z or ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) )
proof end;

theorem :: XXREAL_3:53
for z, y, x being ext-real number holds
( ( z = +infty & y = +infty ) or ( z = -infty & y = -infty ) or not x < z - y or ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) )
proof end;

theorem :: XXREAL_3:54
for x, y, z being ext-real number holds
( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or not x - y < z or ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) )
proof end;

theorem :: XXREAL_3:55
for z, y, x being ext-real number holds
( ( z = +infty & y = -infty ) or ( z = -infty & y = +infty ) or not x < z + y or ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) )
proof end;

theorem :: XXREAL_3:56
for x, y, z being ext-real number holds
( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) )
proof end;

theorem :: XXREAL_3:57
for x, y, z being ext-real number st ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y holds
( y <> +infty & x + y <= z )
proof end;

theorem :: XXREAL_3:58
for x, y, z being ext-real number holds
( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( y = +infty & z = -infty ) or ( y = -infty & z = +infty ) or not x - y <= z or y <> -infty )
proof end;

theorem :: XXREAL_3:59
for x, y, z being ext-real number st ( not x = -infty or not y = -infty ) & ( not y = -infty or not z = +infty ) & x <= z + y holds
y <> -infty
proof end;

theorem :: XXREAL_3:60
for x, y being ext-real number holds
( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )
proof end;

theorem :: XXREAL_3:61
for x, y being ext-real number st ( for e being real number st 0 < e holds
x < y + e ) holds
x <= y
proof end;

theorem :: XXREAL_3:62
for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds
x + t < y + t
proof end;

theorem :: XXREAL_3:63
for x, y, t being ext-real number st t <> -infty & t <> +infty & x < y holds
x - t < y - t
proof end;

theorem :: XXREAL_3:64
for x, y, w, z being ext-real number st x < y & w < z holds
x + w < y + z
proof end;

theorem :: XXREAL_3:65
for x, z, y being ext-real number st 0 <= x & z + x <= y holds
z <= y
proof end;

begin

definition
let x, y be ext-real number ;
func x * y -> ext-real number means :Def5: :: XXREAL_3:def 5
ex a, b being complex number st
( x = a & y = b & it = a * b ) if ( x is real & y is real )
it = +infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) )
it = -infty if ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) )
otherwise it = 0 ;
existence
( ( x is real & y is real implies ex b1 being ext-real number ex a, b being complex number st
( x = a & y = b & b1 = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ex b1 being ext-real number st b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ex b1 being ext-real number st b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ex b1 being ext-real number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & y is real & ex a, b being complex number st
( x = a & y = b & b1 = a * b ) & ex a, b being complex number st
( x = a & y = b & b2 = a * b ) implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & b1 = +infty & b2 = +infty implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) & b1 = -infty & b2 = -infty implies b1 = b2 ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
;
consistency
for b1 being ext-real number holds
( ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a * b ) iff b1 = +infty ) ) & ( x is real & y is real & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( ex a, b being complex number st
( x = a & y = b & b1 = a * b ) iff b1 = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) & ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b1 = +infty iff b1 = -infty ) ) )
;
commutativity
for b1, x, y being ext-real number st ( x is real & y is real implies ex a, b being complex number st
( x = a & y = b & b1 = a * b ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies b1 = +infty ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies b1 = -infty ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies b1 = 0 ) holds
( ( y is real & x is real implies ex a, b being complex number st
( y = a & x = b & b1 = a * b ) ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is positive ) or ( y is negative & x is negative ) ) implies b1 = +infty ) & ( ( not y is real or not x is real ) & ( ( y is positive & x is negative ) or ( y is negative & x is positive ) ) implies b1 = -infty ) & ( ( not y is real or not x is real ) & ( ( y is real & x is real ) or ( not ( y is positive & x is positive ) & not ( y is negative & x is negative ) ) ) & ( ( y is real & x is real ) or ( not ( y is positive & x is negative ) & not ( y is negative & x is positive ) ) ) implies b1 = 0 ) )
;
end;

:: deftheorem Def5 defines * XXREAL_3:def 5 :
for x, y, b3 being ext-real number holds
( ( x is real & y is real implies ( b3 = x * y iff ex a, b being complex number st
( x = a & y = b & b3 = a * b ) ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is positive ) or ( x is negative & y is negative ) ) implies ( b3 = x * y iff b3 = +infty ) ) & ( ( not x is real or not y is real ) & ( ( x is positive & y is negative ) or ( x is negative & y is positive ) ) implies ( b3 = x * y iff b3 = -infty ) ) & ( ( not x is real or not y is real ) & ( ( x is real & y is real ) or ( not ( x is positive & y is positive ) & not ( x is negative & y is negative ) ) ) & ( ( x is real & y is real ) or ( not ( x is positive & y is negative ) & not ( x is negative & y is positive ) ) ) implies ( b3 = x * y iff b3 = 0 ) ) );

registration
let x, y be real number ;
let a, b be complex number ;
identify x * y with a * b when x = a, y = b;
compatibility
( x = a & y = b implies x * y = a * b )
by Def5;
end;

definition
let x be ext-real number ;
func x " -> ext-real number means :Def6: :: XXREAL_3:def 6
ex a being complex number st
( x = a & it = a " ) if x is real
otherwise it = 0 ;
existence
( ( x is real implies ex b1 being ext-real number ex a being complex number st
( x = a & b1 = a " ) ) & ( not x is real implies ex b1 being ext-real number st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ext-real number holds
( ( x is real & ex a being complex number st
( x = a & b1 = a " ) & ex a being complex number st
( x = a & b2 = a " ) implies b1 = b2 ) & ( not x is real & b1 = 0 & b2 = 0 implies b1 = b2 ) )
;
consistency
for b1 being ext-real number holds verum
;
end;

:: deftheorem Def6 defines " XXREAL_3:def 6 :
for x, b2 being ext-real number holds
( ( x is real implies ( b2 = x " iff ex a being complex number st
( x = a & b2 = a " ) ) ) & ( not x is real implies ( b2 = x " iff b2 = 0 ) ) );

registration
let x be real number ;
let a be complex number ;
identify x " with a " when x = a;
compatibility
( x = a implies x " = a " )
by Def6;
end;

definition
let x, y be ext-real number ;
func x / y -> ext-real number equals :: XXREAL_3:def 7
x * (y ");
coherence
x * (y ") is ext-real number
;
end;

:: deftheorem defines / XXREAL_3:def 7 :
for x, y being ext-real number holds x / y = x * (y ");

registration
let x, y be real number ;
let a, b be complex number ;
identify x / y with a / b when x = a, y = b;
compatibility
( x = a & y = b implies x / y = a / b )
proof end;
end;

Lm16: for x being ext-real number holds x * 0 = 0
proof end;

registration
let x be ext-real positive number ;
let y be ext-real negative number ;
cluster x * y -> ext-real negative ;
coherence
x * y is negative
proof end;
end;

registration
let x, y be ext-real negative number ;
cluster x * y -> ext-real positive ;
coherence
x * y is positive
proof end;
end;

registration
let x, y be ext-real positive number ;
cluster x * y -> ext-real positive ;
coherence
x * y is positive
proof end;
end;

registration
let x be ext-real non positive number ;
let y be ext-real non negative number ;
cluster x * y -> ext-real non positive ;
coherence
not x * y is positive
proof end;
end;

registration
let x, y be ext-real non positive number ;
cluster x * y -> ext-real non negative ;
coherence
not x * y is negative
proof end;
end;

registration
let x, y be ext-real non negative number ;
cluster x * y -> ext-real non negative ;
coherence
not x * y is negative
proof end;
end;

registration
let x be ext-real non positive number ;
cluster x " -> ext-real non positive ;
coherence
not x " is positive
proof end;
end;

registration
let x be ext-real non negative number ;
cluster x " -> ext-real non negative ;
coherence
not x " is negative
proof end;
end;

registration
let x be ext-real non negative number ;
let y be ext-real non positive number ;
cluster x / y -> ext-real non positive ;
coherence
not x / y is positive
;
cluster y / x -> ext-real non positive ;
coherence
not y / x is positive
;
end;

registration
let x, y be ext-real non negative number ;
cluster x / y -> ext-real non negative ;
coherence
not x / y is negative
;
end;

registration
let x, y be ext-real non positive number ;
cluster x / y -> ext-real non negative ;
coherence
not x / y is negative
;
end;

Lm17: for x, y being ext-real number st not x is real & x * y = 0 holds
y = 0

proof end;

registration
let x, y be non zero ext-real number ;
cluster x * y -> non zero ext-real ;
coherence
not x * y is zero
proof end;
end;

registration
let x be zero ext-real number ;
let y be ext-real number ;
cluster x * y -> zero ext-real for ext-real number ;
coherence
for b1 being ext-real number st b1 = x * y holds
b1 is zero
by Lm16;
end;

Lm18: for x, y, z being ext-real number st x = 0 holds
x * (y * z) = (x * y) * z

proof end;

Lm19: for y, x, z being ext-real number st y = 0 holds
x * (y * z) = (x * y) * z

proof end;

Lm20: for y, x, z being ext-real number st not y is real holds
x * (y * z) = (x * y) * z

proof end;

Lm21: for x, y, z being ext-real number st not x is real holds
x * (y * z) = (x * y) * z

proof end;

theorem Th66: :: XXREAL_3:66
for x, y, z being ext-real number holds x * (y * z) = (x * y) * z
proof end;

:: for ext-real numbers
registration
let r be real number ;
cluster r " -> ext-real real ;
coherence
r " is real
;
end;

:: for ext-real numbers
registration
let r, s be real number ;
cluster r * s -> ext-real real ;
coherence
r * s is real
;
cluster r / s -> ext-real real ;
coherence
r / s is real
;
end;

registration
cluster -infty " -> zero ext-real ;
coherence
-infty " is zero
by Def6;
cluster +infty " -> zero ext-real ;
coherence
+infty " is zero
by Def6;
end;

theorem :: XXREAL_3:67
for f, g being ext-real number holds (f * g) " = (f ") * (g ")
proof end;

theorem :: XXREAL_3:68
for r being real number
for f, g being ext-real number st r <> 0 & r * f = r * g holds
f = g
proof end;

theorem Th69: :: XXREAL_3:69
for x, y being ext-real number st x <> +infty & x <> -infty & x * y = +infty & not y = +infty holds
y = -infty
proof end;

theorem Th70: :: XXREAL_3:70
for x, y being ext-real number st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds
y = -infty
proof end;

Lm22: for x, y being ext-real number holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 )

proof end;

theorem Th71: :: XXREAL_3:71
for x, y, z being ext-real number st x <= y & 0 <= z holds
x * z <= y * z
proof end;

theorem Th72: :: XXREAL_3:72
for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds
x * z < y * z
proof end;

theorem :: XXREAL_3:73
for x, y being ext-real number holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) by Lm22;

theorem :: XXREAL_3:74
+infty " = 0 ;

theorem :: XXREAL_3:75
-infty " = 0 ;

theorem :: XXREAL_3:76
for x being ext-real number holds x / +infty = 0 ;

theorem :: XXREAL_3:77
for x being ext-real number holds x / -infty = 0 ;

theorem Th78: :: XXREAL_3:78
for x being ext-real number st x <> -infty & x <> +infty & x <> 0 holds
x / x = 1
proof end;

theorem :: XXREAL_3:79
for x, y, z being ext-real number st x <= y & 0 < z holds
x / z <= y / z by Th71;

theorem :: XXREAL_3:80
for x, y, z being ext-real number st x < y & 0 < z & z <> +infty holds
x / z < y / z
proof end;

theorem Th81: :: XXREAL_3:81
for x being ext-real number holds 1 * x = x
proof end;

theorem Th82: :: XXREAL_3:82
for y being ext-real number holds
( not y " = 0 or y = +infty or y = -infty or y = 0 )
proof end;

theorem Th83: :: XXREAL_3:83
for y being ext-real number st 0 < y & y <> +infty holds
+infty / y = +infty
proof end;

theorem Th84: :: XXREAL_3:84
for y being ext-real number st y < 0 & -infty <> y holds
-infty / y = +infty
proof end;

theorem Th85: :: XXREAL_3:85
for y being ext-real number st y < 0 & -infty <> y holds
+infty / y = -infty
proof end;

theorem Th86: :: XXREAL_3:86
for y being ext-real number st 0 < y & y <> +infty holds
-infty / y = -infty
proof end;

theorem :: XXREAL_3:87
for x being ext-real number st x <> +infty & x <> -infty & x <> 0 holds
( x * (1 / x) = 1 & (1 / x) * x = 1 )
proof end;

theorem :: XXREAL_3:88
for y, x being ext-real number st -infty <> y & y <> +infty & y <> 0 holds
( (x * y) / y = x & x * (y / y) = x )
proof end;

theorem :: XXREAL_3:89
for y being ext-real number holds
( +infty * y <> 1 & -infty * y <> 1 )
proof end;

theorem :: XXREAL_3:90
for x, y being ext-real number st x * y <> +infty & x * y <> -infty & not x in REAL holds
y in REAL
proof end;

begin

theorem Th91: :: XXREAL_3:91
for x being ext-real number holds (- 1) * x = - x
proof end;

theorem Th92: :: XXREAL_3:92
for x, y being ext-real number holds - (x * y) = (- x) * y
proof end;

theorem Th93: :: XXREAL_3:93
for y, z, x being ext-real number st y = - z holds
x * (y + z) = (x * y) + (x * z)
proof end;

theorem Th94: :: XXREAL_3:94
for x being ext-real number holds 2 * x = x + x
proof end;

Lm23: for x, y being ext-real number holds x * (y + y) = (x * y) + (x * y)
proof end;

Lm24: for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z)
proof end;

Lm25: for y, z being ext-real number holds 0 * (y + z) = (0 * y) + (0 * z)
;

Lm26: for x, y, z being ext-real number st x is real & y is real holds
x * (y + z) = (x * y) + (x * z)

proof end;

Lm27: for x, y, z being ext-real number st x is real & not y is real holds
x * (y + z) = (x * y) + (x * z)

proof end;

theorem Th95: :: XXREAL_3:95
for x, y, z being ext-real number st x is real holds
x * (y + z) = (x * y) + (x * z)
proof end;

theorem Th96: :: XXREAL_3:96
for y, z, x being ext-real number st y >= 0 & z >= 0 holds
x * (y + z) = (x * y) + (x * z)
proof end;

theorem :: XXREAL_3:97
for y, z, x being ext-real number st y <= 0 & z <= 0 holds
x * (y + z) = (x * y) + (x * z)
proof end;

theorem :: XXREAL_3:98
for x, z being ext-real number holds x * (0 + z) = (x * 0) + (x * z) by Lm24;

theorem :: XXREAL_3:99
for f being ext-real number holds (- f) " = - (f ")
proof end;

theorem :: XXREAL_3:100
for x, y, z being ext-real number st x is real holds
x * (y - z) = (x * y) - (x * z)
proof end;

theorem Th101: :: XXREAL_3:101
for x, y, z being ext-real number st x <= y & z <= 0 holds
y * z <= x * z
proof end;

theorem Th102: :: XXREAL_3:102
for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds
y * z < x * z
proof end;

theorem :: XXREAL_3:103
for x, y, z being ext-real number st x <= y & z < 0 holds
y / z <= x / z by Th101;

theorem :: XXREAL_3:104
for x, y, z being ext-real number st x < y & z < 0 & z <> -infty holds
y / z < x / z
proof end;

theorem :: XXREAL_3:105
for x being ext-real number holds (x / 2) + (x / 2) = x
proof end;