P. 98 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rpne0 9701	A positive real is nonzero. (Contributed by NM, 18-Jul-2008.)
|- ( A e. RR+ -> A =/= 0 )
Theorem	rpap0 9702	A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> A # 0 )
Theorem	rprene0 9703	A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. RR /\ A =/= 0 ) )
Theorem	rpreap0 9704	A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> ( A e. RR /\ A # 0 ) )
Theorem	rpcnne0 9705	A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.)
|- ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
Theorem	rpcnap0 9706	A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.)
|- ( A e. RR+ -> ( A e. CC /\ A # 0 ) )
Theorem	ralrp 9707	Quantification over positive reals. (Contributed by NM, 12-Feb-2008.)
|- ( A. x e. RR+ ph <-> A. x e. RR ( 0 < x -> ph ) )
Theorem	rexrp 9708	Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.)
|- ( E. x e. RR+ ph <-> E. x e. RR ( 0 < x /\ ph ) )
Theorem	rpaddcl 9709	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A + B ) e. RR+ )
Theorem	rpmulcl 9710	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A x. B ) e. RR+ )
Theorem	rpdivcl 9711	Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A / B ) e. RR+ )
Theorem	rpreccl 9712	Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.)
|- ( A e. RR+ -> ( 1 / A ) e. RR+ )
Theorem	rphalfcl 9713	Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.)
|- ( A e. RR+ -> ( A / 2 ) e. RR+ )
Theorem	rpgecl 9714	A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ( A e. RR+ /\ B e. RR /\ A <_ B ) -> B e. RR+ )
Theorem	rphalflt 9715	Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.)
|- ( A e. RR+ -> ( A / 2 ) < A )
Theorem	rerpdivcl 9716	Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
Theorem	ge0p1rp 9717	A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A + 1 ) e. RR+ )
Theorem	rpnegap 9718	Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.)
|- ( ( A e. RR /\ A # 0 ) -> ( A e. RR+ \/_ -u A e. RR+ ) )
Theorem	negelrp 9719	Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.)
|- ( A e. RR -> ( -u A e. RR+ <-> A < 0 ) )
Theorem	negelrpd 9720	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	0nrp 9721	Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.)
|- -. 0 e. RR+
Theorem	ltsubrp 9722	Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A - B ) < A )
Theorem	ltaddrp 9723	Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.)
|- ( ( A e. RR /\ B e. RR+ ) -> A < ( A + B ) )
Theorem	difrp 9724	Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( B - A ) e. RR+ ) )
Theorem	elrpd 9725	Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 < A )   =>    |- ( ph -> A e. RR+ )
Theorem	nnrpd 9726	A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. RR+ )
Theorem	zgt1rpn0n1 9727	An integer greater than 1 is a positive real number not equal to 0 or 1. Useful for working with integer logarithm bases (which is a common case, e.g., base 2, base 3, or base 10). (Contributed by Thierry Arnoux, 26-Sep-2017.) (Proof shortened by AV, 9-Jul-2022.)
|- ( B e. ( ZZ>= ` 2 ) -> ( B e. RR+ /\ B =/= 0 /\ B =/= 1 ) )
Theorem	rpred 9728	A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR )
Theorem	rpxrd 9729	A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. RR* )
Theorem	rpcnd 9730	A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A e. CC )
Theorem	rpgt0d 9731	A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 < A )
Theorem	rpge0d 9732	A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> 0 <_ A )
Theorem	rpne0d 9733	A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A =/= 0 )
Theorem	rpap0d 9734	A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> A # 0 )
Theorem	rpregt0d 9735	A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. RR /\ 0 < A ) )
Theorem	rprege0d 9736	A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. RR /\ 0 <_ A ) )
Theorem	rprene0d 9737	A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. RR /\ A =/= 0 ) )
Theorem	rpcnne0d 9738	A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A e. CC /\ A =/= 0 ) )
Theorem	rpreccld 9739	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( 1 / A ) e. RR+ )
Theorem	rprecred 9740	Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	rphalfcld 9741	Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A / 2 ) e. RR+ )
Theorem	reclt1d 9742	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A < 1 <-> 1 < ( 1 / A ) ) )
Theorem	recgt1d 9743	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( 1 < A <-> ( 1 / A ) < 1 ) )
Theorem	rpaddcld 9744	Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A + B ) e. RR+ )
Theorem	rpmulcld 9745	Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A x. B ) e. RR+ )
Theorem	rpdivcld 9746	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 9747	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 9748	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 9749	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 9750	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 9751	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 9752	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 9753	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 9754	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 9755	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 9756	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 9757	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 9758	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 9759	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 9760	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 9761	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 9762	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 9763	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 9764	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 9765	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 9766	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 9767	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 9768	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 9769	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 9770	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 9771	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 9772	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 9773	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 9774	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 9775	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 9776	'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 9777	'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 9778	'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 9779	'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 9780	'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 9781	'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 9782	'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 9783	'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 9784	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 9785	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 9786	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 9787	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 9788	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 9789	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 9790	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 9791	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 9792	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 9793	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 9794	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 9795	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 9796	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 9797	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 9798	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 9799	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 9800	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 ) )