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	recidapi 7501	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &   |- A # 0   =>   |- (A x. ( 1 / A)) = 1
Theorem	recrecapi 7502	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &   |- A # 0   =>   |- ( 1 / ( 1 / A)) = A
Theorem	dividapi 7503	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
|- A e. CC   &   |- A # 0   =>   |- (A / A) = 1
Theorem	div0api 7504	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
|- A e. CC   &   |- A # 0   =>   |- ( 0 / A) = 0
Theorem	divclapzi 7505	Closure law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &   |- B e. CC   =>   |- (B # 0 -> (A / B) e. CC)
Theorem	divcanap1zi 7506	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &   |- B e. CC   =>   |- (B # 0 -> ((A / B) x. B) = A)
Theorem	divcanap2zi 7507	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &   |- B e. CC   =>   |- (B # 0 -> (B x. (A / B)) = A)
Theorem	divrecapzi 7508	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &   |- B e. CC   =>   |- (B # 0 -> (A / B) = (A x. ( 1 / B)))
Theorem	divcanap3zi 7509	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &   |- B e. CC   =>   |- (B # 0 -> ((B x. A) / B) = A)
Theorem	divcanap4zi 7510	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
|- A e. CC   &   |- B e. CC   =>   |- (B # 0 -> ((A x. B) / B) = A)
Theorem	rec11api 7511	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   =>   |- ((A # 0 /\ B # 0) -> (( 1 / A) = ( 1 / B) <-> A = B))
Theorem	divclapi 7512	Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- B # 0   =>   |- (A / B) e. CC
Theorem	divcanap2i 7513	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- B # 0   =>   |- (B x. (A / B)) = A
Theorem	divcanap1i 7514	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- B # 0   =>   |- ((A / B) x. B) = A
Theorem	divrecapi 7515	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- B # 0   =>   |- (A / B) = (A x. ( 1 / B))
Theorem	divcanap3i 7516	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- B # 0   =>   |- ((B x. A) / B) = A
Theorem	divcanap4i 7517	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- B # 0   =>   |- ((A x. B) / B) = A
Theorem	divap0i 7518	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- A # 0   &   |- B # 0   =>   |- (A / B) # 0
Theorem	rec11apii 7519	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- A # 0   &   |- B # 0   =>   |- (( 1 / A) = ( 1 / B) <-> A = B)
Theorem	divassapzi 7520	An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- ( C # 0 -> ((A x. B) / C) = (A x. (B / C)))
Theorem	divmulapzi 7521	Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (B # 0 -> ((A / B) = C <-> (B x. C) = A))
Theorem	divdirapzi 7522	Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- ( C # 0 -> ((A + B) / C) = ((A / C) + (B / C)))
Theorem	divdiv23apzi 7523	Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- ((B # 0 /\ C # 0) -> ((A / B) / C) = ((A / C) / B))
Theorem	divmulapi 7524	Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- B # 0   =>   |- ((A / B) = C <-> (B x. C) = A)
Theorem	divdiv32api 7525	Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- B # 0   &   |- C # 0   =>   |- ((A / B) / C) = ((A / C) / B)
Theorem	divassapi 7526	An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A x. B) / C) = (A x. (B / C))
Theorem	divdirapi 7527	Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A + B) / C) = ((A / C) + (B / C))
Theorem	div23api 7528	A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A x. B) / C) = ((A / C) x. B)
Theorem	div11api 7529	One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- C # 0   =>   |- ((A / C) = (B / C) <-> A = B)
Theorem	divmuldivapi 7530	Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   =>   |- ((A / B) x. ( C / D)) = ((A x. C) / (B x. D))
Theorem	divmul13api 7531	Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   =>   |- ((A / B) x. ( C / D)) = (( C / B) x. (A / D))
Theorem	divadddivapi 7532	Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   =>   |- ((A / B) + ( C / D)) = (((A x. D) + ( C x. B)) / (B x. D))
Theorem	divdivdivapi 7533	Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   &   |- D e. CC   &   |- B # 0   &   |- D # 0   &   |- C # 0   =>   |- ((A / B) / ( C / D)) = ((A x. D) / (B x. C))
Theorem	rerecclapzi 7534	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   =>   |- (A # 0 -> ( 1 / A) e. RR)
Theorem	rerecclapi 7535	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &   |- A # 0   =>   |- ( 1 / A) e. RR
Theorem	redivclapzi 7536	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &   |- B e. RR   =>   |- (B # 0 -> (A / B) e. RR)
Theorem	redivclapi 7537	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
|- A e. RR   &   |- B e. RR   &   |- B # 0   =>   |- (A / B) e. RR
Theorem	div1d 7538	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
|- (ph -> A e. CC)   =>   |- (ph -> (A / 1) = A)
Theorem	recclapd 7539	Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 1 / A) e. CC)
Theorem	recap0d 7540	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
|- (ph -> A e. CC)   &   |- (ph -> A # 0)   =>   |- (ph -> ( 1 / A) # 0)
Theorem	recidapd 7541	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 7542	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 7543	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 7544	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 7545	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 7546	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 7547	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 7548	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 7549	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 7550	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 7551	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 7552	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 7553	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 7554	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 7555	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 7556	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7464. Generalization of diveqap1d 7555. (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 7557	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7443. (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 7558	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 7559	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 7560	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 7561	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 7562	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 7563	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 7564	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 7565	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 7566	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 7567	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 7568	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 7569	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 7570	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 7571	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 7572	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 7573	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 7574	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 7575	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 7576	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 7577	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 7578	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 7579	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 7580	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 7581	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 7582	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 7583	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 7584	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 7585	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 7586	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 7587	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 7588	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 7589	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 7590	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 7591	A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001.)
|- (A e. RR -> A < (A + 1))
Theorem	lep1 7592	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 7593	A number minus 1 is less than itself. (Contributed by NM, 9-Apr-2006.)
|- (A e. RR -> (A - 1) < A)
Theorem	lem1 7594	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 7595	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 7596	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 7597	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 7598	Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7599 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 7599	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 7600	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)