:: Introduction to Arithmetic of Extended Real Numbers
:: by Library Committee
::
:: Received January 4, 2006
:: Copyright (c) 2006 Association of Mizar Users

begin

definition
let x be set ;
attr x is ext-real means :Def1: :: XXREAL_0:def 1
x in ExtREAL ;
end;

:: deftheorem Def1 defines ext-real XXREAL_0:def 1 :
for x being set holds
( x is ext-real iff x in ExtREAL );

registration
cluster ext-real set ;
existence
ex b1 being number st b1 is ext-real
proof end;
cluster -> ext-real Element of ExtREAL ;
coherence
for b1 being Element of ExtREAL holds b1 is ext-real
by Def1;
end;

definition
func +infty -> set equals :: XXREAL_0:def 2
REAL ;
coherence
REAL is set
;
func -infty -> set equals :: XXREAL_0:def 3
;
coherence
is set
;
end;

:: deftheorem defines +infty XXREAL_0:def 2 :

:: deftheorem defines -infty XXREAL_0:def 3 :

definition
redefine func ExtREAL equals :: XXREAL_0:def 4
REAL \/ ;
compatibility
for b1 being set holds
( b1 = ExtREAL iff b1 = REAL \/ )
;
end;

:: deftheorem defines ExtREAL XXREAL_0:def 4 :

registration
cluster +infty -> ext-real ;
coherence
proof end;
cluster -infty -> ext-real ;
coherence
proof end;
end;

