P. 118 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11701-11800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	absled 11701	Absolute value and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( ( abs ` A ) <_ B <-> ( -u B <_ A /\ A <_ B ) ) )
Theorem	abssubge0d 11702	Absolute value of a nonnegative difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( B - A ) ) = ( B - A ) )
Theorem	abssuble0d 11703	Absolute value of a nonpositive difference. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( abs ` ( A - B ) ) = ( B - A ) )
Theorem	absdifltd 11704	The absolute value of a difference and 'less than' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) < C <-> ( ( B - C ) < A /\ A < ( B + C ) ) ) )
Theorem	absdifled 11705	The absolute value of a difference and 'less than or equal to' relation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( ( abs ` ( A - B ) ) <_ C <-> ( ( B - C ) <_ A /\ A <_ ( B + C ) ) ) )
Theorem	icodiamlt 11706	Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) ) -> ( abs ` ( C - D ) ) < ( B - A ) )
Theorem	abscld 11707	Real closure of absolute value. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) e. RR )
Theorem	absvalsqd 11708	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( A x. ( * ` A ) ) )
Theorem	absvalsq2d 11709	Square of value of absolute value function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
Theorem	absge0d 11710	Absolute value is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> 0 <_ ( abs ` A ) )
Theorem	absval2d 11711	Value of absolute value function. Definition 10.36 of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` A ) = ( sqr ` ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
Theorem	abs00d 11712	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> ( abs ` A ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	absne0d 11713	The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( abs ` A ) =/= 0 )
Theorem	absrpclapd 11714	The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( abs ` A ) e. RR+ )
Theorem	absnegd 11715	Absolute value of negative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` -u A ) = ( abs ` A ) )
Theorem	abscjd 11716	The absolute value of a number and its conjugate are the same. Proposition 10-3.7(b) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( abs ` ( * ` A ) ) = ( abs ` A ) )
Theorem	releabsd 11717	The real part of a number is less than or equal to its absolute value. Proposition 10-3.7(d) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( Re ` A ) <_ ( abs ` A ) )
Theorem	absexpd 11718	Absolute value of positive integer exponentiation. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> ( abs ` ( A ^ N ) ) = ( ( abs ` A ) ^ N ) )
Theorem	abssubd 11719	Swapping order of subtraction doesn't change the absolute value. Example of [Apostol] p. 363. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
Theorem	absmuld 11720	Absolute value distributes over multiplication. Proposition 10-3.7(f) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
Theorem	absdivapd 11721	Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( abs ` ( A / B ) ) = ( ( abs ` A ) / ( abs ` B ) ) )
Theorem	abstrid 11722	Triangle inequality for absolute value. Proposition 10-3.7(h) of [Gleason] p. 133. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A + B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difd 11723	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( abs ` A ) - ( abs ` B ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs2dif2d 11724	Difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` A ) + ( abs ` B ) ) )
Theorem	abs2difabsd 11725	Absolute value of difference of absolute values. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( abs ` ( ( abs ` A ) - ( abs ` B ) ) ) <_ ( abs ` ( A - B ) ) )
Theorem	abs3difd 11726	Absolute value of differences around common element. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( abs ` ( A - B ) ) <_ ( ( abs ` ( A - C ) ) + ( abs ` ( C - B ) ) ) )
Theorem	abs3lemd 11727	Lemma involving absolute value of differences. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. RR )   &    |- ( ph -> ( abs ` ( A - C ) ) < ( D / 2 ) )   &    |- ( ph -> ( abs ` ( C - B ) ) < ( D / 2 ) )   =>    |- ( ph -> ( abs ` ( A - B ) ) < D )
Theorem	qdenre 11728*	The rational numbers are dense in RR: any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 10488. (Contributed by BJ, 15-Oct-2021.)
|- ( ( A e. RR /\ B e. RR+ ) -> E. x e. QQ ( abs ` ( x - A ) ) < B )
4.8.5  The maximum of two real numbers
Theorem	maxcom 11729	The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- sup ( { A , B } , RR , < ) = sup ( { B , A } , RR , < )
Theorem	maxabsle 11730	An upper bound for { A , B }. (Contributed by Jim Kingdon, 20-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> A <_ ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )
Theorem	maxleim 11731	Value of maximum when we know which number is larger. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B -> sup ( { A , B } , RR , < ) = B ) )
Theorem	maxabslemab 11732	Lemma for maxabs 11735. A variation of maxleim 11731- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) = B )
Theorem	maxabslemlub 11733	Lemma for maxabs 11735. A least upper bound for { A , B }. (Contributed by Jim Kingdon, 20-Dec-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> C < ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )   =>    |- ( ph -> ( C < A \/ C < B ) )
Theorem	maxabslemval 11734*	Lemma for maxabs 11735. Value of the supremum. (Contributed by Jim Kingdon, 22-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) e. RR /\ A. x e. { A , B } -. ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) < x /\ A. x e. RR ( x < ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) -> E. z e. { A , B } x < z ) ) )
Theorem	maxabs 11735	Maximum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 20-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) = ( ( ( A + B ) + ( abs ` ( A - B ) ) ) / 2 ) )
Theorem	maxcl 11736	The maximum of two real numbers is a real number. (Contributed by Jim Kingdon, 22-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR , < ) e. RR )
Theorem	maxle1 11737	The maximum of two reals is no smaller than the first real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> A <_ sup ( { A , B } , RR , < ) )
Theorem	maxle2 11738	The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> B <_ sup ( { A , B } , RR , < ) )
Theorem	maxleast 11739	The maximum of two reals is a least upper bound. Lemma 3.11 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 22-Dec-2021.)
|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A <_ C /\ B <_ C ) ) -> sup ( { A , B } , RR , < ) <_ C )
Theorem	maxleastb 11740	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( sup ( { A , B } , RR , < ) <_ C <-> ( A <_ C /\ B <_ C ) ) )
Theorem	maxleastlt 11741	The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ C < sup ( { A , B } , RR , < ) ) ) -> ( C < A \/ C < B ) )
Theorem	maxleb 11742	Equivalence of <_ and being equal to the maximum of two reals. Lemma 3.12 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> sup ( { A , B } , RR , < ) = B ) )
Theorem	dfabsmax 11743	Absolute value of a real number in terms of maximum. Definition 3.13 of [Geuvers], p. 11. (Contributed by BJ and Jim Kingdon, 21-Dec-2021.)
|- ( A e. RR -> ( abs ` A ) = sup ( { A , -u A } , RR , < ) )
Theorem	maxltsup 11744	Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( sup ( { A , B } , RR , < ) < C <-> ( A < C /\ B < C ) ) )
Theorem	max0addsup 11745	The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.)
|- ( A e. RR -> ( sup ( { A , 0 } , RR , < ) + sup ( { -u A , 0 } , RR , < ) ) = ( abs ` A ) )
Theorem	rexanre 11746*	Combine two different upper real properties into one. (Contributed by Mario Carneiro, 8-May-2016.)
|- ( A C_ RR -> ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) ) )
Theorem	rexico 11747*	Restrict the base of an upper real quantifier to an upper real set. (Contributed by Mario Carneiro, 12-May-2016.)
|- ( ( A C_ RR /\ B e. RR ) -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) <-> E. j e. RR A. k e. A ( j <_ k -> ph ) ) )
Theorem	maxclpr 11748	The maximum of two real numbers is one of those numbers if and only if dichotomy ( A <_ B \/ B <_ A) holds. For example, this can be combined with zletric 9501 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 1-Feb-2022.)
|- ( ( A e. RR /\ B e. RR ) -> ( sup ( { A , B } , RR , < ) e. { A , B } <-> ( A <_ B \/ B <_ A ) ) )
Theorem	rpmaxcl 11749	The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> sup ( { A , B } , RR , < ) e. RR+ )
Theorem	zmaxcl 11750	The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> sup ( { A , B } , RR , < ) e. ZZ )
Theorem	nn0maxcl 11751	The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> sup ( { A , B } , RR , < ) e. NN0 )
Theorem	2zsupmax 11752	Two ways to express the maximum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 22-Jan-2023.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> sup ( { A , B } , RR , < ) = if ( A <_ B , B , A ) )
Theorem	fimaxre2 11753*	A nonempty finite set of real numbers has an upper bound. (Contributed by Jeff Madsen, 27-May-2011.) (Revised by Mario Carneiro, 13-Feb-2014.)
|- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A y <_ x )
Theorem	negfi 11754*	The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.)
|- ( ( A C_ RR /\ A e. Fin ) -> { n e. RR | -u n e. A } e. Fin )
4.8.6  The minimum of two real numbers
Theorem	mincom 11755	The minimum of two reals is commutative. (Contributed by Jim Kingdon, 8-Feb-2021.)
|- inf ( { A , B } , RR , < ) = inf ( { B , A } , RR , < )
Theorem	minmax 11756	Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 8-Feb-2021.)
|- ( ( A e. RR /\ B e. RR ) -> inf ( { A , B } , RR , < ) = -u sup ( { -u A , -u B } , RR , < ) )
Theorem	mincl 11757	The minumum of two real numbers is a real number. (Contributed by Jim Kingdon, 25-Apr-2023.)
|- ( ( A e. RR /\ B e. RR ) -> inf ( { A , B } , RR , < ) e. RR )
Theorem	min1inf 11758	The minimum of two numbers is less than or equal to the first. (Contributed by Jim Kingdon, 8-Feb-2021.)
|- ( ( A e. RR /\ B e. RR ) -> inf ( { A , B } , RR , < ) <_ A )
Theorem	min2inf 11759	The minimum of two numbers is less than or equal to the second. (Contributed by Jim Kingdon, 9-Feb-2021.)
|- ( ( A e. RR /\ B e. RR ) -> inf ( { A , B } , RR , < ) <_ B )
Theorem	lemininf 11760	Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by NM, 3-Aug-2007.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ inf ( { B , C } , RR , < ) <-> ( A <_ B /\ A <_ C ) ) )
Theorem	ltmininf 11761	Two ways of saying a number is less than the minimum of two others. (Contributed by Jim Kingdon, 10-Feb-2022.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < inf ( { B , C } , RR , < ) <-> ( A < B /\ A < C ) ) )
Theorem	minabs 11762	The minimum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 15-May-2023.)
|- ( ( A e. RR /\ B e. RR ) -> inf ( { A , B } , RR , < ) = ( ( ( A + B ) - ( abs ` ( A - B ) ) ) / 2 ) )
Theorem	minclpr 11763	The minimum of two real numbers is one of those numbers if and only if dichotomy ( A <_ B \/ B <_ A) holds. For example, this can be combined with zletric 9501 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 23-May-2023.)
|- ( ( A e. RR /\ B e. RR ) -> (inf ( { A , B } , RR , < ) e. { A , B } <-> ( A <_ B \/ B <_ A ) ) )
Theorem	rpmincl 11764	The minumum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 25-Apr-2023.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> inf ( { A , B } , RR , < ) e. RR+ )
Theorem	bdtrilem 11765	Lemma for bdtri 11766. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( ( abs ` ( A - C ) ) + ( abs ` ( B - C ) ) ) <_ ( C + ( abs ` ( ( A + B ) - C ) ) ) )
Theorem	bdtri 11766	Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> inf ( { ( A + B ) , C } , RR , < ) <_ (inf ( { A , C } , RR , < ) + inf ( { B , C } , RR , < ) ) )
Theorem	mul0inf 11767	Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 11588 and mulap0bd 8815 may better express the ideas behind it. (Contributed by Jim Kingdon, 31-Jul-2023.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A x. B ) = 0 <-> inf ( { ( abs ` A ) , ( abs ` B ) } , RR , < ) = 0 ) )
Theorem	mingeb 11768	Equivalence of <_ and being equal to the minimum of two reals. (Contributed by Jim Kingdon, 14-Oct-2024.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> inf ( { A , B } , RR , < ) = A ) )
Theorem	2zinfmin 11769	Two ways to express the minimum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 14-Oct-2024.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> inf ( { A , B } , RR , < ) = if ( A <_ B , A , B ) )
4.8.7  The maximum of two extended reals
Theorem	xrmaxleim 11770	Value of maximum when we know which extended real is larger. (Contributed by Jim Kingdon, 25-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B -> sup ( { A , B } , RR* , < ) = B ) )
Theorem	xrmaxiflemcl 11771	Lemma for xrmaxif 11777. Closure. (Contributed by Jim Kingdon, 29-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> if ( B = +oo , +oo , if ( B = -oo , A , if ( A = +oo , +oo , if ( A = -oo , B , sup ( { A , B } , RR , < ) ) ) ) ) e. RR* )
Theorem	xrmaxifle 11772	An upper bound for { A , B } in the extended reals. (Contributed by Jim Kingdon, 26-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> A <_ if ( B = +oo , +oo , if ( B = -oo , A , if ( A = +oo , +oo , if ( A = -oo , B , sup ( { A , B } , RR , < ) ) ) ) ) )
Theorem	xrmaxiflemab 11773	Lemma for xrmaxif 11777. A variation of xrmaxleim 11770- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 26-Apr-2023.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> if ( B = +oo , +oo , if ( B = -oo , A , if ( A = +oo , +oo , if ( A = -oo , B , sup ( { A , B } , RR , < ) ) ) ) ) = B )
Theorem	xrmaxiflemlub 11774	Lemma for xrmaxif 11777. A least upper bound for { A , B }. (Contributed by Jim Kingdon, 28-Apr-2023.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> C < if ( B = +oo , +oo , if ( B = -oo , A , if ( A = +oo , +oo , if ( A = -oo , B , sup ( { A , B } , RR , < ) ) ) ) ) )   =>    |- ( ph -> ( C < A \/ C < B ) )
Theorem	xrmaxiflemcom 11775	Lemma for xrmaxif 11777. Commutativity of an expression which we will later show to be the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> if ( B = +oo , +oo , if ( B = -oo , A , if ( A = +oo , +oo , if ( A = -oo , B , sup ( { A , B } , RR , < ) ) ) ) ) = if ( A = +oo , +oo , if ( A = -oo , B , if ( B = +oo , +oo , if ( B = -oo , A , sup ( { B , A } , RR , < ) ) ) ) ) )
Theorem	xrmaxiflemval 11776*	Lemma for xrmaxif 11777. Value of the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.)
|- M = if ( B = +oo , +oo , if ( B = -oo , A , if ( A = +oo , +oo , if ( A = -oo , B , sup ( { A , B } , RR , < ) ) ) ) )   =>    |- ( ( A e. RR* /\ B e. RR* ) -> ( M e. RR* /\ A. x e. { A , B } -. M < x /\ A. x e. RR* ( x < M -> E. z e. { A , B } x < z ) ) )
Theorem	xrmaxif 11777	Maximum of two extended reals in terms of if expressions. (Contributed by Jim Kingdon, 26-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> sup ( { A , B } , RR* , < ) = if ( B = +oo , +oo , if ( B = -oo , A , if ( A = +oo , +oo , if ( A = -oo , B , sup ( { A , B } , RR , < ) ) ) ) ) )
Theorem	xrmaxcl 11778	The maximum of two extended reals is an extended real. (Contributed by Jim Kingdon, 29-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> sup ( { A , B } , RR* , < ) e. RR* )
Theorem	xrmax1sup 11779	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> A <_ sup ( { A , B } , RR* , < ) )
Theorem	xrmax2sup 11780	An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> B <_ sup ( { A , B } , RR* , < ) )
Theorem	xrmaxrecl 11781	The maximum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 30-Apr-2023.)
|- ( ( A e. RR /\ B e. RR ) -> sup ( { A , B } , RR* , < ) = sup ( { A , B } , RR , < ) )
Theorem	xrmaxleastlt 11782	The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ C < sup ( { A , B } , RR* , < ) ) ) -> ( C < A \/ C < B ) )
Theorem	xrltmaxsup 11783	The maximum as a least upper bound. (Contributed by Jim Kingdon, 10-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C < sup ( { A , B } , RR* , < ) <-> ( C < A \/ C < B ) ) )
Theorem	xrmaxltsup 11784	Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 30-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( sup ( { A , B } , RR* , < ) < C <-> ( A < C /\ B < C ) ) )
Theorem	xrmaxlesup 11785	Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 10-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( sup ( { A , B } , RR* , < ) <_ C <-> ( A <_ C /\ B <_ C ) ) )
Theorem	xrmaxaddlem 11786	Lemma for xrmaxadd 11787. The case where A is real. (Contributed by Jim Kingdon, 11-May-2023.)
|- ( ( A e. RR /\ B e. RR* /\ C e. RR* ) -> sup ( { ( A +e B ) , ( A +e C ) } , RR* , < ) = ( A +e sup ( { B , C } , RR* , < ) ) )
Theorem	xrmaxadd 11787	Distributing addition over maximum. (Contributed by Jim Kingdon, 11-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> sup ( { ( A +e B ) , ( A +e C ) } , RR* , < ) = ( A +e sup ( { B , C } , RR* , < ) ) )
4.8.8  The minimum of two extended reals
Theorem	xrnegiso 11788	Negation is an order anti-isomorphism of the extended reals, which is its own inverse. (Contributed by Jim Kingdon, 2-May-2023.)
|- F = ( x e. RR* |-> -e x )   =>    |- ( F Isom < , `' < ( RR* , RR* ) /\ `' F = F )
Theorem	infxrnegsupex 11789*	The infimum of a set of extended reals A is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 2-May-2023.)
|- ( ph -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )   &    |- ( ph -> A C_ RR* )   =>    |- ( ph -> inf ( A , RR* , < ) = -e sup ( { z e. RR* | -e z e. A } , RR* , < ) )
Theorem	xrnegcon1d 11790	Contraposition law for extended real unary minus. (Contributed by Jim Kingdon, 2-May-2023.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( -e A = B <-> -e B = A ) )
Theorem	xrminmax 11791	Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 2-May-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> inf ( { A , B } , RR* , < ) = -e sup ( { -e A , -e B } , RR* , < ) )
Theorem	xrmincl 11792	The minumum of two extended reals is an extended real. (Contributed by Jim Kingdon, 3-May-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> inf ( { A , B } , RR* , < ) e. RR* )
Theorem	xrmin1inf 11793	The minimum of two extended reals is less than or equal to the first. (Contributed by Jim Kingdon, 3-May-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> inf ( { A , B } , RR* , < ) <_ A )
Theorem	xrmin2inf 11794	The minimum of two extended reals is less than or equal to the second. (Contributed by Jim Kingdon, 3-May-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> inf ( { A , B } , RR* , < ) <_ B )
Theorem	xrmineqinf 11795	The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) (Revised by Jim Kingdon, 3-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ B <_ A ) -> inf ( { A , B } , RR* , < ) = B )
Theorem	xrltmininf 11796	Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 3-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A < inf ( { B , C } , RR* , < ) <-> ( A < B /\ A < C ) ) )
Theorem	xrlemininf 11797	Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 4-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( A <_ inf ( { B , C } , RR* , < ) <-> ( A <_ B /\ A <_ C ) ) )
Theorem	xrminltinf 11798	Two ways of saying an extended real is greater than the minimum of two others. (Contributed by Jim Kingdon, 19-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> (inf ( { B , C } , RR* , < ) < A <-> ( B < A \/ C < A ) ) )
Theorem	xrminrecl 11799	The minimum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 18-May-2023.)
|- ( ( A e. RR /\ B e. RR ) -> inf ( { A , B } , RR* , < ) = inf ( { A , B } , RR , < ) )
Theorem	xrminrpcl 11800	The minimum of two positive reals is a positive real. (Contributed by Jim Kingdon, 4-May-2023.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> inf ( { A , B } , RR* , < ) e. RR+ )