P. 88 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8701-8800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recrecapi 8701	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 8702	A number divided by itself is one. (Contributed by NM, 9-Feb-1995.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (𝐴 / 𝐴) = 1
Theorem	div0api 8703	Division into zero is zero. (Contributed by NM, 12-Aug-1999.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (0 / 𝐴) = 0
Theorem	divclapzi 8704	Closure law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcanap1zi 8705	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcanap2zi 8706	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecapzi 8707	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divcanap3zi 8708	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4zi 8709	A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	rec11api 8710	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    ⇒   ⊢ ((𝐴 # 0 ∧ 𝐵 # 0) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	divclapi 8711	Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℂ
Theorem	divcanap2i 8712	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐵 · (𝐴 / 𝐵)) = 𝐴
Theorem	divcanap1i 8713	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · 𝐵) = 𝐴
Theorem	divrecapi 8714	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵))
Theorem	divcanap3i 8715	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐵 · 𝐴) / 𝐵) = 𝐴
Theorem	divcanap4i 8716	A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐵) = 𝐴
Theorem	divap0i 8717	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) # 0
Theorem	rec11apii 8718	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵)
Theorem	divassapzi 8719	An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	divmulapzi 8720	Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐵 # 0 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	divdirapzi 8721	Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ (𝐶 # 0 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divdiv23apzi 8722	Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    ⇒   ⊢ ((𝐵 # 0 ∧ 𝐶 # 0) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divmulapi 8723	Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴)
Theorem	divdiv32api 8724	Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵)
Theorem	divassapi 8725	An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶))
Theorem	divdirapi 8726	Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))
Theorem	div23api 8727	A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵)
Theorem	div11api 8728	One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵)
Theorem	divmuldivapi 8729	Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷))
Theorem	divmul13api 8730	Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐶 / 𝐵) · (𝐴 / 𝐷))
Theorem	divadddivapi 8731	Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    ⇒   ⊢ ((𝐴 / 𝐵) + (𝐶 / 𝐷)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) / (𝐵 · 𝐷))
Theorem	divdivdivapi 8732	Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐷 ∈ ℂ    &   ⊢ 𝐵 # 0    &   ⊢ 𝐷 # 0    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶))
Theorem	rerecclapzi 8733	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) ∈ ℝ)
Theorem	rerecclapi 8734	Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐴 # 0    ⇒   ⊢ (1 / 𝐴) ∈ ℝ
Theorem	redivclapzi 8735	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐵 # 0 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	redivclapi 8736	Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 / 𝐵) ∈ ℝ
Theorem	div1d 8737	A number divided by 1 is itself. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 / 1) = 𝐴)
Theorem	recclapd 8738	Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℂ)
Theorem	recap0d 8739	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) # 0)
Theorem	recidapd 8740	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recidap2d 8741	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) · 𝐴) = 1)
Theorem	recrecapd 8742	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / (1 / 𝐴)) = 𝐴)
Theorem	dividapd 8743	A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐴) = 1)
Theorem	div0apd 8744	Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (0 / 𝐴) = 0)
Theorem	apmul1 8745	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 # 𝐵 ↔ (𝐴 · 𝐶) # (𝐵 · 𝐶)))
Theorem	apmul2 8746	Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 6-Jan-2023.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 # 𝐵 ↔ (𝐶 · 𝐴) # (𝐶 · 𝐵)))
Theorem	divclapd 8747	Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℂ)
Theorem	divcanap1d 8748	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	divcanap2d 8749	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divrecapd 8750	Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrecap2d 8751	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divcanap3d 8752	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4d 8753	A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	diveqap0d 8754	If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 0)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	diveqap1d 8755	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	diveqap1ad 8756	The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 8662. Generalization of diveqap1d 8755. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	diveqap0ad 8757	A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 8639. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divap1d 8758	If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐴 # 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) # 1)
Theorem	divap0bd 8759	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 # 0 ↔ (𝐴 / 𝐵) # 0))
Theorem	divnegapd 8760	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	divneg2apd 8761	Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	div2negapd 8762	Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divap0d 8763	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) # 0)
Theorem	recdivapd 8764	The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	recdivap2d 8765	Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	divcanap6d 8766	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	ddcanapd 8767	Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	rec11apd 8768	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → (1 / 𝐴) = (1 / 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmulapd 8769	Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = 𝐶 ↔ (𝐵 · 𝐶) = 𝐴))
Theorem	apdivmuld 8770	Relationship between division and multiplication. (Contributed by Jim Kingdon, 26-Dec-2022.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) # 𝐶 ↔ (𝐵 · 𝐶) # 𝐴))
Theorem	div32apd 8771	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13apd 8772	A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	divdiv32apd 8773	Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcanap5d 8774	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divcanap5rd 8775	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) / (𝐵 · 𝐶)) = (𝐴 / 𝐵))
Theorem	divcanap7d 8776	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcanapd 8777	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐵 / 𝐶) · (𝐴 / 𝐵)) = (𝐴 / 𝐶))
Theorem	dmdcanap2d 8778	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐵 / 𝐶)) = (𝐴 / 𝐶))
Theorem	divdivap1d 8779	Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdivap2d 8780	Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	divmulap2d 8781	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmulap3d 8782	Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divassapd 8783	An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div12apd 8784	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	div23apd 8785	A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	divdirapd 8786	Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divsubdirapd 8787	Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	div11apd 8788	One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    &   ⊢ (𝜑 → (𝐴 / 𝐶) = (𝐵 / 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	divmuldivapd 8789	Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐷 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) · (𝐶 / 𝐷)) = ((𝐴 · 𝐶) / (𝐵 · 𝐷)))
Theorem	divmuleqapd 8790	Cross-multiply in an equality of ratios. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐷 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 / 𝐵) = (𝐶 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐶 · 𝐵)))
Theorem	rerecclapd 8791	Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ)
Theorem	redivclapd 8792	Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ)
Theorem	diveqap1bd 8793	If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8662. Converse of diveqap1d 8755. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.)
⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 # 0)    &   ⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 / 𝐵) = 1)
Theorem	div2subap 8794	Swap the order of subtraction in a division. (Contributed by Scott Fenton, 24-Jun-2013.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐶 # 𝐷)) → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶)))
Theorem	div2subapd 8795	Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2subap 8794. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 𝐷)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) / (𝐶 − 𝐷)) = ((𝐵 − 𝐴) / (𝐷 − 𝐶)))
Theorem	subrecap 8796	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jul-2015.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵)))
Theorem	subrecapi 8797	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵))
Theorem	subrecapd 8798	Subtraction of reciprocals. (Contributed by Scott Fenton, 9-Jan-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) − (1 / 𝐵)) = ((𝐵 − 𝐴) / (𝐴 · 𝐵)))
Theorem	mvllmulapd 8799	Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 𝐶)    ⇒   ⊢ (𝜑 → 𝐵 = (𝐶 / 𝐴))
Theorem	rerecapb 8800*	A real number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 18-Jan-2025.)
⊢ (𝐴 ∈ ℝ → (𝐴 # 0 ↔ ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1))