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

Lm0: not REAL in REAL
;

definition

let x be object ;

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 object holds
( x is ext-real iff x in ExtREAL );

registration

cluster ext-real for object ;

existence
ex b₁ being object st b₁ is ext-real

proof end;

cluster ext-real for set ;

existence
ex b₁ being number st b₁ is ext-real

proof end;

cluster -> ext-real for Element of ExtREAL ;

coherence
for b₁ being Element of ExtREAL holds b₁ is ext-real ;

end;

definition

mode ExtReal is ext-real Number ;

end;

registration

ExtReal ex b₁ being set st
for b₂ being ExtReal holds b₂ in b₁

proof end;

end;

definition

func +infty -> object equals :: XXREAL_0:def 2
REAL ;

coherence
REAL is object ;

func -infty -> object equals :: XXREAL_0:def 3
[0,REAL];

coherence
[0,REAL] is object ;

end;

:: deftheorem defines +infty XXREAL_0:def 2 :
+infty = REAL ;

:: deftheorem defines -infty XXREAL_0:def 3 :
-infty = [0,REAL];

definition

redefine func ExtREAL equals :: XXREAL_0:def 4
REAL \/ {+infty,-infty};

compatibility
for b₁ being set holds
( b₁ = ExtREAL iff b₁ = REAL \/ {+infty,-infty} ) ;

end;

:: deftheorem defines ExtREAL XXREAL_0:def 4 :
ExtREAL = REAL \/ {+infty,-infty};

registration

cluster +infty -> ext-real ;

coherence
+infty is ext-real

proof end;

cluster -infty -> ext-real ;

coherence
-infty is ext-real

proof end;

end;

definition

let x, y be ExtReal;

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 [:{0},REAL+:] & y in [:{0},REAL+:] )
otherwise ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty );

consistency
( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] 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 ARYTM_0:5, XBOOLE_0:3;
reflexivity
for x being ExtReal holds
( ( x in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & x9 <=' y9 ) ) & ( x in [:{0},REAL+:] & x in [:{0},REAL+:] 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 [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty implies x = +infty ) )

proof end;

connectedness
for x, y being ExtReal 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 [:{0},REAL+:] & y in [:{0},REAL+:] & ( 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 [:{0},REAL+:] or not y in [:{0},REAL+:] ) & not ( y in REAL+ & x in [:{0},REAL+:] ) & 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 [:{0},REAL+:] & x in [:{0},REAL+:] 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 [:{0},REAL+:] or not x in [:{0},REAL+:] ) & not ( x in REAL+ & y in [:{0},REAL+:] ) & not y = -infty implies x = +infty ) )

proof end;

end;

:: deftheorem Def5 defines <= XXREAL_0:def 5 :
for x, y being ExtReal 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 [:{0},REAL+:] & y in [:{0},REAL+:] 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 [:{0},REAL+:] or not y in [:{0},REAL+:] ) implies ( x <= y iff ( ( y in REAL+ & x in [:{0},REAL+:] ) or x = -infty or y = +infty ) ) ) );

notation

let a, b be ExtReal;
synonym b >= a for a <= b;
antonym b < a for a <= b;
antonym a > b for a <= b;

end;

Lm1: 0 in REAL
by NUMBERS:19;

Lm2: +infty <> [0,0]

proof end;

Lm3: not +infty in REAL+
by ARYTM_0:1, ORDINAL1:5;

Lm4: not -infty in REAL+

proof end;

Lm5: not +infty in [:{0},REAL+:]

proof end;

Lm6: not -infty in [:{0},REAL+:]

proof end;

Lm7: -infty < +infty

proof end;

theorem Th1: :: XXREAL_0:1

for a, b being ExtReal st a <= b & b <= a holds
a = b

proof end;

Lm8: for a being ExtReal st -infty >= a holds
a = -infty

proof end;

Lm9: for a being ExtReal st +infty <= a holds
a = +infty

proof end;

theorem Th2: :: XXREAL_0:2

for a, b, c being ExtReal st a <= b & b <= c holds
a <= c

proof end;

theorem :: XXREAL_0:3

for a being ExtReal holds a <= +infty by Def5, Lm3, Lm5;

theorem :: XXREAL_0:4

for a being ExtReal st +infty <= a holds
a = +infty by Lm9;

theorem :: XXREAL_0:5

for a being ExtReal holds a >= -infty by Def5, Lm4, Lm6;

theorem :: XXREAL_0:6

for a being ExtReal st -infty >= a holds
a = -infty by Lm8;

theorem :: XXREAL_0:7

-infty < +infty by Lm7;

theorem :: XXREAL_0:8

not +infty in REAL by Lm0;

Lm10: for a being ExtReal holds
( a in REAL or a = +infty or a = -infty )

proof end;

theorem Th9: :: XXREAL_0:9

for a being ExtReal st a in REAL holds
+infty > a

proof end;

theorem Th10: :: XXREAL_0:10

for a, b being ExtReal 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 ExtReal st a in REAL holds
-infty < a

proof end;