definition
let x, y be ext-real number ;
pred x <= y means :Def5: :: XXREAL_0:def 5
ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) if ( x in REAL+ & y in REAL+ )
ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) if ( x in & y in )
otherwise ( ( y in REAL+ & x in ) or x = -infty or y = +infty );
consistency
( x in REAL+ & y in REAL+ & x in & y in implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) )
by ;
reflexivity
for x being ext-real number holds
( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in & x in implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not x in REAL+ or not x in REAL+ ) & ( not x in or not x in ) & not ( x in REAL+ & x in ) & not x = -infty implies x = +infty ) )
proof end;
connectedness
for x, y being ext-real number st ( ( x in REAL+ & y in REAL+ & ( for x9, y9 being Element of REAL+ holds
( not x = x9 or not y = y9 or not x9 <=' y9 ) ) ) or ( x in & y in & ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ) ) or ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) & not ( y in REAL+ & x in ) & not x = -infty & not y = +infty ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & x9 <=' y9 ) ) & ( y in & x in implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & y9 <=' x9 ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in or not x in ) & not ( x in REAL+ & y in ) & not y = -infty implies x = +infty ) )
proof end;
end;

:: deftheorem Def5 defines <= XXREAL_0:def 5 :
for x, y being ext-real number holds
( ( x in REAL+ & y in REAL+ implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in & y in implies ( x <= y iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & y9 <=' x9 ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in or not y in ) implies ( x <= y iff ( ( y in REAL+ & x in ) or x = -infty or y = +infty ) ) ) );

notation
let a, b be ext-real number ;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;
end;

Lm1: +infty <> [0,0]
proof end;

Lm2: not +infty in REAL+
by ;

Lm3: not -infty in REAL+
proof end;

Lm4: not +infty in
proof end;

Lm5: not -infty in
proof end;

Lm6: -infty < +infty
proof end;

theorem Th1: :: XXREAL_0:1
for a, b being ext-real number st a <= b & b <= a holds
a = b
proof end;

Lm7: for a being ext-real number st -infty >= a holds
a = -infty
proof end;

Lm8: for a being ext-real number st +infty <= a holds
a = +infty
proof end;

theorem Th2: :: XXREAL_0:2
for a, b, c being ext-real number st a <= b & b <= c holds
a <= c
proof end;

theorem :: XXREAL_0:3
for a being ext-real number holds a <= +infty by ;

theorem :: XXREAL_0:4
for a being ext-real number st +infty <= a holds
a = +infty by Lm8;

theorem :: XXREAL_0:5
for a being ext-real number holds a >= -infty by ;

theorem :: XXREAL_0:6
for a being ext-real number st -infty >= a holds
a = -infty by Lm7;

theorem :: XXREAL_0:7

theorem :: XXREAL_0:8
not +infty in REAL ;

Lm9: for a being ext-real number holds
( a in REAL or a = +infty or a = -infty )
proof end;

theorem Th9: :: XXREAL_0:9
for a being ext-real number st a in REAL holds
+infty > a
proof end;

theorem Th10: :: XXREAL_0:10
for a, b being ext-real number st a in REAL & b >= a & not b in REAL holds
b = +infty
proof end;

theorem Th11: :: XXREAL_0:11
not -infty in REAL
proof end;

theorem Th12: :: XXREAL_0:12
for a being ext-real number st a in REAL holds
-infty < a
proof end;

theorem Th13: :: XXREAL_0:13
for a, b being ext-real number st a in REAL & b <= a & not b in REAL holds
b = -infty
proof end;

theorem :: XXREAL_0:14
for a being ext-real number holds
( a in REAL or a = +infty or a = -infty ) by Lm9;

begin

registration
cluster natural -> ext-real set ;
coherence
for b1 being number st b1 is natural holds
b1 is ext-real
proof end;
end;

notation
let a be number ;
synonym zero a for empty ;
end;

definition
let a be ext-real number ;
attr a is positive means :: XXREAL_0:def 6
a > 0 ;
attr a is negative means :: XXREAL_0:def 7
a < 0 ;
redefine attr a is empty means :: XXREAL_0:def 8
a = 0 ;
compatibility
( a is zero iff a = 0 )
;
end;

:: deftheorem defines positive XXREAL_0:def 6 :
for a being ext-real number holds
( a is positive iff a > 0 );

:: deftheorem defines negative XXREAL_0:def 7 :
for a being ext-real number holds
( a is negative iff a < 0 );

:: deftheorem defines zero XXREAL_0:def 8 :
for a being ext-real number holds
( a is zero iff a = 0 );

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

registration
cluster +infty -> positive ;
coherence
proof end;
cluster -infty -> negative ;
coherence
proof end;
end;

registration
cluster ext-real positive set ;
existence
ex b1 being ext-real number st b1 is positive
proof end;
cluster ext-real negative set ;
existence
ex b1 being ext-real number st b1 is negative
proof end;
cluster zero ext-real set ;
existence
ex b1 being ext-real number st b1 is zero
proof end;
end;

begin

definition
let a, b be ext-real number ;
func min (a,b) -> set equals :Def9: :: XXREAL_0:def 9
a if a <= b
otherwise b;
correctness
coherence
( ( a <= b implies a is set ) & ( not a <= b implies b is set ) )
;
consistency
for b1 being set holds verum
;
;
commutativity
for b1 being set
for a, b being ext-real number st ( a <= b implies b1 = a ) & ( not a <= b implies b1 = b ) holds
( ( b <= a implies b1 = b ) & ( not b <= a implies b1 = a ) )
by Th1;
idempotence
for a being ext-real number holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) )
;
func max (a,b) -> set equals :Def10: :: XXREAL_0:def 10
a if b <= a
otherwise b;
correctness
coherence
( ( b <= a implies a is set ) & ( not b <= a implies b is set ) )
;
consistency
for b1 being set holds verum
;
;
commutativity
for b1 being set
for a, b being ext-real number st ( b <= a implies b1 = a ) & ( not b <= a implies b1 = b ) holds
( ( a <= b implies b1 = b ) & ( not a <= b implies b1 = a ) )
by Th1;
idempotence
for a being ext-real number holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) )
;
end;

:: deftheorem Def9 defines min XXREAL_0:def 9 :
for a, b being ext-real number holds
( ( a <= b implies min (a,b) = a ) & ( not a <= b implies min (a,b) = b ) );

:: deftheorem Def10 defines max XXREAL_0:def 10 :
for a, b being ext-real number holds
( ( b <= a implies max (a,b) = a ) & ( not b <= a implies max (a,b) = b ) );

theorem :: XXREAL_0:15
for a, b being ext-real number holds
( min (a,b) = a or min (a,b) = b ) by Def9;

theorem :: XXREAL_0:16
for a, b being ext-real number holds
( max (a,b) = a or max (a,b) = b ) by Def10;

registration
let a, b be ext-real number ;
cluster min (a,b) -> ext-real ;
coherence
min (a,b) is ext-real
by Def9;
cluster max (a,b) -> ext-real ;
coherence
max (a,b) is ext-real
by Def10;
end;

theorem Th17: :: XXREAL_0:17
for a, b being ext-real number holds min (a,b) <= a
proof end;

theorem Th18: :: XXREAL_0:18
for a, b, c, d being ext-real number st a <= b & c <= d holds
min (a,c) <= min (b,d)
proof end;

theorem :: XXREAL_0:19
for a, b, c, d being ext-real number st a < b & c < d holds
min (a,c) < min (b,d)
proof end;

theorem :: XXREAL_0:20
for a, b, c being ext-real number st a <= b & a <= c holds
a <= min (b,c) by Def9;

theorem :: XXREAL_0:21
for a, b, c being ext-real number st a < b & a < c holds
a < min (b,c) by Def9;

theorem :: XXREAL_0:22
for a, b, c being ext-real number st a <= min (b,c) holds
a <= b
proof end;

theorem :: XXREAL_0:23
for a, b, c being ext-real number st a < min (b,c) holds
a < b
proof end;

theorem :: XXREAL_0:24
for c, a, b being ext-real number st c <= a & c <= b & ( for d being ext-real number st d <= a & d <= b holds
d <= c ) holds
c = min (a,b)
proof end;

theorem Th25: :: XXREAL_0:25
for a, b being ext-real number holds a <= max (a,b)
proof end;

theorem Th26: :: XXREAL_0:26
for a, b, c, d being ext-real number st a <= b & c <= d holds
max (a,c) <= max (b,d)
proof end;

theorem :: XXREAL_0:27
for a, b, c, d being ext-real number st a < b & c < d holds
max (a,c) < max (b,d)
proof end;

theorem :: XXREAL_0:28
for b, a, c being ext-real number st b <= a & c <= a holds
max (b,c) <= a by Def10;

theorem :: XXREAL_0:29
for b, a, c being ext-real number st b < a & c < a holds
max (b,c) < a by Def10;

theorem :: XXREAL_0:30
for b, c, a being ext-real number st max (b,c) <= a holds
b <= a
proof end;

theorem :: XXREAL_0:31
for b, c, a being ext-real number st max (b,c) < a holds
b < a
proof end;

theorem :: XXREAL_0:32
for a, c, b being ext-real number st a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds
c <= d ) holds
c = max (a,b)
proof end;

theorem :: XXREAL_0:33
for a, b, c being ext-real number holds min ((min (a,b)),c) = min (a,(min (b,c)))
proof end;

theorem :: XXREAL_0:34
for a, b, c being ext-real number holds max ((max (a,b)),c) = max (a,(max (b,c)))
proof end;

theorem :: XXREAL_0:35
for a, b being ext-real number holds min ((max (a,b)),b) = b
proof end;

theorem :: XXREAL_0:36
for a, b being ext-real number holds max ((min (a,b)),b) = b
proof end;

theorem Th37: :: XXREAL_0:37
for a, c, b being ext-real number st a <= c holds
max (a,(min (b,c))) = min ((max (a,b)),c)
proof end;

theorem :: XXREAL_0:38
for a, b, c being ext-real number holds min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))
proof end;

