P. 396 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39501-39600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	reopn 39501	The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- RR e. ( topGen ` ran (,) )
Theorem	elfzop1le2 39502	A member in a half-open integer interval plus 1 is less or equal than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( K e. ( M..^ N ) -> ( K + 1 ) <_ N )
Theorem	sub31 39503	Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( C - ( B - A ) ) )
Theorem	nnne1ge2 39504	A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( N e. NN /\ N =/= 1 ) -> 2 <_ N )
Theorem	lefldiveq 39505	A closed enough, smaller real C has the same floor of A when both are divided by B. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. ( ( A - ( A mod B ) ) [,] A ) )   =>    |- ( ph -> ( |_ ` ( A / B ) ) = ( |_ ` ( C / B ) ) )
Theorem	negsubdi3d 39506	Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( -u A - -u B ) )
Theorem	ltdiv2dd 39507	Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( C / B ) < ( C / A ) )
Theorem	absnpncand 39508	Triangular inequality, combined with cancellation law for subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by abs3difd 14199, and absnpncand 39508 should be deleted afterwards.
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( abs ` ( A - C ) ) <_ ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) )
Theorem	abssinbd 39509	Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> ( abs ` ( sin ` A ) ) <_ 1 )
Theorem	halffl 39510	Floor of ( 1 / 2 ). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( |_ ` ( 1 / 2 ) ) = 0
Theorem	monoords 39511*	Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( M..^ N ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )   &    |- ( ph -> I e. ( M ... N ) )   &    |- ( ph -> J e. ( M ... N ) )   &    |- ( ph -> I < J )   =>    |- ( ph -> ( F ` I ) < ( F ` J ) )
Theorem	hashssle 39512	The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by hashss 13197, and hashssle 39512 should be deleted afterwards.
|- ( ( A e. Fin /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) )
Theorem	lttri5d 39513	Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A =/= B )   &    |- ( ph -> -. B < A )   =>    |- ( ph -> A < B )
Theorem	fzisoeu 39514*	A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 13246 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> H e. Fin )   &    |- ( ph -> < Or H )   &    |- ( ph -> M e. ZZ )   &    |- N = ( ( # ` H ) + ( M - 1 ) )   =>    |- ( ph -> E! f f Isom < , < ( ( M ... N ) , H ) )
Theorem	lt3addmuld 39515	If three real numbers are less than a fourth real number, the sum of the three real numbers is less than three times the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < D )   &    |- ( ph -> B < D )   &    |- ( ph -> C < D )   =>    |- ( ph -> ( ( A + B ) + C ) < ( 3 x. D ) )
Theorem	absnpncan2d 39516	Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( abs ` ( A - D ) ) <_ ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) )
Theorem	fperiodmullem 39517*	A function with period T is also periodic with period nonnegative multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> CC )   &    |- ( ph -> T e. RR )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> X e. RR )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   =>    |- ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )
Theorem	fperiodmul 39518*	A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> CC )   &    |- ( ph -> T e. RR )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> X e. RR )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   =>    |- ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )
Theorem	upbdrech 39519*	Choice of an upper bound for a non empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   &    |- C = sup ( { z | E. x e. A z = B } , RR , < )   =>    |- ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )
Theorem	lt4addmuld 39520	If four real numbers are less than a fifth real number, the sum of the four real numbers is less than four times the fifth real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> E e. RR )   &    |- ( ph -> A < E )   &    |- ( ph -> B < E )   &    |- ( ph -> C < E )   &    |- ( ph -> D < E )   =>    |- ( ph -> ( ( ( A + B ) + C ) + D ) < ( 4 x. E ) )
Theorem	absnpncan3d 39521	Triangular inequality, combined with cancellation law for subtraction (applied three times). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> E e. CC )   =>    |- ( ph -> ( abs ` ( A - E ) ) <_ ( ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) + ( abs ` ( D - E ) ) ) )
Theorem	upbdrech2 39522*	Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   &    |- C = if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) )   =>    |- ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )
Theorem	ssfiunibd 39523*	A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ z e. U. A ) -> B e. RR )   &    |- ( ( ph /\ x e. A ) -> E. y e. RR A. z e. x B <_ y )   &    |- ( ph -> C C_ U. A )   =>    |- ( ph -> E. w e. RR A. z e. C B <_ w )
Theorem	fz1ssfz0 39524	Subset relationship for finite sets of sequential integers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( 1 ... N ) C_ ( 0 ... N )
Theorem	fzdifsuc2 39525	Remove a successor from the end of a finite set of sequential integers. Similar to fzdifsuc 12400, but with a weaker condition. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( N e. ( ZZ>= ` ( M - 1 ) ) -> ( M ... N ) = ( ( M ... ( N + 1 ) ) \ { ( N + 1 ) } ) )
Theorem	fzsscn 39526	A finite sequence of integers is a set of complex numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( M ... N ) C_ CC
Theorem	divcan8d 39527	A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( B / ( A x. B ) ) = ( 1 / A ) )
Theorem	dmmcand 39528	Cancellation law for division and multiplication. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. ( B x. C ) ) = ( A x. C ) )
Theorem	fzssre 39529	A finite sequence of integers is a set of real numbers. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( M ... N ) C_ RR
Theorem	elfzelzd 39530	A member of a finite set of sequential integer is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> K e. ( M ... N ) )   =>    |- ( ph -> K e. ZZ )
Theorem	bccld 39531	A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> N e. NN0 )   &    |- ( ph -> K e. ZZ )   =>    |- ( ph -> ( N _C K ) e. NN0 )
Theorem	leadd12dd 39532	Addition to both sides of 'less than or equal to'. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A + B ) <_ ( C + D ) )
Theorem	fzssnn0 39533	A finite set of sequential integers that is a subset of NN0. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( 0 ... N ) C_ NN0
Theorem	xreqle 39534	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( A e. RR* /\ A = B ) -> A <_ B )
Theorem	xaddid2d 39535	0 is a left identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> ( 0 +e A ) = A )
Theorem	xadd0ge 39536	A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> A <_ ( A +e B ) )
Theorem	elfzolem1 39537	A member in a half-open integer interval is less than or equal to the upper bound minus 1 . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( K e. ( M..^ N ) -> K <_ ( N - 1 ) )
Theorem	xrgtned 39538	'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> B =/= A )
Theorem	xrleneltd 39539	'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A <_ B )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> A < B )
Theorem	xaddcomd 39540	The extended real addition operation is commutative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A +e B ) = ( B +e A ) )
Theorem	supxrre3 39541*	The supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( A C_ RR /\ A =/= (/) ) -> ( sup ( A , RR* , < ) e. RR <-> E. x e. RR A. y e. A y <_ x ) )
Theorem	uzfissfz 39542*	For any finite subset of the upper integers, there is a finite set of sequential integers that includes it. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> A C_ Z )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> E. k e. Z A C_ ( M ... k ) )
Theorem	xleadd2d 39543	Addition of extended reals preserves the "less than or equal" relation, in the right slot. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C +e A ) <_ ( C +e B ) )
Theorem	suprltrp 39544*	The supremum of a nonempty bounded set of reals can be approximated from below by elements of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> X e. RR+ )   =>    |- ( ph -> E. z e. A ( sup ( A , RR , < ) - X ) < z )
Theorem	xleadd1d 39545	Addition of extended reals preserves the "less than or equal" relation, in the left slot. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A +e C ) <_ ( B +e C ) )
Theorem	xreqled 39546	Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> A = B )   =>    |- ( ph -> A <_ B )
Theorem	xrgepnfd 39547	An extended real greater or equal to +oo is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> +oo <_ A )   =>    |- ( ph -> A = +oo )
Theorem	xrge0nemnfd 39548	A nonnegative extended real is not minus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. ( 0 [,] +oo ) )   =>    |- ( ph -> A =/= -oo )
Theorem	supxrgere 39549*	If a real number can be approximated from below by members of a set, then it is smaller or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B e. RR )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. A ( B - x ) < y )   =>    |- ( ph -> B <_ sup ( A , RR* , < ) )
Theorem	iuneqfzuzlem 39550*	Lemma for iuneqfzuz 39551: here, inclusion is proven; aiuneqfzuz uses this lemma twice, to prove equality. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- Z = ( ZZ>= ` N )   =>    |- ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z A C_ U_ n e. Z B )
Theorem	iuneqfzuz 39551*	If two unions indexed by upper integers are equal if they agree on any partial indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- Z = ( ZZ>= ` N )   =>    |- ( A. m e. Z U_ n e. ( N ... m ) A = U_ n e. ( N ... m ) B -> U_ n e. Z A = U_ n e. Z B )
Theorem	xle2addd 39552	Adding both side of two inequalities. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> D e. RR* )   &    |- ( ph -> A <_ C )   &    |- ( ph -> B <_ D )   =>    |- ( ph -> ( A +e B ) <_ ( C +e D ) )
Theorem	supxrgelem 39553*	If an extended real number can be approximated from below by members of a set, then it is smaller or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. A B < ( y +e x ) )   =>    |- ( ph -> B <_ sup ( A , RR* , < ) )
Theorem	supxrge 39554*	If an extended real number can be approximated from below by members of a set, then it is smaller or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ( ph /\ x e. RR+ ) -> E. y e. A B <_ ( y +e x ) )   =>    |- ( ph -> B <_ sup ( A , RR* , < ) )
Theorem	suplesup 39555*	If any element of A can be approximated from below by members of B, then the supremum of A is smaller or equal to the supremum of B. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> B C_ RR* )   &    |- ( ph -> A. x e. A A. y e. RR+ E. z e. B ( x - y ) < z )   =>    |- ( ph -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
Theorem	infxrglb 39556*	The infimum of a set of extended reals is less than an extended real if and only if the set contains a smaller number. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A C_ RR* /\ B e. RR* ) -> (inf ( A , RR* , < ) < B <-> E. x e. A x < B ) )
Theorem	xadd0ge2 39557	A number is less than or equal to itself plus a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> A <_ ( B +e A ) )
Theorem	nepnfltpnf 39558	An extended real that is not +oo is less than +oo. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A =/= +oo )   &    |- ( ph -> A e. RR* )   =>    |- ( ph -> A < +oo )
Theorem	ltadd12dd 39559	Addition to both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B < D )   =>    |- ( ph -> ( A + B ) < ( C + D ) )
Theorem	nemnftgtmnft 39560	An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A e. RR* /\ A =/= -oo ) -> -oo < A )
Theorem	xrgtso 39561	'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- `' < Or RR*
Theorem	rpex 39562	The positive reals form a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- RR+ e. _V
Theorem	xrge0ge0 39563	A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( A e. ( 0 [,] +oo ) -> 0 <_ A )
Theorem	xrssre 39564	A subset of extended reals that does not contain +oo and -oo is a subset of the reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> -. +oo e. A )   &    |- ( ph -> -. -oo e. A )   =>    |- ( ph -> A C_ RR )
Theorem	ssuzfz 39565	A finite subset of the upper integers is a subset of a finite set of sequential integers. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> A C_ Z )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> A C_ ( M ... sup ( A , RR , < ) ) )
Theorem	absfun 39566	The absolute value is a function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- Fun abs
Theorem	infrpge 39567*	The infimum of a non empty, bounded subset of extended reals can be approximated from above by an element of the set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A x <_ y )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> E. z e. A z <_ (inf ( A , RR* , < ) +e B ) )
Theorem	xrlexaddrp 39568*	If an extended real number A can be approximated from above, adding positive reals to B, then A is smaller or equal than B. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ( ph /\ x e. RR+ ) -> A <_ ( B +e x ) )   =>    |- ( ph -> A <_ B )
Theorem	supsubc 39569*	The supremum function distributes over subtraction in a sense similar to that in supaddc 10990. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A C_ RR )   &    |- ( ph -> A =/= (/) )   &    |- ( ph -> E. x e. RR A. y e. A y <_ x )   &    |- ( ph -> B e. RR )   &    |- C = { z | E. v e. A z = ( v - B ) }   =>    |- ( ph -> ( sup ( A , RR , < ) - B ) = sup ( C , RR , < ) )
Theorem	xralrple2 39570*	Show that A is less than B by showing that there is no positive bound on the difference. A variant on xralrple 12036. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ x ph   &    |- ( ph -> A e. RR* )   &    |- ( ph -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( ( 1 + x ) x. B ) ) )
Theorem	nnuzdisj 39571	The first N elements of the set of nonnegative integers are distinct from any later members. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ( 1 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)
Theorem	ltdivgt1 39572	Divsion by a number greater than 1. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( 1 < B <-> ( A / B ) < A ) )
Theorem	xrltned 39573	'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> A =/= B )
Theorem	nnsplit 39574	Express the set of positive integers as the disjoint (see nnuzdisj 39571) union of the first N values and the rest. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( N e. NN -> NN = ( ( 1 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
Theorem	divdiv3d 39575	Division into a fraction. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / B ) / C ) = ( A / ( C x. B ) ) )
Theorem	abslt2sqd 39576	Comparison of the square of two numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( abs ` A ) < ( abs ` B ) )   =>    |- ( ph -> ( A ^ 2 ) < ( B ^ 2 ) )
Theorem	qenom 39577	The set of rational numbers is equinumerous to omega (the set of finite ordinal numbers). (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- QQ ~~ om
Theorem	qct 39578	The set of rational numbers is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- QQ ~<_ om
Theorem	xrltnled 39579	'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A < B <-> -. B <_ A ) )
Theorem	lenlteq 39580	'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> -. A < B )   =>    |- ( ph -> A = B )
Theorem	xrred 39581	An extended real that is neither minus infinity, nor plus infinity, is real. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. RR* )   &    |- ( ph -> A =/= -oo )   &    |- ( ph -> A =/= +oo )   =>    |- ( ph -> A e. RR )
Theorem	rr2sscn2 39582	ℝ^ 2 is a subset of CC^ 2. Common case. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( RR X. RR ) C_ ( CC X. CC )
Theorem	infxr 39583*	The infimum of a set of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ x ph   &    |- F/ y ph   &    |- ( ph -> A C_ RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A. x e. A -. x < B )   &    |- ( ph -> A. x e. RR ( B < x -> E. y e. A y < x ) )   =>    |- ( ph -> inf ( A , RR* , < ) = B )
Theorem	infxrunb2 39584*	The infimum of an unbounded-below set of extended reals is minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( A C_ RR* -> ( A. x e. RR E. y e. A y < x <-> inf ( A , RR* , < ) = -oo ) )
Theorem	infxrbnd2 39585*	The infimum of a bounded-below set of extended reals is greater than minus infinity. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( A C_ RR* -> ( E. x e. RR A. y e. A x <_ y <-> -oo < inf ( A , RR* , < ) ) )
Theorem	infleinflem1 39586	Lemma for infleinf 39588, case B =/= (/) /\ -oo < inf ( B , RR* , < ). (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> B C_ RR* )   &    |- ( ph -> W e. RR+ )   &    |- ( ph -> X e. B )   &    |- ( ph -> X <_ (inf ( B , RR* , < ) +e ( W / 2 ) ) )   &    |- ( ph -> Z e. A )   &    |- ( ph -> Z <_ ( X +e ( W / 2 ) ) )   =>    |- ( ph -> inf ( A , RR* , < ) <_ (inf ( B , RR* , < ) +e W ) )
Theorem	infleinflem2 39587	Lemma for infleinf 39588, when inf ( B , RR* , < ) = -oo. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> B C_ RR* )   &    |- ( ph -> R e. RR )   &    |- ( ph -> X e. B )   &    |- ( ph -> X < ( R - 2 ) )   &    |- ( ph -> Z e. A )   &    |- ( ph -> Z <_ ( X +e 1 ) )   =>    |- ( ph -> Z < R )
Theorem	infleinf 39588*	If any element of B can be approximated from above by members of A, then the infimum of A is smaller or equal to the infimum of B. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> B C_ RR* )   &    |- ( ( ph /\ x e. B /\ y e. RR+ ) -> E. z e. A z <_ ( x +e y ) )   =>    |- ( ph -> inf ( A , RR* , < ) <_ inf ( B , RR* , < ) )
Theorem	xralrple4 39589*	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.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( B + ( x ^ N ) ) ) )
Theorem	xralrple3 39590*	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.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> 0 <_ C )   =>    |- ( ph -> ( A <_ B <-> A. x e. RR+ A <_ ( B + ( C x. x ) ) ) )
Theorem	eluzelzd 39591	A member of an upper set of integers is an integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> N e. ( ZZ>= ` M ) )   =>    |- ( ph -> N e. ZZ )
Theorem	suplesup2 39592*	If any element of A is smaller or equal to an element in B, then the supremum of A is smaller or equal to the supremum of B. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ph -> A C_ RR* )   &    |- ( ph -> B C_ RR* )   &    |- ( ( ph /\ x e. A ) -> E. y e. B x <_ y )   =>    |- ( ph -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )
Theorem	recnnltrp 39593	N is a natural number large enough that its reciprocal is smaller than the given positive E. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- N = ( ( |_ ` ( 1 / E ) ) + 1 )   =>    |- ( E e. RR+ -> ( N e. NN /\ ( 1 / N ) < E ) )
Theorem	fiminre2 39594*	A nonempty finite set of real numbers is bounded below. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A x <_ y )
Theorem	nnn0 39595	The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- NN =/= (/)
Theorem	fzct 39596	A finite set of sequential integer is countable. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( N ... M ) ~<_ om
Theorem	rpgtrecnn 39597*	Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( A e. RR+ -> E. n e. NN ( 1 / n ) < A )
Theorem	fzossuz 39598	A half-open integer interval is a subset of an upper set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( M..^ N ) C_ ( ZZ>= ` M )
Theorem	fzossz 39599	A half-open integer interval is a set of integers. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( M..^ N ) C_ ZZ
Theorem	infrefilb 39600	The infimum of a finite set of reals is less than or equal to any of its elements. (Contributed by Glauco Siliprandi, 8-Apr-2021.)
|- ( ( B C_ RR /\ B e. Fin /\ A e. B ) -> inf ( B , RR , < ) <_ A )