:: XXREAL_0 semantic presentation 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 proof take 0 ; ::_thesis: 0 is ext-real thus 0 in ExtREAL by XBOOLE_0:def_3; :: according to XXREAL_0:def_1 ::_thesis: verum end; 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 proof take ExtREAL ; ::_thesis: for b1 being ext-real number holds b1 in ExtREAL thus for b1 being ext-real number holds b1 in ExtREAL by Def1; ::_thesis: verum end; 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 proof +infty in {REAL,[0,REAL]} by TARSKI:def_2; then +infty in ExtREAL by XBOOLE_0:def_3; hence +infty is ext-real ; ::_thesis: verum end; cluster -infty -> ext-real ; coherence -infty is ext-real proof -infty in {REAL,[0,REAL]} by TARSKI:def_2; then -infty in ExtREAL by XBOOLE_0:def_3; hence -infty is ext-real ; ::_thesis: verum end; 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 ) ) proof let x be ext-real number ; ::_thesis: ( ( 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 ) ) assume A1: ( ( x in REAL+ & x in REAL+ & ( for x9, y9 being Element of REAL+ holds ( not x = x9 or not x = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & x in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds ( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ) ) or ( ( 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 & not x = +infty ) ) ; ::_thesis: contradiction x in ExtREAL by Def1; then A2: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def_3; percases ( ( x in REAL+ & ( for x9, y9 being Element of REAL+ holds ( not x = x9 or not x = y9 or not x9 <=' y9 ) ) ) or ( x in [:{0},REAL+:] & ( for x9, y9 being Element of REAL+ holds ( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ) ) or ( not x in REAL+ & not x in [:{0},REAL+:] & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ) by A1; supposethat A3: x in REAL+ and A4: for x9, y9 being Element of REAL+ holds ( not x = x9 or not x = y9 or not x9 <=' y9 ) ; ::_thesis: contradiction reconsider x9 = x as Element of REAL+ by A3; not x9 <=' x9 by A4; hence contradiction ; ::_thesis: verum end; supposethat A5: x in [:{0},REAL+:] and A6: for x9, y9 being Element of REAL+ holds ( not x = [0,x9] or not x = [0,y9] or not y9 <=' x9 ) ; ::_thesis: contradiction consider z, x9 being set such that A7: z in {0} and A8: x9 in REAL+ and A9: x = [z,x9] by A5, ZFMISC_1:84; reconsider x9 = x9 as Element of REAL+ by A8; x = [0,x9] by A7, A9, TARSKI:def_1; then not x9 <=' x9 by A6; hence contradiction ; ::_thesis: verum end; suppose ( not x in REAL+ & not x in [:{0},REAL+:] & not ( x in REAL+ & x in [:{0},REAL+:] ) & not x = -infty & not x = +infty ) ; ::_thesis: contradiction hence contradiction by A2, TARSKI:def_2, XBOOLE_0:def_3; ::_thesis: verum end; end; 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 [:{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 let x, y be ext-real number ; ::_thesis: ( ( ( 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 ) ) implies ( ( 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 ) ) ) assume A10: ( ( 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 ) ) ; ::_thesis: ( ( 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 ) ) x in ExtREAL by Def1; then A11: ( x in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or x in {+infty,-infty} ) by XBOOLE_0:def_3; y in ExtREAL by Def1; then A12: ( y in (REAL+ \/ [:{0},REAL+:]) \ {[0,0]} or y in {+infty,-infty} ) by XBOOLE_0:def_3; percases ( ( 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 ) ) by A10; supposethat A13: ( x in REAL+ & y in REAL+ ) and A14: for x9, y9 being Element of REAL+ holds ( not x = x9 or not y = y9 or not x9 <=' y9 ) ; ::_thesis: ( ( 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 ) ) hereby ::_thesis: ( ( 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 ) ) assume ( y in REAL+ & x in REAL+ ) ; ::_thesis: ex y9, x9 being Element of REAL+ st ( y = y9 & x = x9 & y9 <=' x9 ) then reconsider x9 = x, y9 = y as Element of REAL+ ; take y9 = y9; ::_thesis: ex x9 being Element of REAL+ st ( y = y9 & x = x9 & y9 <=' x9 ) take x9 = x9; ::_thesis: ( y = y9 & x = x9 & y9 <=' x9 ) thus ( y = y9 & x = x9 ) ; ::_thesis: y9 <=' x9 thus y9 <=' x9 by A14; ::_thesis: verum end; thus ( ( 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 ) ) by A13, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum end; supposethat A15: ( x in [:{0},REAL+:] & y in [:{0},REAL+:] ) and A16: for x9, y9 being Element of REAL+ holds ( not x = [0,x9] or not y = [0,y9] or not y9 <=' x9 ) ; ::_thesis: ( ( 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 ) ) now__::_thesis:_(_y_in_[:{0},REAL+:]_&_x_in_[:{0},REAL+:]_implies_ex_y9,_x9_being_Element_of_REAL+_st_ (_y_=_[0,y9]_&_x_=_[0,x9]_&_x9_<='_y9_)_) assume y in [:{0},REAL+:] ; ::_thesis: ( x in [:{0},REAL+:] implies ex y9, x9 being Element of REAL+ st ( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) ) then consider z, y9 being set such that A17: z in {0} and A18: y9 in REAL+ and A19: y = [z,y9] by ZFMISC_1:84; A20: z = 0 by A17, TARSKI:def_1; assume x in [:{0},REAL+:] ; ::_thesis: ex y9, x9 being Element of REAL+ st ( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) then consider z, x9 being set such that A21: z in {0} and A22: x9 in REAL+ and A23: x = [z,x9] by ZFMISC_1:84; reconsider x9 = x9, y9 = y9 as Element of REAL+ by A18, A22; take y9 = y9; ::_thesis: ex x9 being Element of REAL+ st ( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) take x9 = x9; ::_thesis: ( y = [0,y9] & x = [0,x9] & x9 <=' y9 ) thus ( y = [0,y9] & x = [0,x9] ) by A17, A19, A21, A23, TARSKI:def_1; ::_thesis: x9 <=' y9 z = 0 by A21, TARSKI:def_1; hence x9 <=' y9 by A16, A19, A20, A23; ::_thesis: verum end; hence ( ( 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 ) ) by A15, ARYTM_0:5, XBOOLE_0:3; ::_thesis: verum end; suppose ( ( 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 ) ; ::_thesis: ( ( 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 ) ) hence ( ( 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 ) ) by A11, A12, TARSKI:def_2, XBOOLE_0:def_3; ::_thesis: verum end; end; 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 [:{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] proof assume +infty = [0,0] ; ::_thesis: contradiction then +infty = {{0},{0}} by ENUMSET1:29 .= {{0}} by ENUMSET1:29 ; hence contradiction by TARSKI:def_1; ::_thesis: verum end; Lm2: not +infty in REAL+ by ARYTM_0:1, ORDINAL1:5; Lm3: not -infty in REAL+ proof A1: ( {0,REAL} in -infty & REAL in {0,REAL} ) by TARSKI:def_2; assume -infty in REAL+ ; ::_thesis: contradiction hence contradiction by A1, ARYTM_0:1, XREGULAR:7; ::_thesis: verum end; Lm4: not +infty in [:{0},REAL+:] proof assume +infty in [:{0},REAL+:] ; ::_thesis: contradiction then +infty in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def_3; then +infty in REAL by Lm1, ZFMISC_1:56; hence contradiction ; ::_thesis: verum end; Lm5: not -infty in [:{0},REAL+:] proof assume -infty in [:{0},REAL+:] ; ::_thesis: contradiction then REAL in REAL+ by ZFMISC_1:87; hence contradiction by ARYTM_0:1, ORDINAL1:5; ::_thesis: verum end; Lm6: -infty < +infty proof -infty <> +infty by TARSKI:def_2; hence -infty < +infty by Def5, Lm3, Lm5; ::_thesis: verum end; theorem Th1: :: XXREAL_0:1 for a, b being ext-real number st a <= b & b <= a holds a = b proof let a, b be ext-real number ; ::_thesis: ( a <= b & b <= a implies a = b ) assume that A1: a <= b and A2: b <= a ; ::_thesis: a = b percases ( ( a in REAL+ & b in REAL+ ) or ( a in REAL+ & b in [:{0},REAL+:] ) or ( b in REAL+ & a in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) or ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) or ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) & ( not b in REAL+ or not a in [:{0},REAL+:] ) & ( not a in REAL+ or not b in [:{0},REAL+:] ) ) ) ; suppose ( a in REAL+ & b in REAL+ ) ; ::_thesis: a = b then ( ex a9, b9 being Element of REAL+ st ( a = a9 & b = b9 & a9 <=' b9 ) & ex b99, a99 being Element of REAL+ st ( b = b99 & a = a99 & b99 <=' a99 ) ) by A1, A2, Def5; hence a = b by ARYTM_1:4; ::_thesis: verum end; supposeA3: ( a in REAL+ & b in [:{0},REAL+:] ) ; ::_thesis: a = b then ( not b in REAL+ & not a in [:{0},REAL+:] ) by ARYTM_0:5, XBOOLE_0:3; hence a = b by A1, A3, Def5, Lm3, Lm4; ::_thesis: verum end; supposeA4: ( b in REAL+ & a in [:{0},REAL+:] ) ; ::_thesis: a = b then ( not a in REAL+ & not b in [:{0},REAL+:] ) by ARYTM_0:5, XBOOLE_0:3; hence a = b by A2, A4, Def5, Lm3, Lm4; ::_thesis: verum end; supposeA5: ( a in [:{0},REAL+:] & b in [:{0},REAL+:] ) ; ::_thesis: a = b consider a9, b9 being Element of REAL+ such that A6: ( a = [0,a9] & b = [0,b9] ) and A7: b9 <=' a9 by A1, A5, Def5; consider b99, a99 being Element of REAL+ such that A8: ( b = [0,b99] & a = [0,a99] ) and A9: a99 <=' b99 by A2, A5, Def5; ( a9 = a99 & b9 = b99 ) by A6, A8, XTUPLE_0:1; hence a = b by A7, A8, A9, ARYTM_1:4; ::_thesis: verum end; suppose ( ( a = -infty or a = +infty ) & ( b = -infty or b = +infty ) ) ; ::_thesis: a = b hence a = b by A1, A2, Lm6; ::_thesis: verum end; supposethat A10: ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) and A11: ( not b in REAL+ or not a in [:{0},REAL+:] ) and A12: ( not a in REAL+ or not b in [:{0},REAL+:] ) ; ::_thesis: a = b ( a = -infty or b = +infty ) by A1, A10, A11, Def5; hence a = b by A2, A10, A12, Def5, Lm6; ::_thesis: verum end; end; end; Lm7: for a being ext-real number st -infty >= a holds a = -infty proof let a be ext-real number ; ::_thesis: ( -infty >= a implies a = -infty ) a >= -infty by Def5, Lm3, Lm5; hence ( -infty >= a implies a = -infty ) by Th1; ::_thesis: verum end; Lm8: for a being ext-real number st +infty <= a holds a = +infty proof let a be ext-real number ; ::_thesis: ( +infty <= a implies a = +infty ) a <= +infty by Def5, Lm2, Lm4; hence ( +infty <= a implies a = +infty ) by Th1; ::_thesis: verum end; theorem Th2: :: XXREAL_0:2 for a, b, c being ext-real number st a <= b & b <= c holds a <= c proof let a, b, c be ext-real number ; ::_thesis: ( a <= b & b <= c implies a <= c ) assume that A1: a <= b and A2: b <= c ; ::_thesis: a <= c percases ( ( a in REAL+ & b in REAL+ & c in REAL+ ) or ( a in REAL+ & b in [:{0},REAL+:] ) or ( b in REAL+ & c in [:{0},REAL+:] ) or ( a in [:{0},REAL+:] & c in REAL+ ) or ( a in [:{0},REAL+:] & b in [:{0},REAL+:] & c in [:{0},REAL+:] ) or ( ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) & ( not a in REAL+ or not b in [:{0},REAL+:] ) & ( not b in REAL+ or not c in [:{0},REAL+:] ) & ( not a in [:{0},REAL+:] or not c in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ) ) ; supposethat A3: a in REAL+ and A4: b in REAL+ and A5: c in REAL+ ; ::_thesis: a <= c consider b99, c9 being Element of REAL+ such that A6: b = b99 and A7: c = c9 and A8: b99 <=' c9 by A2, A4, A5, Def5; consider a9, b9 being Element of REAL+ such that A9: a = a9 and A10: ( b = b9 & a9 <=' b9 ) by A1, A3, A4, Def5; a9 <=' c9 by A10, A6, A8, ARYTM_1:3; hence a <= c by A5, A9, A7, Def5; ::_thesis: verum end; supposeA11: ( a in REAL+ & b in [:{0},REAL+:] ) ; ::_thesis: a <= c then ( ( not a in REAL+ or not b in REAL+ ) & ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3; hence a <= c by A1, A11, Def5, Lm3, Lm4; ::_thesis: verum end; supposeA12: ( b in REAL+ & c in [:{0},REAL+:] ) ; ::_thesis: a <= c then ( ( not c in REAL+ or not b in REAL+ ) & ( not c in [:{0},REAL+:] or not b in [:{0},REAL+:] ) ) by ARYTM_0:5, XBOOLE_0:3; hence a <= c by A2, A12, Def5, Lm3, Lm4; ::_thesis: verum end; supposeA13: ( a in [:{0},REAL+:] & c in REAL+ ) ; ::_thesis: a <= c ( ( not a in REAL+ or not c in REAL+ ) & ( not a in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ) by A13, ARYTM_0:5, XBOOLE_0:3; hence a <= c by A13, Def5; ::_thesis: verum end; supposethat A14: a in [:{0},REAL+:] and A15: b in [:{0},REAL+:] and A16: c in [:{0},REAL+:] ; ::_thesis: a <= c consider b99, c9 being Element of REAL+ such that A17: b = [0,b99] and A18: c = [0,c9] and A19: c9 <=' b99 by A2, A15, A16, Def5; consider a9, b9 being Element of REAL+ such that A20: a = [0,a9] and A21: b = [0,b9] and A22: b9 <=' a9 by A1, A14, A15, Def5; b9 = b99 by A21, A17, XTUPLE_0:1; then c9 <=' a9 by A22, A19, ARYTM_1:3; hence a <= c by A14, A16, A20, A18, Def5; ::_thesis: verum end; supposethat A23: ( not a in REAL+ or not b in REAL+ or not c in REAL+ ) and A24: ( not a in REAL+ or not b in [:{0},REAL+:] ) and A25: ( not b in REAL+ or not c in [:{0},REAL+:] ) and A26: ( not a in [:{0},REAL+:] or not c in REAL+ ) and A27: ( not a in [:{0},REAL+:] or not b in [:{0},REAL+:] or not c in [:{0},REAL+:] ) ; ::_thesis: a <= c A28: ( b = +infty implies c = +infty ) by A2, Lm8; A29: ( b = -infty implies a = -infty ) by A1, Lm7; ( a = -infty or b = +infty or b = -infty or c = +infty ) by A1, A2, A23, A25, A26, A27, Def5; hence a <= c by A1, A2, A23, A24, A25, A27, A28, A29, Def5; ::_thesis: verum end; end; end; 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 ) proof let a be ext-real number ; ::_thesis: ( a in REAL or a = +infty or a = -infty ) a in ExtREAL by Def1; then ( a in REAL or a in {+infty,-infty} ) by XBOOLE_0:def_3; hence ( a in REAL or a = +infty or a = -infty ) by TARSKI:def_2; ::_thesis: verum end; theorem Th9: :: XXREAL_0:9 for a being ext-real number st a in REAL holds +infty > a proof let a be ext-real number ; ::_thesis: ( a in REAL implies +infty > a ) assume a in REAL ; ::_thesis: +infty > a then A1: a <> +infty ; +infty >= a by Def5, Lm2, Lm4; hence +infty > a by A1, Th1; ::_thesis: verum 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 let a, b be ext-real number ; ::_thesis: ( a in REAL & b >= a & not b in REAL implies b = +infty ) assume that A1: a in REAL and A2: b >= a ; ::_thesis: ( b in REAL or b = +infty ) assume A3: not b in REAL ; ::_thesis: b = +infty ( b = -infty implies a = -infty ) by A2, Lm7; hence b = +infty by A1, A3, Lm9; ::_thesis: verum end; theorem Th11: :: XXREAL_0:11 not -infty in REAL proof A1: ( {0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} ) by TARSKI:def_2; assume -infty in REAL ; ::_thesis: contradiction hence contradiction by A1, XREGULAR:7; ::_thesis: verum end; theorem Th12: :: XXREAL_0:12 for a being ext-real number st a in REAL holds -infty < a proof let a be ext-real number ; ::_thesis: ( a in REAL implies -infty < a ) -infty <= a by Def5, Lm3, Lm5; hence ( a in REAL implies -infty < a ) by Th1, Th11; ::_thesis: verum 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 let a, b be ext-real number ; ::_thesis: ( a in REAL & b <= a & not b in REAL implies b = -infty ) assume that A1: a in REAL and A2: b <= a ; ::_thesis: ( b in REAL or b = -infty ) assume A3: not b in REAL ; ::_thesis: b = -infty ( b = +infty implies a = +infty ) by A2, Lm8; hence b = -infty by A1, A3, Lm9; ::_thesis: verum 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 for set ; coherence for b1 being number st b1 is natural holds b1 is ext-real proof let a be number ; ::_thesis: ( a is natural implies a is ext-real ) assume a is natural ; ::_thesis: a is ext-real then a in NAT by ORDINAL1:def_12; hence a in ExtREAL by XBOOLE_0:def_3; :: according to XXREAL_0:def_1 ::_thesis: verum end; 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 ) proof let r be ext-real number ; ::_thesis: ( r is positive implies ( not r is negative & not r is zero ) ) assume r > 0 ; :: according to XXREAL_0:def_6 ::_thesis: ( not r is negative & not r is zero ) hence ( r >= 0 & r <> 0 ) ; :: according to XXREAL_0:def_7,XXREAL_0:def_8 ::_thesis: verum end; 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 proof let r be ext-real number ; ::_thesis: ( not r is negative & not r is zero implies r is positive ) assume ( r >= 0 & r <> 0 ) ; :: according to XXREAL_0:def_7,XXREAL_0:def_8 ::_thesis: r is positive hence r > 0 by Th1; :: according to XXREAL_0:def_6 ::_thesis: verum end; 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 ) proof let r be ext-real number ; ::_thesis: ( r is negative implies ( not r is positive & not r is zero ) ) assume r < 0 ; :: according to XXREAL_0:def_7 ::_thesis: ( not r is positive & not r is zero ) hence ( r <= 0 & r <> {} ) ; :: according to XXREAL_0:def_6,XXREAL_0:def_8 ::_thesis: verum end; 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 proof thus 0 < +infty by Th9; :: according to XXREAL_0:def_6 ::_thesis: verum end; cluster -infty -> negative ; coherence -infty is negative proof thus 0 > -infty by Th12; :: according to XXREAL_0:def_7 ::_thesis: verum end; end; registration cluster ext-real positive for set ; existence ex b1 being ext-real number st b1 is positive proof take +infty ; ::_thesis: +infty is positive thus +infty is positive ; ::_thesis: verum end; cluster ext-real negative for set ; existence ex b1 being ext-real number st b1 is negative proof take -infty ; ::_thesis: -infty is negative thus -infty is negative ; ::_thesis: verum end; cluster zero ext-real for set ; existence ex b1 being ext-real number st b1 is zero proof reconsider z = 0 as ext-real number ; take z ; ::_thesis: z is zero thus z = 0 ; :: according to XXREAL_0:def_8 ::_thesis: verum 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 let a, b be ext-real number ; ::_thesis: min (a,b) <= a ( a <= b or not a <= b ) ; hence min (a,b) <= a by Def9; ::_thesis: verum 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 let a, b, c, d be ext-real number ; ::_thesis: ( a <= b & c <= d implies min (a,c) <= min (b,d) ) assume that A1: a <= b and A2: c <= d ; ::_thesis: min (a,c) <= min (b,d) min (a,c) <= c by Th17; then A3: min (a,c) <= d by A2, Th2; min (a,c) <= a by Th17; then min (a,c) <= b by A1, Th2; hence min (a,c) <= min (b,d) by A3, Def9; ::_thesis: verum 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 let a, b, c, d be ext-real number ; ::_thesis: ( a < b & c < d implies min (a,c) < min (b,d) ) assume that A1: a < b and A2: c < d ; ::_thesis: min (a,c) < min (b,d) min (a,c) <= c by Th17; then A3: min (a,c) < d by A2, Th2; min (a,c) <= a by Th17; then min (a,c) < b by A1, Th2; hence min (a,c) < min (b,d) by A3, Def9; ::_thesis: verum 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 let a, b, c be ext-real number ; ::_thesis: ( a <= min (b,c) implies a <= b ) min (b,c) <= b by Th17; hence ( a <= min (b,c) implies a <= b ) by Th2; ::_thesis: verum end; theorem :: XXREAL_0:23 for a, b, c being ext-real number st a < min (b,c) holds a < b proof let a, b, c be ext-real number ; ::_thesis: ( a < min (b,c) implies a < b ) min (b,c) <= b by Th17; hence ( a < min (b,c) implies a < b ) by Th2; ::_thesis: verum 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 let c, a, b be ext-real number ; ::_thesis: ( c <= a & c <= b & ( for d being ext-real number st d <= a & d <= b holds d <= c ) implies c = min (a,b) ) assume that A1: ( c <= a & c <= b ) and A2: for d being ext-real number st d <= a & d <= b holds d <= c ; ::_thesis: c = min (a,b) ( min (a,b) <= a & min (a,b) <= b ) by Th17; then A3: min (a,b) <= c by A2; c <= min (a,b) by A1, Def9; hence c = min (a,b) by A3, Th1; ::_thesis: verum end; theorem Th25: :: XXREAL_0:25 for a, b being ext-real number holds a <= max (a,b) proof let a, b be ext-real number ; ::_thesis: a <= max (a,b) ( a <= b or not a <= b ) ; hence a <= max (a,b) by Def10; ::_thesis: verum 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 let a, b, c, d be ext-real number ; ::_thesis: ( a <= b & c <= d implies max (a,c) <= max (b,d) ) assume that A1: a <= b and A2: c <= d ; ::_thesis: max (a,c) <= max (b,d) d <= max (b,d) by Th25; then A3: c <= max (b,d) by A2, Th2; b <= max (b,d) by Th25; then a <= max (b,d) by A1, Th2; hence max (a,c) <= max (b,d) by A3, Def10; ::_thesis: verum 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 let a, b, c, d be ext-real number ; ::_thesis: ( a < b & c < d implies max (a,c) < max (b,d) ) assume that A1: a < b and A2: c < d ; ::_thesis: max (a,c) < max (b,d) d <= max (b,d) by Th25; then A3: c < max (b,d) by A2, Th2; b <= max (b,d) by Th25; then a < max (b,d) by A1, Th2; hence max (a,c) < max (b,d) by A3, Def10; ::_thesis: verum 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 let b, c, a be ext-real number ; ::_thesis: ( max (b,c) <= a implies b <= a ) b <= max (b,c) by Th25; hence ( max (b,c) <= a implies b <= a ) by Th2; ::_thesis: verum end; theorem :: XXREAL_0:31 for b, c, a being ext-real number st max (b,c) < a holds b < a proof let b, c, a be ext-real number ; ::_thesis: ( max (b,c) < a implies b < a ) b <= max (b,c) by Th25; hence ( max (b,c) < a implies b < a ) by Th2; ::_thesis: verum 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 let a, c, b be ext-real number ; ::_thesis: ( a <= c & b <= c & ( for d being ext-real number st a <= d & b <= d holds c <= d ) implies c = max (a,b) ) assume that A1: ( a <= c & b <= c ) and A2: for d being ext-real number st a <= d & b <= d holds c <= d ; ::_thesis: c = max (a,b) ( a <= max (a,b) & b <= max (a,b) ) by Th25; then A3: c <= max (a,b) by A2; max (a,b) <= c by A1, Def10; hence c = max (a,b) by A3, Th1; ::_thesis: verum 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 let a, b, c be ext-real number ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c))) percases ( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) ) by Th2; suppose ( a <= b & a <= c ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c))) then ( min (a,b) = a & min (a,c) = a ) by Def9; hence min ((min (a,b)),c) = min (a,(min (b,c))) by Def9; ::_thesis: verum end; suppose ( b <= a & b <= c ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c))) then ( min (a,b) = b & min (b,c) = b ) by Def9; hence min ((min (a,b)),c) = min (a,(min (b,c))) ; ::_thesis: verum end; suppose ( c <= b & c <= a ) ; ::_thesis: min ((min (a,b)),c) = min (a,(min (b,c))) then ( min (b,c) = c & min (a,c) = c ) by Def9; hence min ((min (a,b)),c) = min (a,(min (b,c))) by Def9; ::_thesis: verum end; end; 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 let a, b, c be ext-real number ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c))) percases ( ( a <= b & a <= c ) or ( b <= a & b <= c ) or ( c <= b & c <= a ) ) by Th2; supposeA1: ( a <= b & a <= c ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c))) A2: ( max (b,c) = b or max (b,c) = c ) by Def10; max (a,b) = b by A1, Def10; hence max ((max (a,b)),c) = max (a,(max (b,c))) by A1, A2, Def10; ::_thesis: verum end; supposeA3: ( b <= a & b <= c ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c))) then max (a,b) = a by Def10; hence max ((max (a,b)),c) = max (a,(max (b,c))) by A3, Def10; ::_thesis: verum end; supposeA4: ( c <= b & c <= a ) ; ::_thesis: max ((max (a,b)),c) = max (a,(max (b,c))) A5: ( max (a,b) = b or max (a,b) = a ) by Def10; max (b,c) = b by A4, Def10; hence max ((max (a,b)),c) = max (a,(max (b,c))) by A4, A5, Def10; ::_thesis: verum end; end; end; theorem :: XXREAL_0:35 for a, b being ext-real number holds min ((max (a,b)),b) = b proof let a, b be ext-real number ; ::_thesis: min ((max (a,b)),b) = b b <= max (a,b) by Th25; hence min ((max (a,b)),b) = b by Def9; ::_thesis: verum end; theorem :: XXREAL_0:36 for a, b being ext-real number holds max ((min (a,b)),b) = b proof let a, b be ext-real number ; ::_thesis: max ((min (a,b)),b) = b min (a,b) <= b by Th17; hence max ((min (a,b)),b) = b by Def10; ::_thesis: verum 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 let a, c, b be ext-real number ; ::_thesis: ( a <= c implies max (a,(min (b,c))) = min ((max (a,b)),c) ) assume A1: a <= c ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c) percases ( a <= b or b <= a ) ; supposeA2: a <= b ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c) then a <= min (b,c) by A1, Def9; hence max (a,(min (b,c))) = min (b,c) by Def10 .= min ((max (a,b)),c) by A2, Def10 ; ::_thesis: verum end; supposeA3: b <= a ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),c) then b <= c by A1, Th2; hence max (a,(min (b,c))) = max (a,b) by Def9 .= a by A3, Def10 .= min (a,c) by A1, Def9 .= min ((max (a,b)),c) by A3, Def10 ; ::_thesis: verum end; end; 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 let a, b, c be ext-real number ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c))) percases ( b <= c or c <= b ) ; supposeA1: b <= c ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c))) then A2: min (a,b) <= min (a,c) by Th18; thus min (a,(max (b,c))) = min (a,c) by A1, Def10 .= max ((min (a,b)),(min (a,c))) by A2, Def10 ; ::_thesis: verum end; supposeA3: c <= b ; ::_thesis: min (a,(max (b,c))) = max ((min (a,b)),(min (a,c))) then A4: min (a,c) <= min (a,b) by Th18; thus min (a,(max (b,c))) = min (a,b) by A3, Def10 .= max ((min (a,b)),(min (a,c))) by A4, Def10 ; ::_thesis: verum end; end; 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 let a, b, c be ext-real number ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c))) percases ( b <= c or c <= b ) ; supposeA1: b <= c ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c))) then A2: max (a,b) <= max (a,c) by Th26; thus max (a,(min (b,c))) = max (a,b) by A1, Def9 .= min ((max (a,b)),(max (a,c))) by A2, Def9 ; ::_thesis: verum end; supposeA3: c <= b ; ::_thesis: max (a,(min (b,c))) = min ((max (a,b)),(max (a,c))) then A4: max (a,c) <= max (a,b) by Th26; thus max (a,(min (b,c))) = max (a,c) by A3, Def9 .= min ((max (a,b)),(max (a,c))) by A4, Def9 ; ::_thesis: verum end; end; 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 let a, b, c be ext-real number ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) percases ( a <= c or c <= a ) ; supposeA1: a <= c ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) then A2: max (a,b) <= max (b,c) by Th26; min (a,b) <= min (b,c) by A1, Th18; hence max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = max ((min (b,c)),(min (c,a))) by Def10 .= max ((min (b,c)),a) by A1, Def9 .= min ((max (a,b)),c) by A1, Th37 .= min ((max (a,b)),(max (c,a))) by A1, Def10 .= min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) by A2, Def9 ; ::_thesis: verum end; supposeA3: c <= a ; ::_thesis: max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) then A4: max (a,b) >= max (b,c) by Th26; min (a,b) >= min (b,c) by A3, Th18; hence max ((max ((min (a,b)),(min (b,c)))),(min (c,a))) = max ((min (a,b)),(min (c,a))) by Def10 .= max ((min (a,b)),c) by A3, Def9 .= min ((max (c,b)),a) by A3, Th37 .= min ((max (c,b)),(max (c,a))) by A3, Def10 .= min ((min ((max (a,b)),(max (b,c)))),(max (c,a))) by A4, Def9 ; ::_thesis: verum end; end; end; theorem :: XXREAL_0:41 for a being ext-real number holds max (a,+infty) = +infty proof let a be ext-real number ; ::_thesis: max (a,+infty) = +infty a <= +infty by Def5, Lm2, Lm4; hence max (a,+infty) = +infty by Def10; ::_thesis: verum end; theorem :: XXREAL_0:42 for a being ext-real number holds min (a,+infty) = a proof let a be ext-real number ; ::_thesis: min (a,+infty) = a a <= +infty by Def5, Lm2, Lm4; hence min (a,+infty) = a by Def9; ::_thesis: verum end; theorem :: XXREAL_0:43 for a being ext-real number holds max (a,-infty) = a proof let a be ext-real number ; ::_thesis: max (a,-infty) = a a >= -infty by Def5, Lm3, Lm5; hence max (a,-infty) = a by Def10; ::_thesis: verum end; theorem :: XXREAL_0:44 for a being ext-real number holds min (a,-infty) = -infty proof let a be ext-real number ; ::_thesis: min (a,-infty) = -infty a >= -infty by Def5, Lm3, Lm5; hence min (a,-infty) = -infty by Def9; ::_thesis: verum 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 let a, c, b be ext-real number ; ::_thesis: ( a in REAL & c in REAL & a <= b & b <= c implies b in REAL ) assume that A1: a in REAL and A2: c in REAL and A3: a <= b and A4: b <= c ; ::_thesis: b in REAL ( b in REAL or b = +infty ) by A1, A3, Th10; hence b in REAL by A2, A4, Th13; ::_thesis: verum 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 let a, b, c be ext-real number ; ::_thesis: ( a in REAL & a <= b & b < c implies b in REAL ) assume that A1: ( a in REAL & a <= b ) and A2: b < c ; ::_thesis: b in REAL ( b in REAL or b = +infty ) by A1, Th10; hence b in REAL by A2, Lm8; ::_thesis: verum 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 let c, a, b be ext-real number ; ::_thesis: ( c in REAL & a < b & b <= c implies b in REAL ) assume that A1: c in REAL and A2: a < b and A3: b <= c ; ::_thesis: b in REAL ( b in REAL or b = -infty ) by A1, A3, Th13; hence b in REAL by A2, Lm7; ::_thesis: verum end; theorem :: XXREAL_0:48 for a, b, c being ext-real number st a < b & b < c holds b in REAL proof let a, b, c be ext-real number ; ::_thesis: ( a < b & b < c implies b in REAL ) assume A1: ( a < b & b < c ) ; ::_thesis: b in REAL ( b in REAL or b = +infty or b = -infty ) by Lm9; hence b in REAL by A1, Lm7, Lm8; ::_thesis: verum 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 Nat; 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 let a, b be ext-real number ; ::_thesis: ( max (a,b) <= a implies max (a,b) = a ) assume max (a,b) <= a ; ::_thesis: max (a,b) = a then ( max (a,b) < a or max (a,b) = a ) by Th1; hence max (a,b) = a by Th25; ::_thesis: verum end; theorem :: XXREAL_0:50 for a, b being ext-real number st a <= min (a,b) holds min (a,b) = a proof let a, b be ext-real number ; ::_thesis: ( a <= min (a,b) implies min (a,b) = a ) assume min (a,b) >= a ; ::_thesis: min (a,b) = a then ( min (a,b) > a or min (a,b) = a ) by Th1; hence min (a,b) = a by Th17; ::_thesis: verum end;