P. 120 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	releabsd 11901	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 11902	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 11903	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 11904	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 11905	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 11906	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 11907	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 11908	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 11909	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 11910	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 11911	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 11912*	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 10640. (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 11913	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 11914	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 11915	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 11916	Lemma for maxabs 11919. A variation of maxleim 11915- 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 11917	Lemma for maxabs 11919. 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 11918*	Lemma for maxabs 11919. 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 11919	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 11920	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 11921	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 11922	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 11923	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 11924	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 11925	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 11926	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 11927	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 11928	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 11929	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 11930*	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 11931*	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 11932	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 9638 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 11933	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 11934	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 11935	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 11936	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 11937*	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 11938*	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 11939	The minimum of two reals is commutative. (Contributed by Jim Kingdon, 8-Feb-2021.)
|- inf ( { A , B } , RR , < ) = inf ( { B , A } , RR , < )
Theorem	minmax 11940	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 11941	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 11942	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 11943	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 11944	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 11945	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 11946	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 11947	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 9638 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 11948	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 11949	Lemma for bdtri 11950. (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 11950	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 11951	Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 11772 and mulap0bd 8948 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 11952	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 11953	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 11954	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 11955	Lemma for xrmaxif 11961. 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 11956	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 11957	Lemma for xrmaxif 11961. A variation of xrmaxleim 11954- 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 11958	Lemma for xrmaxif 11961. 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 11959	Lemma for xrmaxif 11961. 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 11960*	Lemma for xrmaxif 11961. 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 11961	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 11962	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 11963	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 11964	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 11965	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 11966	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 11967	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 11968	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 11969	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 11970	Lemma for xrmaxadd 11971. 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 11971	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 11972	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 11973*	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 11974	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 11975	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 11976	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 11977	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 11978	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 11979	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 11980	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 11981	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 11982	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 11983	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 11984	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+ )
Theorem	xrminadd 11985	Distributing addition over minimum. (Contributed by Jim Kingdon, 10-May-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> inf ( { ( A +e B ) , ( A +e C ) } , RR* , < ) = ( A +einf ( { B , C } , RR* , < ) ) )
Theorem	xrbdtri 11986	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* /\ 0 < C ) ) -> inf ( { ( A +e B ) , C } , RR* , < ) <_ (inf ( { A , C } , RR* , < ) +einf ( { B , C } , RR* , < ) ) )
Theorem	iooinsup 11987	Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = ( sup ( { A , C } , RR* , < ) (,)inf ( { B , D } , RR* , < ) ) )
4.9  Elementary limits and convergence
4.9.1  Limits
Syntax	cli 11988	Extend class notation with convergence relation for limits.
class ~~>
Definition	df-clim 11989*	Define the limit relation for complex number sequences. See clim 11991 for its relational expression. (Contributed by NM, 28-Aug-2005.)
|- ~~> = { <. f , y >. | ( y e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( f ` k ) e. CC /\ ( abs ` ( ( f ` k ) - y ) ) < x ) ) }
Theorem	climrel 11990	The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Rel ~~>
Theorem	clim 11991*	Express the predicate: The limit of complex number sequence F is A, or F converges to A. This means that for any real x, no matter how small, there always exists an integer j such that the absolute difference of any later complex number in the sequence and the limit is less than x. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( ph -> F e. V )   &    |- ( ( ph /\ k e. ZZ ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
Theorem	climcl 11992	Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- ( F ~~> A -> A e. CC )
Theorem	clim2 11993*	Express the predicate: The limit of complex number sequence F is A, or F converges to A, with more general quantifier restrictions than clim 11991. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> A <-> ( A e. CC /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < x ) ) ) )
Theorem	clim2c 11994*	Express the predicate F converges to A. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> A <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < x ) )
Theorem	clim0 11995*	Express the predicate F converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   =>    |- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` B ) < x ) ) )
Theorem	clim0c 11996*	Express the predicate F converges to 0. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ( ph /\ k e. Z ) -> B e. CC )   =>    |- ( ph -> ( F ~~> 0 <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < x ) )
Theorem	climi 11997*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. RR+ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> F ~~> A )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( B e. CC /\ ( abs ` ( B - A ) ) < C ) )
Theorem	climi2 11998*	Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. RR+ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> F ~~> A )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( B - A ) ) < C )
Theorem	climi0 11999*	Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> C e. RR+ )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )   &    |- ( ph -> F ~~> 0 )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` B ) < C )
Theorem	climconst 12000*	An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. V )   &    |- ( ph -> A e. CC )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   =>    |- ( ph -> F ~~> A )