:: Introduction to Arithmetic of Extended Real Numbers :: by Library Committee :: :: Received January 4, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin definition let x be set ; attrx 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 for set ; existence ex b1 being number st b1 is ext-real proofend; cluster -> ext-real for Element of ExtREAL ; coherence for b1 being Element of ExtREAL holds b1 is ext-real by Def1; end; registration ext-real number ex b1 being set st for b2 being ext-real number holds b2 in b1 proofend; end; definition func +infty -> set equals :: XXREAL_0:def 2 REAL ; coherence REAL is set ; func -infty -> set equals :: XXREAL_0:def 3 [0,REAL]; coherence [0,REAL] is set ; 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 b1 being set holds ( b1 = ExtREAL iff b1 = 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 proofend; cluster -infty -> ext-real ; coherence -infty is ext-real proofend; end; definition let x, y be ext-real number ; predx <= 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 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 [:{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 ) ) proofend; 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 [:{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 ) ) proofend; 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 [:{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 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] proofend; Lm2: not +infty in REAL+ by ARYTM_0:1, ORDINAL1:5; Lm3: not -infty in REAL+ proofend; Lm4: not +infty in [:{0},REAL+:] proofend; Lm5: not -infty in [:{0},REAL+:] proofend; Lm6: -infty < +infty proofend; theorem Th1: :: XXREAL_0:1 for a, b being ext-real number st a <= b & b <= a holds a = b proofend; Lm7: for a being ext-real number st -infty >= a holds a = -infty proofend; Lm8: for a being ext-real number st +infty <= a holds a = +infty proofend; theorem Th2: :: XXREAL_0:2 for a, b, c being ext-real number st a <= b & b <= c holds a <= c proofend; theorem :: XXREAL_0:3 for a being ext-real number holds a <= +infty by Def5, Lm2, Lm4; 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 Def5, Lm3, Lm5; theorem :: XXREAL_0:6 for a being ext-real number st -infty >= a holds a = -infty by Lm7; theorem :: XXREAL_0:7 -infty < +infty by Lm6; 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 ) proofend; theorem Th9: :: XXREAL_0:9 for a being ext-real number st a in REAL holds +infty > a proofend; 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 proofend; theorem Th11: :: XXREAL_0:11 not -infty in REAL proofend; theorem Th12: :: XXREAL_0:12 for a being ext-real number st a in REAL holds -infty < a proofend; 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 proofend; 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 for set ; coherence for b1 being number st b1 is natural holds b1 is ext-real proofend; end; notation let a be number ; synonym zero a for empty ; end; definition let a be ext-real number ; attra is positive means :: XXREAL_0:def 6 a > 0 ; attra 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 for set ; coherence for b1 being ext-real number st b1 is positive holds ( not b1 is negative & not b1 is zero ) proofend; cluster non zero ext-real non negative -> ext-real positive for set ; coherence for b1 being ext-real number st not b1 is negative & not b1 is zero holds b1 is positive proofend; cluster ext-real negative -> non zero ext-real non positive for set ; coherence for b1 being ext-real number st b1 is negative holds ( not b1 is positive & not b1 is zero ) proofend; cluster non zero ext-real non positive -> ext-real negative for 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 for 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 for 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 +infty is positive proofend; cluster -infty -> negative ; coherence -infty is negative proofend; end; registration cluster ext-real positive for set ; existence ex b1 being ext-real number st b1 is positive proofend; cluster ext-real negative for set ; existence ex b1 being ext-real number st b1 is negative proofend; cluster zero ext-real for set ; existence ex b1 being ext-real number st b1 is zero proofend; 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 proofend; 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) proofend; 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) proofend; 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 proofend; theorem :: XXREAL_0:23 for a, b, c being ext-real number st a < min (b,c) holds a < b proofend; 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) proofend; theorem Th25: :: XXREAL_0:25 for a, b being ext-real number holds a <= max (a,b) proofend; 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) proofend; 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) proofend; 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 proofend; theorem :: XXREAL_0:31 for b, c, a being ext-real number st max (b,c) < a holds b < a proofend; 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) proofend; theorem :: XXREAL_0:33 for a, b, c being ext-real number holds min ((min (a,b)),c) = min (a,(min (b,c))) proofend; theorem :: XXREAL_0:34 for a, b, c being ext-real number holds max ((max (a,b)),c) = max (a,(max (b,c))) proofend; theorem :: XXREAL_0:35 for a, b being ext-real number holds min ((max (a,b)),b) = b proofend; theorem :: XXREAL_0:36 for a, b being ext-real number holds max ((min (a,b)),b) = b proofend; 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) proofend; 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))) proofend; 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))) proofend; 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))) proofend; theorem :: XXREAL_0:41 for a being ext-real number holds max (a,+infty) = +infty proofend; theorem :: XXREAL_0:42 for a being ext-real number holds min (a,+infty) = a proofend; theorem :: XXREAL_0:43 for a being ext-real number holds max (a,-infty) = a proofend; theorem :: XXREAL_0:44 for a being ext-real number holds min (a,-infty) = -infty proofend; 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 proofend; theorem :: XXREAL_0:46 for a, b, c being ext-real number st a in REAL & a <= b & b < c holds b in REAL proofend; theorem :: XXREAL_0:47 for c, a, b being ext-real number st c in REAL & a < b & b <= c holds b in REAL proofend; theorem :: XXREAL_0:48 for a, b, c being ext-real number st a < b & b < c holds b in REAL proofend; :: from AMI_2, 2008.02.14, A.T. 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 Nat; cluster IFGT (x,y,a,b) -> natural ; coherence IFGT (x,y,a,b) is natural by Def11; end; :: from TOPREAL7, 2008.07.05, A.T. theorem :: XXREAL_0:49 for a, b being ext-real number st max (a,b) <= a holds max (a,b) = a proofend; theorem :: XXREAL_0:50 for a, b being ext-real number st a <= min (a,b) holds min (a,b) = a proofend;