P. 76 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7501-7600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recidapd 7501	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> (A x. ( 1 / A)) = 1)
Theorem	recidap2d 7502	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> (( 1 / A) x. A) = 1)
Theorem	recrecapd 7503	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 1 / ( 1 / A)) = A)
Theorem	dividapd 7504	A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> (A / A) = 1)
Theorem	div0apd 7505	Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 0 / A) = 0)
Theorem	apmul1 7506	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
|- ((A e. CC /\ B e. CC /\ ( C e. CC /\ C # 0)) -> (A # B <-> (A x. C) # (B x. C)))
Theorem	divclapd 7507	Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) e. CC)
Theorem	divcanap1d 7508	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 / B) x. B) = A)
Theorem	divcanap2d 7509	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (B x. (A / B)) = A)
Theorem	divrecapd 7510	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) = (A x. ( 1 / B)))
Theorem	divrecap2d 7511	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> (A / B) = (( 1 / B) x. A))
Theorem	divcanap3d 7512	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ((B x. A) / B) = A)
Theorem	divcanap4d 7513	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 7514	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 7515	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 7516	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7424. Generalization of diveqap1d 7515. (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 7517	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7403. (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 7518	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 7519	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 7520	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) = ( -uA / B))
Theorem	divneg2apd 7521	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 / -uB))
Theorem	div2negapd 7522	Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> B e. CC)   &   |- (ph -> B # 0)   =>   |- (ph -> ( -uA / -uB) = (A / B))
Theorem	divap0d 7523	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 7524	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 7525	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 7526	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 7527	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 7528	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 7529	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 7530	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 7531	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 7532	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 7533	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 7534	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 7535	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 7536	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 7537	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 7538	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 7539	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 7540	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 7541	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 7542	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 7543	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 7544	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 7545	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 7546	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 7547	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	rerecclapd 7548	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 7549	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 7550	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 7551	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- (A e. RR -> A < (A + 1))
Theorem	lep1 7552	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 7553	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|- (A e. RR -> (A - 1) < A)
Theorem	lem1 7554	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 7555	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 7556	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 7557	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 7558	Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7559 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 7559	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 7560	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 7561	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 7562	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 7563	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 7564	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 7565	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 7566	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 7567	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 7568	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 7569	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 7570	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 7571	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 7572	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 7573	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 7574	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 7575	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 7576	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 7577	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 7578	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 7579	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 7580	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 7581	'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 7582	'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 7583	'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 7584	'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 7585	'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 7586	'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 7587	'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 7588	'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 7589	'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 7590	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 7591	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 7592	Lemma for lt2msq 7593. (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 7593	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 7594	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 7595	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 7596	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 7597	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 7598	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 7599	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 7600	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))