:: Basic Operations on Extended Real Numbers
:: by Andrzej Trybulec
::
:: Copyright (c) 2008-2018 Association of Mizar Users

definition
let x, y be ExtReal;
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 ExtReal 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
existence
ex b1 being ExtReal st
( not b1 is real & b1 is positive )
proof end;
existence
ex b1 being ExtReal st
( not b1 is real & b1 is negative )
proof end;
end;

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

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

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

theorem Th3: :: XXREAL_3:3
for x, z being ExtReal st x < z holds
ex y being Real st
( x < y & y < z )
proof end;

definition
let x, y be ExtReal;
func x + y -> ExtReal means :Def2: :: XXREAL_3:def 2
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
( ( x is real & y is real implies ex b1 being ExtReal ex a, b being Complex st
( x = a & y = b & b1 = a + b ) ) & ( ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ex b1 being ExtReal st b1 = +infty ) & ( ( ( x = -infty & y <> +infty ) or ( y = -infty & x <> +infty ) ) implies ex b1 being ExtReal 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 ExtReal st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ExtReal holds
( ( x is real & y is real & ex a, b being Complex st
( x = a & y = b & b1 = a + b ) & ex a, b being Complex 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 ExtReal holds
( ( x is real & y is real & ( ( x = +infty & y <> -infty ) or ( y = +infty & x <> -infty ) ) implies ( ex a, b being Complex 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 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 ExtReal st ( x is real & y is real implies ex a, b being Complex 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 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 ExtReal holds
( ( x is real & y is real implies ( b3 = x + y iff ex a, b being Complex 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 ExtReal;
func - x -> ExtReal means :Def3: :: XXREAL_3:def 3
ex a being Complex 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 ExtReal ex a being Complex st
( x = a & b1 = - a ) ) & ( x = +infty implies ex b1 being ExtReal st b1 = -infty ) & ( not x is real & not x = +infty implies ex b1 being ExtReal st b1 = +infty ) )
proof end;
uniqueness
for b1, b2 being ExtReal holds
( ( x is real & ex a being Complex st
( x = a & b1 = - a ) & ex a being Complex 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 ExtReal st x is real & x = +infty holds
( ex a being Complex st
( x = a & b1 = - a ) iff b1 = -infty )
;
involutiveness
for b1, b2 being ExtReal st ( b2 is real implies ex a being Complex 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 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 ExtReal holds
( ( x is real implies ( b2 = - x iff ex a being Complex 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 ExtReal;
func x - y -> ExtReal equals :: XXREAL_3:def 4
x + (- y);
coherence
x + (- y) is ExtReal
;
end;

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

registration
let x, y be Real;
let a, b be Complex;
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;
let a be Complex;
identify - x with - a when x = a;
compatibility
( x = a implies - x = - a )
by Def3;
end;

:: for ExtReals
registration
let r be Real;
cluster - r -> real ;
coherence
- r is real
;
end;

:: for ExtReals
registration
let r, s be Real;
cluster r + s -> real ;
coherence
r + s is real
;
cluster r - s -> real ;
coherence
r - s is real
;
end;

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

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

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

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

registration
let x, y be Real;
let a, b be Complex;
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 ExtReal holds x + 0 = x
proof end;

theorem Th5: :: XXREAL_3:5

theorem Th6: :: XXREAL_3:6

Lm1:
by Def2;

Lm2:
by Def2;

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

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

Lm3: for x being ExtReal holds
( - x in REAL iff x in REAL )

proof end;

Lm4:
proof end;

Lm5:
by Def3;

Lm6: for x being ExtReal st x in REAL holds
- () = () + (- x)

proof end;

Lm7: for x being ExtReal st x in REAL holds
- () = () + (- x)

proof end;

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

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

Lm8: for x, y being ExtReal holds
( not x + y = +infty or x = +infty or y = +infty )

proof end;

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

proof end;

theorem Th11: :: XXREAL_3:11
for r being Real
for f, g being ExtReal st r + f = r + g holds
f = g
proof end;

theorem :: XXREAL_3:12
for r being Real
for f, g being ExtReal st r - f = r - g holds
f = g
proof end;

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

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

theorem Th15: :: XXREAL_3:15
for x being ExtReal holds x - 0 = x
proof end;

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

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

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

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

theorem Th20: :: XXREAL_3:20
for x, y being ExtReal 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 ExtReal 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 ExtReal st x is real holds
( (y - x) + x = y & (y + x) - x = y )
proof end;

theorem Th23: :: XXREAL_3:23
for x being ExtReal 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 x, z being ExtReal st z is real holds
x = (x + z) - z
proof end;

Lm10:
by Def3;

Lm11: for x being ExtReal st x in REAL holds
- () = () + (- x)

proof end;

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

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

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

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

theorem Th29: :: XXREAL_3:29
for x, y, z being ExtReal 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 ExtReal 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 ExtReal 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 ExtReal 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 x, y, z being ExtReal st z is real holds
(z + x) - (z + y) = x - y
proof end;

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

Lm12: for x, y, z being ExtReal st x <= y holds
x + z <= y + z

proof end;

Lm13: for x, y being ExtReal st x >= 0 & y > 0 holds
x + y > 0

proof end;

Lm14: for x, y being ExtReal st x <= 0 & y < 0 holds
x + y < 0

proof end;

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

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

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

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

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

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

registration
let x be positive ExtReal;
cluster - x -> negative ;
coherence
- x is negative
proof end;
end;

registration
let x be negative ExtReal;
cluster - x -> positive ;
coherence
- x is positive
proof end;
end;

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

registration
let x be positive ExtReal;
let y be non positive ExtReal;
cluster x - y -> positive ;
coherence
x - y is positive
;
cluster y - x -> negative ;
coherence
y - x is negative
;
end;

registration
let x be negative ExtReal;
let y be non negative ExtReal;
cluster x - y -> negative ;
coherence
x - y is negative
;
cluster y - x -> positive ;
coherence
y - x is positive
;
end;

Lm15: for x, y being ExtReal st x <= y holds
- y <= - x

proof end;

theorem :: XXREAL_3:35
for x, y, z being ExtReal st x <= y holds
x + z <= y + z by Lm12;

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

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

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

theorem Th39: :: XXREAL_3:39
for x, z being ExtReal st 0 <= z holds
x <= x + z
proof end;

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

theorem :: XXREAL_3:41
for x, y, z being ExtReal 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 ExtReal 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 x, y, z being ExtReal 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 ExtReal 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 ExtReal st x is real holds
( y + x <= z iff y <= z - x )
proof end;

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

Lm16:
by XREAL_0:def 1;

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

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

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

theorem :: XXREAL_3:50
for x being ExtReal st 0 < x holds
ex y being Real st
( 0 < y & y + y < x )
proof end;

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

theorem :: XXREAL_3:52
for x, y, z being ExtReal 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 x, y, z being ExtReal 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 ExtReal 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 x, y, z being ExtReal 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 ExtReal 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 ExtReal 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 ExtReal 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 ExtReal 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 ExtReal holds
( ( x <= - y implies y <= - x ) & ( - x <= y implies - y <= x ) )
proof end;

theorem :: XXREAL_3:61
for x, y being ExtReal st ( for e being Real st 0 < e holds
x < y + e ) holds
x <= y
proof end;

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

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

theorem :: XXREAL_3:64
for x, y, z, w being ExtReal st x < y & w < z holds
x + w < y + z
proof end;

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

definition
let x, y be ExtReal;
func x * y -> ExtReal means :Def5: :: XXREAL_3:def 5
ex a, b being Complex 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 ExtReal ex a, b being Complex 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 ExtReal 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 ExtReal 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 ExtReal st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ExtReal holds
( ( x is real & y is real & ex a, b being Complex st
( x = a & y = b & b1 = a * b ) & ex a, b being Complex 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 ExtReal 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 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 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 ExtReal st ( x is real & y is real implies ex a, b being Complex 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 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 ExtReal holds
( ( x is real & y is real implies ( b3 = x * y iff ex a, b being Complex 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;
let a, b be Complex;
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 ExtReal;
func x " -> ExtReal means :Def6: :: XXREAL_3:def 6
ex a being Complex st
( x = a & it = a " ) if x is real
otherwise it = 0 ;
existence
( ( x is real implies ex b1 being ExtReal ex a being Complex st
( x = a & b1 = a " ) ) & ( not x is real implies ex b1 being ExtReal st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being ExtReal holds
( ( x is real & ex a being Complex st
( x = a & b1 = a " ) & ex a being Complex st
( x = a & b2 = a " ) implies b1 = b2 ) & ( not x is real & b1 = 0 & b2 = 0 implies b1 = b2 ) )
;
consistency
for b1 being ExtReal holds verum
;
end;

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

registration
let x be Real;
let a be Complex;
identify x " with a " when x = a;
compatibility
( x = a implies x " = a " )
by Def6;
end;

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

:: deftheorem defines / XXREAL_3:def 7 :
for x, y being ExtReal holds x / y = x * (y ");

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

Lm17: for x being ExtReal holds x * 0 = 0
proof end;

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

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

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

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

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

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

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

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

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

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

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

Lm18: for x, y being ExtReal st not x is real & x * y = 0 holds
y = 0

proof end;

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

registration
let x be zero ExtReal;
let y be ExtReal;
cluster x * y -> zero for ExtReal;
coherence
for b1 being ExtReal st b1 = x * y holds
b1 is zero
by Lm17;
end;

Lm19: for x, y, z being ExtReal st x = 0 holds
x * (y * z) = (x * y) * z

proof end;

Lm20: for x, y, z being ExtReal st y = 0 holds
x * (y * z) = (x * y) * z

proof end;

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

proof end;

Lm22: for x, y, z being ExtReal st not x is real holds
x * (y * z) = (x * y) * z

proof end;

theorem Th66: :: XXREAL_3:66
for x, y, z being ExtReal holds x * (y * z) = (x * y) * z
proof end;

:: for ExtReals
registration
let r be Real;
cluster r " -> real ;
coherence
r " is real
;
end;

:: for ExtReals
registration
let r, s be Real;
cluster r * s -> real ;
coherence
r * s is real
;
cluster r / s -> real ;
coherence
r / s is real
;
end;

registration
coherence by Def6;
coherence by Def6;
end;

theorem :: XXREAL_3:67
for f, g being ExtReal holds (f * g) " = (f ") * (g ")
proof end;

theorem :: XXREAL_3:68
for r being Real
for f, g being ExtReal st r <> 0 & r * f = r * g holds
f = g
proof end;

theorem Th69: :: XXREAL_3:69
for x, y being ExtReal 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 ExtReal st x <> +infty & x <> -infty & x * y = -infty & not y = +infty holds
y = -infty
proof end;

Lm23: for x, y being ExtReal 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 ExtReal st x <= y & 0 <= z holds
x * z <= y * z
proof end;

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

theorem :: XXREAL_3:73
for x, y being ExtReal holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) by Lm23;

theorem :: XXREAL_3:74

theorem :: XXREAL_3:75

theorem :: XXREAL_3:76
for x being ExtReal holds x / +infty = 0 ;

theorem :: XXREAL_3:77
for x being ExtReal holds x / -infty = 0 ;

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

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

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

theorem Th81: :: XXREAL_3:81
for x being ExtReal holds 1 * x = x
proof end;

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

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

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

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

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

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

theorem :: XXREAL_3:88
for x, y being ExtReal 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 ExtReal holds
( +infty * y <> 1 & -infty * y <> 1 )
proof end;

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

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

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

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

theorem Th94: :: XXREAL_3:94
for x being ExtReal holds 2 * x = x + x
proof end;

Lm24: for x, y being ExtReal holds x * (y + y) = (x * y) + (x * y)
proof end;

Lm25: for x, z being ExtReal holds x * (0 + z) = (x * 0) + (x * z)
proof end;

Lm26: for y, z being ExtReal holds 0 * (y + z) = (0 * y) + (0 * z)
;

Lm27: for x, y, z being ExtReal st x is real & y is real holds
x * (y + z) = (x * y) + (x * z)

proof end;

Lm28: for x, y, z being ExtReal 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 ExtReal st x is real holds
x * (y + z) = (x * y) + (x * z)
proof end;

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

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

theorem :: XXREAL_3:98
for x, z being ExtReal holds x * (0 + z) = (x * 0) + (x * z) by Lm25;

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

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

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

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

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

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

theorem :: XXREAL_3:105
for x being ExtReal holds (x / 2) + (x / 2) = x
proof end;

registration
let x, y be Nat;
cluster x + y -> natural ;
coherence
x + y is natural
;
cluster x * y -> natural ;
coherence
x * y is natural
;
end;

registration
cluster - 1 -> dim-like ;
coherence
- 1 is dim-like
;
let n be dim-like number ;
cluster n + 1 -> natural ;
coherence
n + 1 is natural
;
end;