P. 96 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rpdivcld 9501	Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A / B ) e. RR+ )
Theorem	ltrecd 9502	The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
Theorem	lerecd 9503	The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
Theorem	ltrec1d 9504	Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> ( 1 / A ) < B )   =>    |- ( ph -> ( 1 / B ) < A )
Theorem	lerec2d 9505	Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A <_ ( 1 / B ) )   =>    |- ( ph -> B <_ ( 1 / A ) )
Theorem	lediv2ad 9506	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( C / B ) <_ ( C / A ) )
Theorem	ltdiv2d 9507	Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A < B <-> ( C / B ) < ( C / A ) ) )
Theorem	lediv2d 9508	Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( C / B ) <_ ( C / A ) ) )
Theorem	ledivdivd 9509	Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> D e. RR+ )   &    |- ( ph -> ( A / B ) <_ ( C / D ) )   =>    |- ( ph -> ( D / C ) <_ ( B / A ) )
Theorem	divge1 9510	The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
|- ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> 1 <_ ( B / A ) )
Theorem	divlt1lt 9511	A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) < 1 <-> A < B ) )
Theorem	divle1le 9512	A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) <_ 1 <-> A <_ B ) )
Theorem	ledivge1le 9513	If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021.)
|- ( ( A e. RR /\ B e. RR+ /\ ( C e. RR+ /\ 1 <_ C ) ) -> ( A <_ B -> ( A / C ) <_ B ) )
Theorem	ge0p1rpd 9514	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> ( A + 1 ) e. RR+ )
Theorem	rerpdivcld 9515	Closure law for division of a real by a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A / B ) e. RR )
Theorem	ltsubrpd 9516	Subtracting a positive real from another number decreases it. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A - B ) < A )
Theorem	ltaddrpd 9517	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> A < ( A + B ) )
Theorem	ltaddrp2d 9518	Adding a positive number to another number increases it. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> A < ( B + A ) )
Theorem	ltmulgt11d 9519	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( 1 < A <-> B < ( B x. A ) ) )
Theorem	ltmulgt12d 9520	Multiplication by a number greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( 1 < A <-> B < ( A x. B ) ) )
Theorem	gt0divd 9521	Division of a positive number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( 0 < A <-> 0 < ( A / B ) ) )
Theorem	ge0divd 9522	Division of a nonnegative number by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( 0 <_ A <-> 0 <_ ( A / B ) ) )
Theorem	rpgecld 9523	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> B <_ A )   =>    |- ( ph -> A e. RR+ )
Theorem	divge0d 9524	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> 0 <_ A )   =>    |- ( ph -> 0 <_ ( A / B ) )
Theorem	ltmul1d 9525	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
Theorem	ltmul2d 9526	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A < B <-> ( C x. A ) < ( C x. B ) ) )
Theorem	lemul1d 9527	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( A x. C ) <_ ( B x. C ) ) )
Theorem	lemul2d 9528	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )
Theorem	ltdiv1d 9529	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A < B <-> ( A / C ) < ( B / C ) ) )
Theorem	lediv1d 9530	Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( A / C ) <_ ( B / C ) ) )
Theorem	ltmuldivd 9531	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A x. C ) < B <-> A < ( B / C ) ) )
Theorem	ltmuldiv2d 9532	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( C x. A ) < B <-> A < ( B / C ) ) )
Theorem	lemuldivd 9533	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A x. C ) <_ B <-> A <_ ( B / C ) ) )
Theorem	lemuldiv2d 9534	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( C x. A ) <_ B <-> A <_ ( B / C ) ) )
Theorem	ltdivmuld 9535	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A / C ) < B <-> A < ( C x. B ) ) )
Theorem	ltdivmul2d 9536	'Less than' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A / C ) < B <-> A < ( B x. C ) ) )
Theorem	ledivmuld 9537	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A / C ) <_ B <-> A <_ ( C x. B ) ) )
Theorem	ledivmul2d 9538	'Less than or equal to' relationship between division and multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( ( A / C ) <_ B <-> A <_ ( B x. C ) ) )
Theorem	ltmul1dd 9539	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( A x. C ) < ( B x. C ) )
Theorem	ltmul2dd 9540	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( C x. A ) < ( C x. B ) )
Theorem	ltdiv1dd 9541	Division of both sides of 'less than' by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( A / C ) < ( B / C ) )
Theorem	lediv1dd 9542	Division of both sides of a less than or equal to relation by a positive number. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A / C ) <_ ( B / C ) )
Theorem	lediv12ad 9543	Comparison of ratio of two nonnegative numbers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> D e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A <_ B )   &    |- ( ph -> C <_ D )   =>    |- ( ph -> ( A / D ) <_ ( B / C ) )
Theorem	ltdiv23d 9544	Swap denominator with other side of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> ( A / B ) < C )   =>    |- ( ph -> ( A / C ) < B )
Theorem	lediv23d 9545	Swap denominator with other side of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> ( A / B ) <_ C )   =>    |- ( ph -> ( A / C ) <_ B )
Theorem	mul2lt0rlt0 9546	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A x. B ) < 0 )   =>    |- ( ( ph /\ B < 0 ) -> 0 < A )
Theorem	mul2lt0rgt0 9547	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A x. B ) < 0 )   =>    |- ( ( ph /\ 0 < B ) -> A < 0 )
Theorem	mul2lt0llt0 9548	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A x. B ) < 0 )   =>    |- ( ( ph /\ A < 0 ) -> 0 < B )
Theorem	mul2lt0lgt0 9549	If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 2-Oct-2018.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> ( A x. B ) < 0 )   =>    |- ( ( ph /\ 0 < A ) -> B < 0 )
Theorem	mul2lt0np 9550	The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < 0 )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> ( A x. B ) < 0 )
Theorem	mul2lt0pn 9551	The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < 0 )   &    |- ( ph -> 0 < B )   =>    |- ( ph -> ( B x. A ) < 0 )
Theorem	lt2mul2divd 9552	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR+ )   =>    |- ( ph -> ( ( A x. B ) < ( C x. D ) <-> ( A / D ) < ( C / B ) ) )
Theorem	nnledivrp 9553	Division of a positive integer by a positive number is less than or equal to the integer iff the number is greater than or equal to 1. (Contributed by AV, 19-Jun-2021.)
|- ( ( A e. NN /\ B e. RR+ ) -> ( 1 <_ B <-> ( A / B ) <_ A ) )
Theorem	nn0ledivnn 9554	Division of a nonnegative integer by a positive integer is less than or equal to the integer. (Contributed by AV, 19-Jun-2021.)
|- ( ( A e. NN0 /\ B e. NN ) -> ( A / B ) <_ A )
Theorem	addlelt 9555	If the sum of a real number and a positive real number is less than or equal to a third real number, the first real number is less than the third real number. (Contributed by AV, 1-Jul-2021.)
|- ( ( M e. RR /\ N e. RR /\ A e. RR+ ) -> ( ( M + A ) <_ N -> M < N ) )
4.5.2  Infinity and the extended real number system (cont.)
Syntax	cxne 9556	Extend class notation to include the negative of an extended real.
class -e A
Syntax	cxad 9557	Extend class notation to include addition of extended reals.
class +e
Syntax	cxmu 9558	Extend class notation to include multiplication of extended reals.
class xe
Definition	df-xneg 9559	Define the negative of an extended real number. (Contributed by FL, 26-Dec-2011.)
|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
Definition	df-xadd 9560*	Define addition over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- +e = ( x e. RR* , y e. RR* |-> if ( x = +oo , if ( y = -oo , 0 , +oo ) , if ( x = -oo , if ( y = +oo , 0 , -oo ) , if ( y = +oo , +oo , if ( y = -oo , -oo , ( x + y ) ) ) ) ) )
Definition	df-xmul 9561*	Define multiplication over extended real numbers. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- xe = ( x e. RR* , y e. RR* |-> if ( ( x = 0 \/ y = 0 ) , 0 , if ( ( ( ( 0 < y /\ x = +oo ) \/ ( y < 0 /\ x = -oo ) ) \/ ( ( 0 < x /\ y = +oo ) \/ ( x < 0 /\ y = -oo ) ) ) , +oo , if ( ( ( ( 0 < y /\ x = -oo ) \/ ( y < 0 /\ x = +oo ) ) \/ ( ( 0 < x /\ y = -oo ) \/ ( x < 0 /\ y = +oo ) ) ) , -oo , ( x x. y ) ) ) ) )
Theorem	ltxr 9562	The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 14-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> ( ( ( ( A e. RR /\ B e. RR ) /\ A <RR B ) \/ ( A = -oo /\ B = +oo ) ) \/ ( ( A e. RR /\ B = +oo ) \/ ( A = -oo /\ B e. RR ) ) ) ) )
Theorem	elxr 9563	Membership in the set of extended reals. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
Theorem	xrnemnf 9564	An extended real other than minus infinity is real or positive infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )
Theorem	xrnepnf 9565	An extended real other than plus infinity is real or negative infinite. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= +oo ) <-> ( A e. RR \/ A = -oo ) )
Theorem	xrltnr 9566	The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR* -> -. A < A )
Theorem	ltpnf 9567	Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> A < +oo )
Theorem	0ltpnf 9568	Zero is less than plus infinity (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 < +oo
Theorem	mnflt 9569	Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005.)
|- ( A e. RR -> -oo < A )
Theorem	mnflt0 9570	Minus infinity is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- -oo < 0
Theorem	mnfltpnf 9571	Minus infinity is less than plus infinity. (Contributed by NM, 14-Oct-2005.)
|- -oo < +oo
Theorem	mnfltxr 9572	Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006.)
|- ( ( A e. RR \/ A = +oo ) -> -oo < A )
Theorem	pnfnlt 9573	No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)
|- ( A e. RR* -> -. +oo < A )
Theorem	nltmnf 9574	No extended real is less than minus infinity. (Contributed by NM, 15-Oct-2005.)
|- ( A e. RR* -> -. A < -oo )
Theorem	pnfge 9575	Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
|- ( A e. RR* -> A <_ +oo )
Theorem	0lepnf 9576	0 less than or equal to positive infinity. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- 0 <_ +oo
Theorem	nn0pnfge0 9577	If a number is a nonnegative integer or positive infinity, it is greater than or equal to 0. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
|- ( ( N e. NN0 \/ N = +oo ) -> 0 <_ N )
Theorem	mnfle 9578	Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006.)
|- ( A e. RR* -> -oo <_ A )
Theorem	xrltnsym 9579	Ordering on the extended reals is not symmetric. (Contributed by NM, 15-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> -. B < A ) )
Theorem	xrltnsym2 9580	'Less than' is antisymmetric and irreflexive for extended reals. (Contributed by NM, 6-Feb-2007.)
|- ( ( A e. RR* /\ B e. RR* ) -> -. ( A < B /\ B < A ) )
Theorem	xrlttr 9581	Ordering on the extended reals is transitive. (Contributed by NM, 15-Oct-2005.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B < C ) -> A < C ) )
Theorem	xrltso 9582	'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)
|- < Or RR*
Theorem	xrlttri3 9583	Extended real version of lttri3 7844. (Contributed by NM, 9-Feb-2006.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
Theorem	xrltle 9584	'Less than' implies 'less than or equal' for extended reals. (Contributed by NM, 19-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> A <_ B ) )
Theorem	xrltled 9585	'Less than' implies 'less than or equal to' for extended reals. Deduction form of xrltle 9584. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> A <_ B )
Theorem	xrleid 9586	'Less than or equal to' is reflexive for extended reals. (Contributed by NM, 7-Feb-2007.)
|- ( A e. RR* -> A <_ A )
Theorem	xrleidd 9587	'Less than or equal to' is reflexive for extended reals. Deduction form of xrleid 9586. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> A <_ A )
Theorem	xrletri3 9588	Trichotomy law for extended reals. (Contributed by FL, 2-Aug-2009.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
Theorem	xrlelttr 9589	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
Theorem	xrltletr 9590	Transitive law for ordering on extended reals. (Contributed by NM, 19-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
Theorem	xrletr 9591	Transitive law for ordering on extended reals. (Contributed by NM, 9-Feb-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )
Theorem	xrlttrd 9592	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A < B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	xrlelttrd 9593	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B < C )   =>    |- ( ph -> A < C )
Theorem	xrltletrd 9594	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A < B )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> A < C )
Theorem	xrletrd 9595	Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> C e. RR* )   &    |- ( ph -> A <_ B )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> A <_ C )
Theorem	xrltne 9596	'Less than' implies not equal for extended reals. (Contributed by NM, 20-Jan-2006.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B =/= A )
Theorem	nltpnft 9597	An extended real is not less than plus infinity iff they are equal. (Contributed by NM, 30-Jan-2006.)
|- ( A e. RR* -> ( A = +oo <-> -. A < +oo ) )
Theorem	npnflt 9598	An extended real is less than plus infinity iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.)
|- ( A e. RR* -> ( A < +oo <-> A =/= +oo ) )
Theorem	xgepnf 9599	An extended real which is greater than plus infinity is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
|- ( A e. RR* -> ( +oo <_ A <-> A = +oo ) )
Theorem	ngtmnft 9600	An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
|- ( A e. RR* -> ( A = -oo <-> -. -oo < A ) )