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	recid2d 10401	Multiplication of a number and its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( ( 1 / A ) x. A ) = 1 )
Theorem	recrecd 10402	A number is equal to the reciprocal of its reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 1 / ( 1 / A ) ) = A )
Theorem	dividd 10403	A number divided by itself is one. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( A / A ) = 1 )
Theorem	div0d 10404	Division into zero is zero. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 0 / A ) = 0 )
Theorem	divcld 10405	Closure law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) e. CC )
Theorem	divcan1d 10406	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) x. B ) = A )
Theorem	divcan2d 10407	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( B x. ( A / B ) ) = A )
Theorem	divrecd 10408	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) = ( A x. ( 1 / B ) ) )
Theorem	divrec2d 10409	Relationship between division and reciprocal. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( A / B ) = ( ( 1 / B ) x. A ) )
Theorem	divcan3d 10410	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( B x. A ) / B ) = A )
Theorem	divcan4d 10411	A cancellation law for division. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A x. B ) / B ) = A )
Theorem	diveq0d 10412	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 / B ) = 0 )   =>    |- ( ph -> A = 0 )
Theorem	diveq1d 10413	Equality in terms of unit ratio. (Contributed by Mario Carneiro, 27-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> ( A / B ) = 1 )   =>    |- ( ph -> A = B )
Theorem	diveq1ad 10414	The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 10323. Generalization of diveq1d 10413. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) = 1 <-> A = B ) )
Theorem	diveq0ad 10415	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 10302. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   =>    |- ( ph -> ( ( A / B ) = 0 <-> A = 0 ) )
Theorem	divne1d 10416	If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 10413. (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 10417	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 10418	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 10419	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 10420	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 10421	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 10422	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 10423	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 10424	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 10425	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 10426	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 10427	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 10428	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 10429	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 10430	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 10431	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 10432	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 10433	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 10434	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 10435	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 10436	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 10437	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 10438	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 10439	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 10440	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 10441	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 10442	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 10443	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 10444	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 10445	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 10446	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 10447	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 10448	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 10449	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 10450	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 10451	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 10452	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 10453	If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 10323. Converse of diveq1d 10413. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> B e. CC )   &    |- ( ph -> B =/= 0 )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( A / B ) = 1 )
Theorem	div2sub 10454	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 10455	Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 10454. (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 10456	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 10457	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 10458	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 10459	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 10460	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 10461	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 10462	Move LHS left multiplication to RHS. Uses divcan4i 10376. (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 10463	Hypothesis for weak deduction theorem to eliminate 0 < A. (Contributed by NM, 15-May-1999.)
|- 0 < if ( 0 < A , A , 1 )
Theorem	elimge0 10464	Hypothesis for weak deduction theorem to eliminate 0 <_ A. (Contributed by NM, 30-Jul-1999.)
|- 0 <_ if ( 0 <_ A , A , 0 )
Theorem	ltp1 10465	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- ( A e. RR -> A < ( A + 1 ) )
Theorem	lep1 10466	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 10467	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|- ( A e. RR -> ( A - 1 ) < A )
Theorem	lem1 10468	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 10469	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 10470	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 10471	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 10472	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 10473	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 10474	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 10475	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 10476	Lemma for ltmul1 10477. 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 10477	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 10478	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 10479	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 10480	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 10481	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 10482	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 10483	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 10484	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 10485	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 10486	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 10487	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 10488	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 10489	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 10490	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 10491	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 10492	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 10493	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 10494	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 10495	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 10496	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 10497	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 10498	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 10499	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 10500	'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 ) ) )