theorem Th13: :: XXREAL_0:13

for a, b being ExtReal st a in REAL & b <= a & not b in REAL holds
b = -infty

proof end;

theorem :: XXREAL_0:14

for a being ExtReal holds
( a in REAL or a = +infty or a = -infty ) by Lm10;

registration

cluster natural -> ext-real for object ;

coherence
for b₁ being object st b₁ is natural holds
b₁ is ext-real by NUMBERS:19, XBOOLE_0:def 3;

end;

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

definition

let a be ExtReal;

attr a is positive means :: XXREAL_0:def 6
a > 0 ;

attr a is negative means :: XXREAL_0:def 7
a < 0 ;

end;

:: deftheorem defines positive XXREAL_0:def 6 :
for a being ExtReal holds
( a is positive iff a > 0 );

:: deftheorem defines negative XXREAL_0:def 7 :
for a being ExtReal holds
( a is negative iff a < 0 );

:: deftheorem XXREAL_0:def 8 :
canceled;

registration

cluster ext-real positive -> non zero non negative for object ;

coherence
for b₁ being ExtReal st b₁ is positive holds
( not b₁ is negative & not b₁ is zero ) ;

cluster non zero ext-real non negative -> positive for object ;

coherence
for b₁ being ExtReal st not b₁ is negative & not b₁ is zero holds
b₁ is positive by Th1;

cluster ext-real negative -> non zero non positive for object ;

coherence
for b₁ being ExtReal st b₁ is negative holds
( not b₁ is positive & not b₁ is zero ) ;

cluster non zero ext-real non positive -> negative for object ;

coherence
for b₁ being ExtReal st not b₁ is positive & not b₁ is zero holds
b₁ is negative ;

cluster zero ext-real -> non positive non negative for object ;

coherence
for b₁ being ExtReal st b₁ is zero holds
( not b₁ is negative & not b₁ is positive ) ;

cluster ext-real non positive non negative -> zero for object ;

coherence
for b₁ being ExtReal st not b₁ is negative & not b₁ is positive holds
b₁ is zero ;

end;

registration

cluster +infty -> positive ;

coherence
+infty is positive by Th9, Lm1;

cluster -infty -> negative ;

coherence
-infty is negative by Th12, Lm1;

end;

registration

cluster ext-real positive for object ;

existence
ex b₁ being ExtReal st b₁ is positive

proof end;

cluster ext-real negative for object ;

existence
ex b₁ being ExtReal st b₁ is negative

proof end;

cluster zero ext-real for object ;

existence
ex b₁ being ExtReal st b₁ is zero

proof end;

end;

definition

let a, b be ExtReal;

func min (a,b) -> ExtReal equals :Def8: :: XXREAL_0:def 9
a if a <= b
otherwise b;

correctness
coherence
( ( a <= b implies a is ExtReal ) & ( not a <= b implies b is ExtReal ) );
consistency
for b₁ being ExtReal holds verum;
;
commutativity
for b₁, a, b being ExtReal st ( a <= b implies b₁ = a ) & ( not a <= b implies b₁ = b ) holds
( ( b <= a implies b₁ = b ) & ( not b <= a implies b₁ = a ) ) by Th1;
idempotence
for a being ExtReal holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;

func max (a,b) -> ExtReal equals :Def9: :: XXREAL_0:def 10
a if b <= a
otherwise b;

correctness
coherence
( ( b <= a implies a is ExtReal ) & ( not b <= a implies b is ExtReal ) );
consistency
for b₁ being ExtReal holds verum;
;
commutativity
for b₁, a, b being ExtReal st ( b <= a implies b₁ = a ) & ( not b <= a implies b₁ = b ) holds
( ( a <= b implies b₁ = b ) & ( not a <= b implies b₁ = a ) ) by Th1;
idempotence
for a being ExtReal holds
( ( a <= a implies a = a ) & ( not a <= a implies a = a ) ) ;

end;

:: deftheorem Def8 defines min XXREAL_0:def 9 :
for a, b being ExtReal holds
( ( a <= b implies min (a,b) = a ) & ( not a <= b implies min (a,b) = b ) );

:: deftheorem Def9 defines max XXREAL_0:def 10 :
for a, b being ExtReal holds
( ( b <= a implies max (a,b) = a ) & ( not b <= a implies max (a,b) = b ) );

theorem :: XXREAL_0:15

for a, b being ExtReal holds
( min (a,b) = a or min (a,b) = b ) by Def8;

theorem :: XXREAL_0:16

for a, b being ExtReal holds
( max (a,b) = a or max (a,b) = b ) by Def9;

registration

let a, b be ExtReal;

cluster min (a,b) -> ;

coherence
min (a,b) is ext-real ;

cluster max (a,b) -> ;

coherence
max (a,b) is ext-real ;

end;

theorem Th17: :: XXREAL_0:17

for a, b being ExtReal holds min (a,b) <= a

proof end;

theorem Th18: :: XXREAL_0:18

for a, b, c, d being ExtReal st a <= b & c <= d holds
min (a,c) <= min (b,d)

