P. 397 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39601-39700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	infxrrefi 39601	The real and extended real infima match when the set is finite. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> inf ( A , RR* , < ) = inf ( A , RR , < ) )
Theorem	xrralrecnnle 39602*	Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- F/ n ph   &    |- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A <_ B <-> A. n e. NN A <_ ( B + ( 1 / n ) ) ) )
Theorem	fzoct 39603	A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( N..^ M ) ~<_ om
Theorem	frexr 39604	A function taking real values, is a function taking extended real values. Common case. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> F : A --> RR )   =>    |- ( ph -> F : A --> RR* )
Theorem	nnrecrp 39605	The reciprocal of a positive natural number is a positive real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( N e. NN -> ( 1 / N ) e. RR+ )
Theorem	qred 39606	A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. QQ )   =>    |- ( ph -> A e. RR )
Theorem	reclt0d 39607	The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> ( 1 / A ) < 0 )
Theorem	lt0neg1dd 39608	If a number is negative, its negative is positive. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> 0 < -u A )
Theorem	mnfled 39609	Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> -oo <_ A )
Theorem	xrleidd 39610	'Less than or equal to' is reflexive for extended reals. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> A <_ A )
Theorem	negelrpd 39611	The negation of a negative number is in the positive real numbers. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> -u A e. RR+ )
Theorem	infxrcld 39612	The infimum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A C_ RR* )   =>    |- ( ph -> inf ( A , RR* , < ) e. RR* )
Theorem	xrralrecnnge 39613*	Show that A is less than B by showing that there is no positive bound on the difference. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- F/ n ph   &    |- ( ph -> A e. RR )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A <_ B <-> A. n e. NN ( A - ( 1 / n ) ) <_ B ) )
Theorem	reclt0 39614	The reciprocal of a negative number is negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( A < 0 <-> ( 1 / A ) < 0 ) )
Theorem	ltmulneg 39615	Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> C < 0 )   =>    |- ( ph -> ( A < B <-> ( B x. C ) < ( A x. C ) ) )
Theorem	allbutfi 39616*	For all but finitely many. Some authors say "cofinitely many". Some authors say "ultimately". Compare with eliuniin 39279 and eliuniin2 39303 (here, the precondition can be dropped; see eliuniincex 39292). (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- Z = ( ZZ>= ` M )   &    |- A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B   =>    |- ( X e. A <-> E. n e. Z A. m e. ( ZZ>= ` n ) X e. B )
Theorem	ltdiv23neg 39617	Swap denominator with other side of 'less than', when both are negative. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B < 0 )   &    |- ( ph -> C e. RR )   &    |- ( ph -> C < 0 )   =>    |- ( ph -> ( ( A / B ) < C <-> ( A / C ) < B ) )
Theorem	xreqnltd 39618	A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> A = B )   =>    |- ( ph -> -. A < B )
Theorem	mnfnre2 39619	Minus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- -. -oo e. RR
Theorem	uzssre 39620	An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ZZ>= ` M ) C_ RR
Theorem	zssxr 39621	The integers are a subset of the extended reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ZZ C_ RR*
Theorem	fisupclrnmpt 39622*	A nonempty finite indexed set contains its supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> R Or A )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> B =/= (/) )   &    |- ( ( ph /\ x e. B ) -> C e. A )   =>    |- ( ph -> sup ( ran ( x e. B |-> C ) , A , R ) e. A )
Theorem	supxrunb3 39623*	The supremum of an unbounded-above set of extended reals is plus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A C_ RR* -> ( A. x e. RR E. y e. A x <_ y <-> sup ( A , RR* , < ) = +oo ) )
Theorem	elfzod 39624	Membership in a half-open integer interval. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> K e. ( ZZ>= ` M ) )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K < N )   =>    |- ( ph -> K e. ( M..^ N ) )
Theorem	fimaxre4 39625*	A nonempty finite set of real numbers is bounded (image set version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> E. y e. RR A. x e. A B <_ y )
Theorem	ren0 39626	The set of reals is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- RR =/= (/)
Theorem	eluzelz2 39627	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> N e. ZZ )
Theorem	pnfnre2 39628	Plus infinity is not a real number. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- -. +oo e. RR
Theorem	resabs2d 39629	Absorption law for restriction. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> B C_ C )   =>    |- ( ph -> ( ( A |` B ) |` C ) = ( A |` B ) )
Theorem	uzid2 39630	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( M e. ( ZZ>= ` N ) -> M e. ( ZZ>= ` M ) )
Theorem	uzidd 39631	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   =>    |- ( ph -> M e. ( ZZ>= ` M ) )
Theorem	supxrleubrnmpt 39632*	The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   &    |- ( ph -> C e. RR* )   =>    |- ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> A. x e. A B <_ C ) )
Theorem	uzssre2 39633	An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   =>    |- Z C_ RR
Theorem	uzssd 39634	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
Theorem	eluzd 39635	Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> M <_ N )   =>    |- ( ph -> N e. Z )
Theorem	elfzd 39636	Membership in a finite set of sequential integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> M <_ K )   &    |- ( ph -> K <_ N )   =>    |- ( ph -> K e. ( M ... N ) )
Theorem	infxrlbrnmpt2 39637*	A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   &    |- ( ph -> C e. A )   &    |- ( ph -> D e. RR* )   &    |- ( x = C -> B = D )   =>    |- ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) <_ D )
Theorem	xrre4 39638	An extended real is real iff it is not an infinty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A e. RR* -> ( A e. RR <-> ( A =/= -oo /\ A =/= +oo ) ) )
Theorem	uz0 39639	The upper integers function applied to a non integer, is the empty set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
Theorem	eluzelz2d 39640	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   =>    |- ( ph -> N e. ZZ )
Theorem	infleinf2 39641*	If any element in B is larger or equal to an element in A, then the infimum of A is smaller or equal to the infimum of B. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B C_ RR* )   &    |- ( ( ph /\ x e. B ) -> E. y e. A y <_ x )   =>    |- ( ph -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
Theorem	unb2ltle 39642*	"Unbounded below" expressed with < and with <_. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A C_ RR* -> ( A. w e. RR E. y e. A y < w <-> A. x e. RR E. y e. A y <_ x ) )
Theorem	uzidd2 39643	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ph -> M e. Z )
Theorem	uzssd2 39644	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> N e. Z )   =>    |- ( ph -> ( ZZ>= ` N ) C_ Z )
Theorem	rexabslelem 39645*	An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) )
Theorem	rexabsle 39646*	An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. w e. RR A. x e. A B <_ w /\ E. z e. RR A. x e. A z <_ B ) ) )
Theorem	allbutfiinf 39647*	Given a "for all but finitely many" condition, the condition holds from N on. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   &    |- A = U_ n e. Z |^|_ m e. ( ZZ>= ` n ) B   &    |- ( ph -> X e. A )   &    |- N = inf ( { n e. Z | A. m e. ( ZZ>= ` n ) X e. B } , RR , < )   =>    |- ( ph -> ( N e. Z /\ A. m e. ( ZZ>= ` N ) X e. B ) )
Theorem	supxrrernmpt 39648*	The real and extended real indexed suprema match when the indexed real supremum exists. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   =>    |- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( x e. A |-> B ) , RR , < ) )
Theorem	suprleubrnmpt 39649*	The supremum of a nonempty bounded indexed set of reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( sup ( ran ( x e. A |-> B ) , RR , < ) <_ C <-> A. x e. A B <_ C ) )
Theorem	infrnmptle 39650*	An indexed infimum of extended reals is smaller than another indexed infimum of extended reals, when every indexed element is smaller than the corresponding one. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   &    |- ( ( ph /\ x e. A ) -> C e. RR* )   &    |- ( ( ph /\ x e. A ) -> B <_ C )   =>    |- ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) <_ inf ( ran ( x e. A |-> C ) , RR* , < ) )
Theorem	infxrunb3 39651*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( A C_ RR* -> ( A. x e. RR E. y e. A y <_ x <-> inf ( A , RR* , < ) = -oo ) )
Theorem	uzn0d 39652	The upper integers are all nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   =>    |- ( ph -> Z =/= (/) )
Theorem	uzssd3 39653	Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> ( ZZ>= ` N ) C_ Z )
Theorem	rexabsle2 39654*	An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( E. y e. RR A. x e. A ( abs ` B ) <_ y <-> ( E. y e. RR A. x e. A B <_ y /\ E. y e. RR A. x e. A y <_ B ) ) )
Theorem	infxrunb3rnmpt 39655*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   =>    |- ( ph -> ( A. y e. RR E. x e. A B <_ y <-> inf ( ran ( x e. A |-> B ) , RR* , < ) = -oo ) )
Theorem	supxrre3rnmpt 39656*	The indexed supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ x ph   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   =>    |- ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) e. RR <-> E. y e. RR A. x e. A B <_ y ) )
Theorem	uzublem 39657*	A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- F/_ j X   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> Y e. RR )   &    |- W = sup ( ran ( j e. ( M ... K ) |-> B ) , RR , < )   &    |- X = if ( W <_ Y , Y , W )   &    |- ( ph -> K e. Z )   &    |- ( ( ph /\ j e. Z ) -> B e. RR )   &    |- ( ph -> A. j e. ( ZZ>= ` K ) B <_ Y )   =>    |- ( ph -> E. x e. RR A. j e. Z B <_ x )
Theorem	uzub 39658*	A set of reals, indexed by upper integers, is bound if and only if any upper part is bound. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
|- F/ j ph   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ( ph /\ j e. Z ) -> B e. RR )   =>    |- ( ph -> ( E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) B <_ x <-> E. x e. RR A. j e. Z B <_ x ) )
Theorem	ssrexr 39659	A subset of the reals is a subset of the extended reals (common case). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ RR )   =>    |- ( ph -> A C_ RR* )
Theorem	supxrmnf2 39660	Removing minus infinity from a set does not affect its supremum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( A C_ RR* -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
Theorem	supxrcli 39661	The supremum of an arbitrary set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- A C_ RR*   =>    |- sup ( A , RR* , < ) e. RR*
Theorem	uzid3 39662	Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- Z = ( ZZ>= ` M )   =>    |- ( N e. Z -> N e. ( ZZ>= ` N ) )
Theorem	infxrlesupxr 39663	The supremum of a nonempty set is larger than or equal to the infimum. The second condition is needed, see supxrltinfxr 39677. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> A =/= (/) )   =>    |- ( ph -> inf ( A , RR* , < ) <_ sup ( A , RR* , < ) )
Theorem	xnegeqd 39664	Equality of two extended numbers with -e in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A = B )   =>    |- ( ph -> -e A = -e B )
Theorem	xnegrecl 39665	The extended real negative of a real number is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( A e. RR -> -e A e. RR )
Theorem	xnegnegi 39666	Extended real version of negneg 10331. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- A e. RR*   =>    |- -e -e A = A
Theorem	xnegeqi 39667	Equality of two extended numbers with -e in front of them. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- A = B   =>    |- -e A = -e B
Theorem	nfxnegd 39668	Deduction version of nfxneg 39691. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/_ x -e A )
Theorem	xnegnegd 39669	Extended real version of negnegd 10383. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> -e -e A = A )
Theorem	uzred 39670	An upper integer is a real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. Z )   =>    |- ( ph -> A e. RR )
Theorem	xnegcli 39671	Closure of extended real negative. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- A e. RR*   =>    |- -e A e. RR*
Theorem	supminfrnmpt 39672*	The indexed supremum of a bounded-above set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   =>    |- ( ph -> sup ( ran ( x e. A |-> B ) , RR , < ) = -uinf ( ran ( x e. A |-> -u B ) , RR , < ) )
Theorem	ceilged 39673	The ceiling of a real number is greater than or equal to that number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   =>    |- ( ph -> A <_ (⌈ ` A ) )
Theorem	infxrpnf 39674	Adding plus infinity to a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( A C_ RR* -> inf ( ( A u. { +oo } ) , RR* , < ) = inf ( A , RR* , < ) )
Theorem	infxrrnmptcl 39675*	The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   =>    |- ( ph -> inf ( ran ( x e. A |-> B ) , RR* , < ) e. RR* )
Theorem	leneg2d 39676	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A <_ -u B <-> B <_ -u A ) )
Theorem	supxrltinfxr 39677	The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- sup ( (/) , RR* , < ) < inf ( (/) , RR* , < )
Theorem	max1d 39678	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> A <_ if ( A <_ B , B , A ) )
Theorem	ceilcld 39679	Closure of the ceiling function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   =>    |- ( ph -> (⌈ ` A ) e. ZZ )
Theorem	supxrleubrnmptf 39680	The supremum of a nonempty bounded indexed set of extended reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- F/_ x A   &    |- F/_ x C   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   &    |- ( ph -> C e. RR* )   =>    |- ( ph -> ( sup ( ran ( x e. A |-> B ) , RR* , < ) <_ C <-> A. x e. A B <_ C ) )
Theorem	nleltd 39681	'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> -. B <_ A )   =>    |- ( ph -> A < B )
Theorem	zxrd 39682	An integer is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. RR* )
Theorem	infxrgelbrnmpt 39683*	The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   &    |- ( ph -> C e. RR* )   =>    |- ( ph -> ( C <_ inf ( ran ( x e. A |-> B ) , RR* , < ) <-> A. x e. A C <_ B ) )
Theorem	rphalfltd 39684	Half of a positive real is less than the original number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A / 2 ) < A )
Theorem	uzssz2 39685	An upper set of integers is a subset of all integers. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- Z = ( ZZ>= ` M )   =>    |- Z C_ ZZ
Theorem	1xr 39686	1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- 1 e. RR*
Theorem	leneg3d 39687	Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( -u A <_ B <-> -u B <_ A ) )
Theorem	max2d 39688	A number is less than or equal to the maximum of it and another. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> B <_ if ( A <_ B , B , A ) )
Theorem	uzn0bi 39689	The upper integers function needs to be applied to an integer, in order to return a nonempty set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ( ZZ>= ` M ) =/= (/) <-> M e. ZZ )
Theorem	xnegrecl2 39690	If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ( A e. RR* /\ -e A e. RR ) -> A e. RR )
Theorem	nfxneg 39691	Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/_ x A   =>    |- F/_ x -e A
Theorem	uzxrd 39692	An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> A e. Z )   =>    |- ( ph -> A e. RR* )
Theorem	infxrpnf2 39693	Removing plus infinity from a set does not affect its infimum. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( A C_ RR* -> inf ( ( A \ { +oo } ) , RR* , < ) = inf ( A , RR* , < ) )
Theorem	supminfxr 39694*	The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ RR )   =>    |- ( ph -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
Theorem	infrpgernmpt 39695*	The infimum of a non empty, bounded below, indexed subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- F/ x ph   &    |- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR* )   &    |- ( ph -> E. y e. RR A. x e. A y <_ B )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> E. x e. A B <_ (inf ( ran ( x e. A |-> B ) , RR* , < ) +e C ) )
Theorem	xnegre 39696	An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( A e. RR* -> ( A e. RR <-> -e A e. RR ) )
Theorem	xnegrecl2d 39697	If the extended real negative is real, then the number itself is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR* )   &    |- ( ph -> -e A e. RR )   =>    |- ( ph -> A e. RR )
Theorem	uzxr 39698	An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( A e. ( ZZ>= ` M ) -> A e. RR* )
Theorem	supminfxr2 39699*	The extended real suprema of a set of extended reals is the extended real negative of the extended real infima of that set's image under extended real negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A C_ RR* )   =>    |- ( ph -> sup ( A , RR* , < ) = -einf ( { x e. RR* | -e x e. A } , RR* , < ) )
Theorem	xnegred 39700	An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> ( A e. RR <-> -e A e. RR ) )