P. 90 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8901-9000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recap0apzi 8901	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) # 0)
Theorem	recidapzi 8902	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	div1i 8903	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 / 1) = 𝐴
Theorem	eqnegi 8904	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐴 ↔ 𝐴 = 0)
Theorem	recclapi 8905	Closure law for reciprocal. (Contributed by NM, 30-Apr-2005.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (1 / 𝐴) ∈ ℂ
Theorem	recidapi 8906	Multiplication of a number and its reciprocal. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (𝐴 · (1 / 𝐴)) = 1
Theorem	recrecapi 8907	A number is equal to the reciprocal of its reciprocal. Theorem I.10 of [Apostol] p. 18. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (1 / (1 / 𝐴)) = 𝐴
Theorem	dividapi 8908	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (𝐴 / 𝐴) = 1
Theorem	div0api 8909	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (0 / 𝐴) = 0
Theorem	divclapzi 8910	Closure law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcanap1zi 8911	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcanap2zi 8912	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecapzi 8913	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divcanap3zi 8914	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4zi 8915	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	rec11api 8916	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 # 0 ∧ 𝐵 # 0) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divclapi 8917	Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℂ
Theorem	divcanap2i 8918	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐵 · (𝐴 / 𝐵)) = 𝐴
Theorem	divcanap1i 8919	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · 𝐵) = 𝐴
Theorem	divrecapi 8920	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))
Theorem	divcanap3i 8921	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐵 · 𝐴) / 𝐵) = 𝐴
Theorem	divcanap4i 8922	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐵) = 𝐴
Theorem	divap0i 8923	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) # 0
Theorem	rec11apii 8924	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵)
Theorem	divassapzi 8925	An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	divmulapzi 8926	Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	divdirapzi 8927	Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divdiv23apzi 8928	Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐵 # 0 ∧ 𝐶 # 0) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divmulapi 8929	Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)
Theorem	divdiv32api 8930	Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)
Theorem	divassapi 8931	An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))
Theorem	divdirapi 8932	Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))
Theorem	div23api 8933	A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)
Theorem	div11api 8934	One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵)
Theorem	divmuldivapi 8935	Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷))
Theorem	divmul13api 8936	Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷))
Theorem	divadddivapi 8937	Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷))
Theorem	divdivdivapi 8938	Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))
Theorem	rerecclapzi 8939	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) ∈ ℝ)
Theorem	rerecclapi 8940	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (1 / 𝐴) ∈ ℝ
Theorem	redivclapzi 8941	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	redivclapi 8942	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℝ
Theorem	div1d 8943	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 / 1) = 𝐴)
Theorem	recclapd 8944	Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℂ)
Theorem	recap0d 8945	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) # 0)
Theorem	recidapd 8946	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recidap2d 8947	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) · 𝐴) = 1)
Theorem	recrecapd 8948	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / (1 / 𝐴)) = 𝐴)
Theorem	dividapd 8949	A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
Theorem	div0apd 8950	Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (0 / 𝐴) = 0)
Theorem	apmul1 8951	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 # 𝐵 ↔ (𝐴 · 𝐶) # (𝐵 · 𝐶)))
Theorem	apmul2 8952	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 6-Jan-2023.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 # 𝐵 ↔ (𝐶 · 𝐴) # (𝐶 · 𝐵)))
Theorem	divclapd 8953	Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcanap1d 8954	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcanap2d 8955	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecapd 8956	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrecap2d 8957	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divcanap3d 8958	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4d 8959	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	diveqap0d 8960	If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	diveqap1d 8961	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	diveqap1ad 8962	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 8868. Generalization of diveqap1d 8961. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	diveqap0ad 8963	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 8845. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divap1d 8964	If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐴 # 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) # 1)
Theorem	divap0bd 8965	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 # 0 ↔ (𝐴 / 𝐵) # 0))
Theorem	divnegapd 8966	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	divneg2apd 8967	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	div2negapd 8968	Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divap0d 8969	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) # 0)
Theorem	recdivapd 8970	The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	recdivap2d 8971	Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	divcanap6d 8972	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	ddcanapd 8973	Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	rec11apd 8974	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (1 / 𝐴) = (1 / 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmulapd 8975	Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	apdivmuld 8976	Relationship between division and multiplication. (Contributed by Jim Kingdon, 26-Dec-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) # 𝐶 ↔ (𝐵 · 𝐶) # 𝐴))
Theorem	div32apd 8977	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13apd 8978	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	divdiv32apd 8979	Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcanap5d 8980	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divcanap5rd 8981	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) / (𝐵 · 𝐶)) = (𝐴 / 𝐵))
Theorem	divcanap7d 8982	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcanapd 8983	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐶) · (𝐴 / 𝐵)) = (𝐴 / 𝐶))
Theorem	dmdcanap2d 8984	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐶)) = (𝐴 / 𝐶))
Theorem	divdivap1d 8985	Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdivap2d 8986	Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	divmulap2d 8987	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmulap3d 8988	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divassapd 8989	An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div12apd 8990	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	div23apd 8991	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	divdirapd 8992	Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divsubdirapd 8993	Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	div11apd 8994	One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmuldivapd 8995	Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐷 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷)))
Theorem	divmuleqapd 8996	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐷 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐶 · 𝐵)))
Theorem	rerecclapd 8997	Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	redivclapd 8998	Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	diveqap1bd 8999	If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8868. Converse of diveqap1d 8961. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)
Theorem	div2subap 9000	Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 # 𝐷)) → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶)))