P. 105 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10401-10500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	divne1d 10401	If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 10398. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ( A / B ) =/= 1 )
Theorem	divne0bd 10402	A ratio is zero iff the numerator is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A =/= 0 <-> ( A / B ) =/= 0 ) )
Theorem	divnegd 10403	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> -u ( A / B ) = ( -u A / B ) )
Theorem	divneg2d 10404	Move negative sign inside of a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> -u ( A / B ) = ( A / -u B ) )
Theorem	div2negd 10405	Quotient of two negatives. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( -u A / -u B ) = ( A / B ) )
Theorem	divne0d 10406	The ratio of nonzero numbers is nonzero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) =/= 0 )
Theorem	recdivd 10407	The reciprocal of a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( 1 / ( A / B ) ) = ( B / A ) )
Theorem	recdiv2d 10408	Division into a reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( 1 / A ) / B ) = ( 1 / ( A x. B ) ) )
Theorem	divcan6d 10409	Cancellation of inverted fractions. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. ( B / A ) ) = 1 )
Theorem	ddcand 10410	Cancellation in a double division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / ( A / B ) ) = B )
Theorem	rec11d 10411	Reciprocal is one-to-one. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> ( 1 / A ) = ( 1 / B ) )   =>    |- ( ph -> A = B )
Theorem	divmuld 10412	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) = C <-> ( B x. C ) = A ) )
Theorem	div32d 10413	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	div13d 10414	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	divdiv32d 10415	Swap denominators in a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	divcan5d 10416	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	divcan5rd 10417	Cancellation of common factor in a ratio. (Contributed by Mario Carneiro, 1-Jan-2017.)
|- ( 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	divcan7d 10418	Cancel equal divisors in a division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	dmdcand 10419	Cancellation law for division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	dmdcan2d 10420	Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.)
|- ( 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	divdiv1d 10421	Division into a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	divdiv2d 10422	Division by a fraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	divmul2d 10423	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( C x. B ) ) )
Theorem	divmul3d 10424	Relationship between division and multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / C ) = B <-> A = ( B x. C ) ) )
Theorem	divassd 10425	An associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	div12d 10426	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	div23d 10427	A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	divdird 10428	Distribution of division over addition. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A + B ) / C ) = ( ( A / C ) + ( B / C ) ) )
Theorem	divsubdird 10429	Distribution of division over subtraction. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A - B ) / C ) = ( ( A / C ) - ( B / C ) ) )
Theorem	div11d 10430	One-to-one relationship for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> C =/= 0 )   &    |- ( ph -> ( A / C ) = ( B / C ) )   =>    |- ( ph -> A = B )
Theorem	divmuldivd 10431	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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	divmul13d 10432	Swap denominators of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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 ) ) = ( ( C / B ) x. ( A / D ) ) )
Theorem	divmul24d 10433	Swap the numerators in the product of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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 / D ) x. ( C / B ) ) )
Theorem	divadddivd 10434	Addition of two ratios. Theorem I.13 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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 ) + ( C / D ) ) = ( ( ( A x. D ) + ( C x. B ) ) / ( B x. D ) ) )
Theorem	divsubdivd 10435	Subtraction of two ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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 ) - ( C / D ) ) = ( ( ( A x. D ) - ( C x. B ) ) / ( B x. D ) ) )
Theorem	divmuleqd 10436	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( 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 ) = ( C / D ) <-> ( A x. D ) = ( C x. B ) ) )
Theorem	divdivdivd 10437	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> D =/= 0 )   &    |- ( ph -> C =/= 0 )   =>    |- ( ph -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) )
Theorem	diveq1bd 10438	If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 10308. Converse of diveq1d 10398. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A / B ) = 1 )
Theorem	div2sub 10439	Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC /\ C =/= D ) ) -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )
Theorem	div2subd 10440	Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 10439. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> C =/= D )   =>    |- ( ph -> ( ( A - B ) / ( C - D ) ) = ( ( B - A ) / ( D - C ) ) )
Theorem	rereccld 10441	Closure law for reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 1 / A ) e. RR )
Theorem	redivcld 10442	Closure law for division of reals. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) e. RR )
Theorem	subrec 10443	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) )
Theorem	subreci 10444	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
|- A e. CC   &    |- B e. CC   &    |- A =/= 0   &    |- B =/= 0   =>    |- ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) )
Theorem	subrecd 10445	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( 1 / A ) - ( 1 / B ) ) = ( ( B - A ) / ( A x. B ) ) )
Theorem	mvllmuld 10446	Move LHS left multiplication to RHS. (Contributed by David A. Wheeler, 15-Oct-2018.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> ( A x. B ) = C )   =>    |- ( ph -> B = ( C / A ) )
Theorem	mvllmuli 10447	Move LHS left multiplication to RHS. Uses divcan4i 10361. (Contributed by David A. Wheeler, 11-Oct-2018.)
|- A e. CC   &    |- B e. CC   &    |- A =/= 0   &    |- ( A x. B ) = C   =>    |- B = ( C / A )
5.3.7  Ordering on reals (cont.)
Theorem	elimgt0 10448	Hypothesis for weak deduction theorem to eliminate 0 < A. (Contributed by NM, 15-May-1999.)
|- 0 < if ( 0 < A , A , 1 )
Theorem	elimge0 10449	Hypothesis for weak deduction theorem to eliminate 0 <_ A. (Contributed by NM, 30-Jul-1999.)
|- 0 <_ if ( 0 <_ A , A , 0 )
Theorem	ltp1 10450	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- ( A e. RR -> A < ( A + 1 ) )
Theorem	lep1 10451	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 10452	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|- ( A e. RR -> ( A - 1 ) < A )
Theorem	lem1 10453	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 10454	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 10455	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 10456	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	prodgt0 10457	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 10458	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 10459	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 10460	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	ltmul1a 10461	Lemma for ltmul1 10462. Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 15-May-1999.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) /\ A < B ) -> ( A x. C ) < ( B x. C ) )
Theorem	ltmul1 10462	Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of [Apostol] p. 20. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 27-May-2016.)
|- ( ( A e. RR /\ B e. RR /\ ( C e. RR /\ 0 < C ) ) -> ( A < B <-> ( A x. C ) < ( B x. C ) ) )
Theorem	ltmul2 10463	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	lemul1 10464	Multiplication of both sides of 'less than or equal to' by a positive number. (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	lemul2 10465	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 10466	Multiplication of both sides of 'less than or equal to' by a nonnegative number. (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 10467	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 10468	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 10469	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 10470	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 10471	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 10472	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 10473	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 10474	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 10475	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 10476	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 10477	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 10478	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 10479	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 10480	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 10481	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	mulge0b 10482	A condition for multiplication to be nonnegative. (Contributed by Scott Fenton, 25-Jun-2013.)
|- ( ( A e. RR /\ B e. RR ) -> ( 0 <_ ( A x. B ) <-> ( ( A <_ 0 /\ B <_ 0 ) \/ ( 0 <_ A /\ 0 <_ B ) ) ) )
Theorem	mulle0b 10483	A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( A x. B ) <_ 0 <-> ( ( A <_ 0 /\ 0 <_ B ) \/ ( 0 <_ A /\ B <_ 0 ) ) ) )
Theorem	mulsuble0b 10484	A condition for multiplication of subtraction to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( ( A - B ) x. ( C - B ) ) <_ 0 <-> ( ( A <_ B /\ B <_ C ) \/ ( C <_ B /\ B <_ A ) ) ) )
Theorem	ltmuldiv 10485	'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 10486	'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 10487	'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 10488	'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 10489	'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 10490	'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 10491	'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	ledivmul2OLD 10492	'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ 0 < B ) -> ( ( A / B ) <_ C <-> A <_ ( C x. B ) ) )
Theorem	lemuldiv 10493	'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 10494	'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 10495	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 10496	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 10497	Lemma for lt2msq 10498. (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 10498	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 10499	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 10500	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 ) )