theorem :: XXREAL_0:39
for a, b, c being ext-real number holds max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))
proof end;

theorem :: XXREAL_0:40
for a, b, c being ext-real number holds max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a)))
proof end;

theorem :: XXREAL_0:41
for a being ext-real number holds max (a,+infty) = +infty
proof end;

theorem :: XXREAL_0:42
for a being ext-real number holds min (a,+infty) = a
proof end;

theorem :: XXREAL_0:43
for a being ext-real number holds max (a,-infty) = a
proof end;

theorem :: XXREAL_0:44
for a being ext-real number holds min (a,-infty) = -infty
proof end;

begin

theorem :: XXREAL_0:45
for a, c, b being ext-real number st a in REAL & c in REAL & a <= b & b <= c holds
b in REAL
proof end;

theorem :: XXREAL_0:46
for a, b, c being ext-real number st a in REAL & a <= b & b < c holds
b in REAL
proof end;

theorem :: XXREAL_0:47
for c, a, b being ext-real number st c in REAL & a < b & b <= c holds
b in REAL
proof end;

theorem :: XXREAL_0:48
for a, b, c being ext-real number st a < b & b < c holds
b in REAL
proof end;

definition
let x, y be ext-real number ;
let a, b be set ;
func IFGT (x,y,a,b) -> set equals :Def11: :: XXREAL_0:def 11
a if x > y
otherwise b;
correctness
coherence
( ( x > y implies a is set ) & ( not x > y implies b is set ) )
;
consistency
for b1 being set holds verum
;
;
end;

:: deftheorem Def11 defines IFGT XXREAL_0:def 11 :
for x, y being ext-real number
for a, b being set holds
( ( x > y implies IFGT (x,y,a,b) = a ) & ( not x > y implies IFGT (x,y,a,b) = b ) );

registration
let x, y be ext-real number ;
let a, b be natural number ;
cluster IFGT (x,y,a,b) -> natural ;
coherence
IFGT (x,y,a,b) is natural
by Def11;
end;

theorem :: XXREAL_0:49
for a, b being ext-real number st max (a,b) <= a holds
max (a,b) = a
proof end;

theorem :: XXREAL_0:50
for a, b being ext-real number st a <= min (a,b) holds
min (a,b) = a
proof end;