P. 83 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divcanap4d 8201	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A x. B ) / B ) = A )
Theorem	diveqap0d 8202	If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> ( A / B ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	diveqap1d 8203	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> ( A / B ) = 1 )   =>    |- ( ph -> A = B )
Theorem	diveqap1ad 8204	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 8111. Generalization of diveqap1d 8203. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) = 1 <-> A = B ) )
Theorem	diveqap0ad 8205	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 8088. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) = 0 <-> A = 0 ) )
Theorem	divap1d 8206	If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> A # B )   =>    |- ( ph -> ( A / B ) # 1 )
Theorem	divap0bd 8207	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A # 0 <-> ( A / B ) # 0 ) )
Theorem	divnegapd 8208	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> -u ( A / B ) = ( -u A / B ) )
Theorem	divneg2apd 8209	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> -u ( A / B ) = ( A / -u B ) )
Theorem	div2negapd 8210	Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( -u A / -u B ) = ( A / B ) )
Theorem	divap0d 8211	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / B ) # 0 )
Theorem	recdivapd 8212	The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( 1 / ( A / B ) ) = ( B / A ) )
Theorem	recdivap2d 8213	Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
Theorem	divcanap6d 8214	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) x. ( B / A ) ) = 1 )
Theorem	ddcanapd 8215	Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / ( A / B ) ) = B )
Theorem	rec11apd 8216	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> B # 0 )   &    |- ( ph -> ( 1 / A ) = ( 1 / B ) )   =>    |- ( ph -> A = B )
Theorem	divmulapd 8217	Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) = C <-> ( B x. C ) = A ) )
Theorem	div32apd 8218	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) x. C ) = ( A x. ( C / B ) ) )
Theorem	div13apd 8219	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( ( A / B ) x. C ) = ( ( C / B ) x. A ) )
Theorem	divdiv32apd 8220	Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-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 ) / B ) )
Theorem	divcanap5d 8221	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( C x. A ) / ( C x. B ) ) = ( A / B ) )
Theorem	divcanap5rd 8222	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A x. C ) / ( B x. C ) ) = ( A / B ) )
Theorem	divcanap7d 8223	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A / C ) / ( B / C ) ) = ( A / B ) )
Theorem	dmdcanapd 8224	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( B / C ) x. ( A / B ) ) = ( A / C ) )
Theorem	dmdcanap2d 8225	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A / B ) x. ( B / C ) ) = ( A / C ) )
Theorem	divdivap1d 8226	Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A / B ) / C ) = ( A / ( B x. C ) ) )
Theorem	divdivap2d 8227	Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( A / ( B / C ) ) = ( ( A x. C ) / B ) )
Theorem	divmulap2d 8228	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( C x. B ) ) )
Theorem	divmulap3d 8229	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( B x. C ) ) )
Theorem	divassapd 8230	An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A x. B ) / C ) = ( A x. ( B / C ) ) )
Theorem	div12apd 8231	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( A x. ( B / C ) ) = ( B x. ( A / C ) ) )
Theorem	div23apd 8232	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A x. B ) / C ) = ( ( A / C ) x. B ) )
Theorem	divdirapd 8233	Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divsubdirapd 8234	Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   =>    |- ( ph -> ( ( A - B ) / C ) = ( ( A / C ) - ( B / C ) ) )
Theorem	div11apd 8235	One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C # 0 )   &    |- ( ph -> ( A / C ) = ( B / C ) )   =>    |- ( ph -> A = B )
Theorem	divmuldivapd 8236	Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B # 0 )   &    |- ( ph -> D # 0 )   =>    |- ( ph -> ( ( A / B ) x. ( C / D ) ) = ( ( A x. C ) / ( B x. D ) ) )
Theorem	rerecclapd 8237	Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> A # 0 )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	redivclapd 8238	Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B # 0 )   =>    |- ( ph -> ( A / B ) e. RR )
Theorem	mvllmulapd 8239	Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A # 0 )   &    |- ( ph -> ( A x. B ) = C )   =>    |- ( ph -> B = ( C / A ) )
3.3.9  Ordering on reals (cont.)
Theorem	ltp1 8240	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- ( A e. RR -> A < ( A + 1 ) )
Theorem	lep1 8241	A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006.)
|- ( A e. RR -> A <_ ( A + 1 ) )
Theorem	ltm1 8242	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|- ( A e. RR -> ( A - 1 ) < A )
Theorem	lem1 8243	A number minus 1 is less than or equal to itself. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- ( A e. RR -> ( A - 1 ) <_ A )
Theorem	letrp1 8244	A transitive property of 'less than or equal' and plus 1. (Contributed by NM, 5-Aug-2005.)
|- ( ( A e. RR /\ B e. RR /\ A <_ B ) -> A <_ ( B + 1 ) )
Theorem	p1le 8245	A transitive property of plus 1 and 'less than or equal'. (Contributed by NM, 16-Aug-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( A + 1 ) <_ B ) -> A <_ B )
Theorem	recgt0 8246	The reciprocal of a positive number is positive. Exercise 4 of [Apostol] p. 21. (Contributed by NM, 25-Aug-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )
Theorem	prodgt0gt0 8247	Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 8248 for the same theorem with 0 < A replaced by the weaker condition 0 <_ A. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 < ( A x. B ) ) ) -> 0 < B )
Theorem	prodgt0 8248	Infer that a multiplicand is positive from a nonnegative multiplier and positive product. (Contributed by NM, 24-Apr-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 < ( A x. B ) ) ) -> 0 < B )
Theorem	prodgt02 8249	Infer that a multiplier is positive from a nonnegative multiplicand and positive product. (Contributed by NM, 24-Apr-2005.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ B /\ 0 < ( A x. B ) ) ) -> 0 < A )
Theorem	prodge0 8250	Infer that a multiplicand is nonnegative from a positive multiplier and nonnegative product. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < A /\ 0 <_ ( A x. B ) ) ) -> 0 <_ B )
Theorem	prodge02 8251	Infer that a multiplier is nonnegative from a positive multiplicand and nonnegative product. (Contributed by NM, 2-Jul-2005.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 < B /\ 0 <_ ( A x. B ) ) ) -> 0 <_ A )
Theorem	ltmul2 8252	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( C x. A ) < ( C x. B ) ) )
Theorem	lemul2 8253	Multiplication of both sides of 'less than or equal to' by a positive number. (Contributed by NM, 16-Mar-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( C x. A ) <_ ( C x. B ) ) )
Theorem	lemul1a 8254	Multiplication of both sides of 'less than or equal to' by a nonnegative number. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 21-Feb-2005.)
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( A x. C ) <_ ( B x. C ) )
Theorem	lemul2a 8255	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C x. A ) <_ ( C x. B ) )
Theorem	ltmul12a 8256	Comparison of product of two positive numbers. (Contributed by NM, 30-Dec-2005.)
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 <_ C /\ C < D ) ) ) -> ( A x. C ) < ( B x. D ) )
Theorem	lemul12b 8257	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
|- ( ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) /\ ( C e. RR /\ ( D e. RR /\ 0 <_ D ) ) ) -> ( ( A <_ B /\ C <_ D ) -> ( A x. C ) <_ ( B x. D ) ) )
Theorem	lemul12a 8258	Comparison of product of two nonnegative numbers. (Contributed by NM, 22-Feb-2008.)
|- ( ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR ) /\ ( ( C e. RR /\ 0 <_ C ) /\ D e. RR ) ) -> ( ( A <_ B /\ C <_ D ) -> ( A x. C ) <_ ( B x. D ) ) )
Theorem	mulgt1 8259	The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 < ( A x. B ) )
Theorem	ltmulgt11 8260	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )
Theorem	ltmulgt12 8261	Multiplication by a number greater than 1. (Contributed by NM, 24-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( B x. A ) ) )
Theorem	lemulge11 8262	Multiplication by a number greater than or equal to 1. (Contributed by NM, 17-Dec-2005.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ ( A x. B ) )
Theorem	lemulge12 8263	Multiplication by a number greater than or equal to 1. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 1 <_ B ) ) -> A <_ ( B x. A ) )
Theorem	ltdiv1 8264	Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A / C ) < ( B / C ) ) )
Theorem	lediv1 8265	Division of both sides of a less than or equal to relation by a positive number. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( A / C ) <_ ( B / C ) ) )
Theorem	gt0div 8266	Division of a positive number by a positive number. (Contributed by NM, 28-Sep-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( 0 < A <-> 0 < ( A / B ) ) )
Theorem	ge0div 8267	Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005.)
|- ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( 0 <_ A <-> 0 <_ ( A / B ) ) )
Theorem	divgt0 8268	The ratio of two positive numbers is positive. (Contributed by NM, 12-Oct-1999.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 < ( A / B ) )
Theorem	divge0 8269	The ratio of nonnegative and positive numbers is nonnegative. (Contributed by NM, 27-Sep-1999.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) )
Theorem	ltmuldiv 8270	'Less than' relationship between division and multiplication. (Contributed by NM, 12-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) < B <-> A < ( B / C ) ) )
Theorem	ltmuldiv2 8271	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. A ) < B <-> A < ( B / C ) ) )
Theorem	ltdivmul 8272	'Less than' relationship between division and multiplication. (Contributed by NM, 18-Nov-2004.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < B <-> A < ( C x. B ) ) )
Theorem	ledivmul 8273	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ B <-> A <_ ( C x. B ) ) )
Theorem	ltdivmul2 8274	'Less than' relationship between division and multiplication. (Contributed by NM, 24-Feb-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) < B <-> A < ( B x. C ) ) )
Theorem	lt2mul2div 8275	'Less than' relationship between division and multiplication. (Contributed by NM, 8-Jan-2006.)
|- ( ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) /\ ( C e. RR /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A x. B ) < ( C x. D ) <-> ( A / D ) < ( C / B ) ) )
Theorem	ledivmul2 8276	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / C ) <_ B <-> A <_ ( B x. C ) ) )
Theorem	lemuldiv 8277	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( A x. C ) <_ B <-> A <_ ( B / C ) ) )
Theorem	lemuldiv2 8278	'Less than or equal' relationship between division and multiplication. (Contributed by NM, 10-Mar-2006.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( ( C x. A ) <_ B <-> A <_ ( B / C ) ) )
Theorem	ltrec 8279	The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A < B <-> ( 1 / B ) < ( 1 / A ) ) )
Theorem	lerec 8280	The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ B <-> ( 1 / B ) <_ ( 1 / A ) ) )
Theorem	lt2msq1 8281	Lemma for lt2msq 8282. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) < ( B x. B ) )
Theorem	lt2msq 8282	Two nonnegative numbers compare the same as their squares. (Contributed by Roy F. Longton, 8-Aug-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A < B <-> ( A x. A ) < ( B x. B ) ) )
Theorem	ltdiv2 8283	Division of a positive number by both sides of 'less than'. (Contributed by NM, 27-Apr-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( C / B ) < ( C / A ) ) )
Theorem	ltrec1 8284	Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( 1 / A ) < B <-> ( 1 / B ) < A ) )
Theorem	lerec2 8285	Reciprocal swap in a 'less than or equal to' relation. (Contributed by NM, 24-Feb-2005.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ ( 1 / B ) <-> B <_ ( 1 / A ) ) )
Theorem	ledivdiv 8286	Invert ratios of positive numbers and swap their ordering. (Contributed by NM, 9-Jan-2006.)
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) ) /\ ( ( C e. RR /\ 0 < C ) /\ ( D e. RR /\ 0 < D ) ) ) -> ( ( A / B ) <_ ( C / D ) <-> ( D / C ) <_ ( B / A ) ) )
Theorem	lediv2 8287	Division of a positive number by both sides of 'less than or equal to'. (Contributed by NM, 10-Jan-2006.)
|- ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( A <_ B <-> ( C / B ) <_ ( C / A ) ) )
Theorem	ltdiv23 8288	Swap denominator with other side of 'less than'. (Contributed by NM, 3-Oct-1999.)
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) < C <-> ( A / C ) < B ) )
Theorem	lediv23 8289	Swap denominator with other side of 'less than or equal to'. (Contributed by NM, 30-May-2005.)
|- ( ( A e. RR /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 < C ) ) -> ( ( A / B ) <_ C <-> ( A / C ) <_ B ) )
Theorem	lediv12a 8290	Comparison of ratio of two nonnegative numbers. (Contributed by NM, 31-Dec-2005.)
|- ( ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) /\ ( ( C e. RR /\ D e. RR ) /\ ( 0 < C /\ C <_ D ) ) ) -> ( A / D ) <_ ( B / C ) )
Theorem	lediv2a 8291	Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Paul Chapman, 7-Sep-2007.)
|- ( ( ( ( A e. RR /\ 0 < A ) /\ ( B e. RR /\ 0 < B ) /\ ( C e. RR /\ 0 <_ C ) ) /\ A <_ B ) -> ( C / B ) <_ ( C / A ) )
Theorem	reclt1 8292	The reciprocal of a positive number less than 1 is greater than 1. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( A < 1 <-> 1 < ( 1 / A ) ) )
Theorem	recgt1 8293	The reciprocal of a positive number greater than 1 is less than 1. (Contributed by NM, 28-Dec-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( 1 < A <-> ( 1 / A ) < 1 ) )
Theorem	recgt1i 8294	The reciprocal of a number greater than 1 is positive and less than 1. (Contributed by NM, 23-Feb-2005.)
|- ( ( A e. RR /\ 1 < A ) -> ( 0 < ( 1 / A ) /\ ( 1 / A ) < 1 ) )
Theorem	recp1lt1 8295	Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( A / ( 1 + A ) ) < 1 )
Theorem	recreclt 8296	Given a positive number A, construct a new positive number less than both A and 1. (Contributed by NM, 28-Dec-2005.)
|- ( ( A e. RR /\ 0 < A ) -> ( ( 1 / ( 1 + ( 1 / A ) ) ) < 1 /\ ( 1 / ( 1 + ( 1 / A ) ) ) < A ) )
Theorem	le2msq 8297	The square function on nonnegative reals is monotonic. (Contributed by NM, 3-Aug-1999.) (Proof shortened by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A <_ B <-> ( A x. A ) <_ ( B x. B ) ) )
Theorem	msq11 8298	The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A x. A ) = ( B x. B ) <-> A = B ) )
Theorem	ledivp1 8299	Less-than-or-equal-to and division relation. (Lemma for computing upper bounds of products. The "+ 1" prevents division by zero.) (Contributed by NM, 28-Sep-2005.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( A / ( B + 1 ) ) x. B ) <_ A )
Theorem	squeeze0 8300*	If a nonnegative number is less than any positive number, it is zero. (Contributed by NM, 11-Feb-2006.)
|- ( ( A e. RR /\ 0 <_ A /\ A. x e. RR ( 0 < x -> A < x ) ) -> A = 0 )