proof end;

theorem :: XXREAL_0:19

for a, b, c, d being ExtReal st a < b & c < d holds
min (a,c) < min (b,d)

proof end;

theorem :: XXREAL_0:20

for a, b, c being ExtReal st a <= b & a <= c holds
a <= min (b,c) by Def8;

theorem :: XXREAL_0:21

for a, b, c being ExtReal st a < b & a < c holds
a < min (b,c) by Def8;

theorem :: XXREAL_0:22

for a, b, c being ExtReal st a <= min (b,c) holds
a <= b

proof end;

theorem :: XXREAL_0:23

for a, b, c being ExtReal st a < min (b,c) holds
a < b

proof end;

theorem :: XXREAL_0:24

for a, b, c being ExtReal st c <= a & c <= b & ( for d being ExtReal st d <= a & d <= b holds
d <= c ) holds
c = min (a,b)

proof end;

theorem Th25: :: XXREAL_0:25

for a, b being ExtReal holds a <= max (a,b)

proof end;

theorem Th26: :: XXREAL_0:26

for a, b, c, d being ExtReal st a <= b & c <= d holds
max (a,c) <= max (b,d)

proof end;

theorem :: XXREAL_0:27

for a, b, c, d being ExtReal st a < b & c < d holds
max (a,c) < max (b,d)

proof end;

theorem :: XXREAL_0:28

for a, b, c being ExtReal st b <= a & c <= a holds
max (b,c) <= a by Def9;

theorem :: XXREAL_0:29

for a, b, c being ExtReal st b < a & c < a holds
max (b,c) < a by Def9;

theorem :: XXREAL_0:30

for a, b, c being ExtReal st max (b,c) <= a holds
b <= a

proof end;

theorem :: XXREAL_0:31

for a, b, c being ExtReal st max (b,c) < a holds
b < a

proof end;

theorem :: XXREAL_0:32

for a, b, c being ExtReal st a <= c & b <= c & ( for d being ExtReal st a <= d & b <= d holds
c <= d ) holds
c = max (a,b)

proof end;

theorem :: XXREAL_0:33

for a, b, c being ExtReal holds min ((min (a,b)),c) = min (a,(min (b,c)))

proof end;

theorem :: XXREAL_0:34

for a, b, c being ExtReal holds max ((max (a,b)),c) = max (a,(max (b,c)))

proof end;

theorem :: XXREAL_0:35

for a, b being ExtReal holds min ((max (a,b)),b) = b by Th25, Def8;

theorem :: XXREAL_0:36

for a, b being ExtReal holds max ((min (a,b)),b) = b by Th17, Def9;

theorem Th37: :: XXREAL_0:37

for a, b, c being ExtReal 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 ExtReal holds min (a,(max (b,c))) = max ((min (a,b)),(min (a,c)))

proof end;

theorem :: XXREAL_0:39

for a, b, c being ExtReal holds max (a,(min (b,c))) = min ((max (a,b)),(max (a,c)))

proof end;

theorem :: XXREAL_0:40

for a, b, c being ExtReal 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 ExtReal holds max (a,+infty) = +infty

proof end;

theorem :: XXREAL_0:42

for a being ExtReal holds min (a,+infty) = a

proof end;

theorem :: XXREAL_0:43

for a being ExtReal holds max (a,-infty) = a

proof end;

theorem :: XXREAL_0:44

for a being ExtReal holds min (a,-infty) = -infty

proof end;

theorem :: XXREAL_0:45

for a, b, c being ExtReal 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 ExtReal st a in REAL & a <= b & b < c holds
b in REAL

proof end;

theorem :: XXREAL_0:47

for a, b, c being ExtReal st c in REAL & a < b & b <= c holds
b in REAL

proof end;

theorem :: XXREAL_0:48

for a, b, c being ExtReal st a < b & b < c holds
b in REAL

proof end;

:: from AMI_2, 2008.02.14, A.T.

definition

let x, y be ExtReal;
let a, b be object ;

func IFGT (x,y,a,b) -> object equals :Def10: :: XXREAL_0:def 11
a if x > y
otherwise b;

correctness
coherence
( ( x > y implies a is object ) & ( not x > y implies b is object ) );
consistency
for b₁ being object holds verum;
;

end;

:: deftheorem Def10 defines IFGT XXREAL_0:def 11 :
for x, y being ExtReal
for a, b being object 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 ExtReal;
let a, b be natural Number ;

cluster IFGT (x,y,a,b) -> natural ;

coherence
IFGT (x,y,a,b) is natural by Def10;

end;

:: from TOPREAL7, 2008.07.05, A.T.

theorem :: XXREAL_0:49

for a, b being ExtReal st max (a,b) <= a holds
max (a,b) = a

proof end;

theorem :: XXREAL_0:50

for a, b being ExtReal st a <= min (a,b) holds
min (a,b) = a

proof end;

registration

let x be ExtReal;

reduce In (x,ExtREAL) to x;

reducibility
In (x,ExtREAL) = x by Def1, SUBSET_1:def 8;

end;