P. 87 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8601-8700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	apsub1 8601	Subtraction respects apartness. Analogue of subcan2 8184 for apartness. (Contributed by Jim Kingdon, 6-Jan-2022.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 # 𝐵 ↔ (𝐴 − 𝐶) # (𝐵 − 𝐶)))
Theorem	subap0 8602	Two numbers being apart is equivalent to their difference being apart from zero. (Contributed by Jim Kingdon, 25-Dec-2022.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) # 0 ↔ 𝐴 # 𝐵))
Theorem	subap0d 8603	Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) # 0)
Theorem	cnstab 8604	Equality of complex numbers is stable. Stability here means ¬ ¬ 𝐴 = 𝐵 → 𝐴 = 𝐵 as defined at df-stab 831. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → STAB 𝐴 = 𝐵)
Theorem	aprcl 8605	Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.)
⊢ (𝐴 # 𝐵 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
Theorem	apsscn 8606*	The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 # 𝐵} ⊆ ℂ
Theorem	lt0ap0 8607	A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 # 0)
Theorem	lt0ap0d 8608	A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → 𝐴 # 0)
Theorem	aptap 8609	Complex apartness (as defined at df-ap 8541) is a tight apartness (as defined at df-tap 7251). (Contributed by Jim Kingdon, 16-Feb-2025.)
⊢ # TAp ℂ
4.3.7  Reciprocals
Theorem	recextlem1 8610	Lemma for recexap 8612. (Contributed by Eric Schmidt, 23-May-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) = ((𝐴 · 𝐴) + (𝐵 · 𝐵)))
Theorem	recexaplem2 8611	Lemma for recexap 8612. (Contributed by Jim Kingdon, 20-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) # 0) → ((𝐴 · 𝐴) + (𝐵 · 𝐵)) # 0)
Theorem	recexap 8612*	Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)
Theorem	mulap0 8613	The product of two numbers apart from zero is apart from zero. Lemma 2.15 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 · 𝐵) # 0)
Theorem	mulap0b 8614	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 # 0 ∧ 𝐵 # 0) ↔ (𝐴 · 𝐵) # 0))
Theorem	mulap0i 8615	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 · 𝐵) # 0
Theorem	mulap0bd 8616	The product of two numbers apart from zero is apart from zero. Exercise 11.11 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 # 0 ∧ 𝐵 # 0) ↔ (𝐴 · 𝐵) # 0))
Theorem	mulap0d 8617	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) # 0)
Theorem	mulap0bad 8618	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8617 and consequence of mulap0bd 8616. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) # 0)    ⇒   ⊢ (𝜑 → 𝐴 # 0)
Theorem	mulap0bbd 8619	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8617 and consequence of mulap0bd 8616. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) # 0)    ⇒   ⊢ (𝜑 → 𝐵 # 0)
Theorem	mulcanapd 8620	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	mulcanap2d 8621	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulcanapad 8622	Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcanapd 8620. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    &   ⊢ (𝜑 → (𝐶 · 𝐴) = (𝐶 · 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	mulcanap2ad 8623	Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcanap2d 8621. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    &   ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐵 · 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	mulcanap 8624	Cancellation law for multiplication (full theorem form). (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	mulcanap2 8625	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulcanapi 8626	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)
Theorem	muleqadd 8627	Property of numbers whose product equals their sum. Equation 5 of [Kreyszig] p. 12. (Contributed by NM, 13-Nov-2006.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 · 𝐵) = (𝐴 + 𝐵) ↔ ((𝐴 − 1) · (𝐵 − 1)) = 1))
Theorem	receuap 8628*	Existential uniqueness of reciprocals. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)
Theorem	mul0eqap 8629	If two numbers are apart from each other and their product is zero, one of them must be zero. (Contributed by Jim Kingdon, 31-Jul-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 𝐵)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐴 = 0 ∨ 𝐵 = 0))
Theorem	recapb 8630*	A complex number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies), generalized from real to complex numbers. (Contributed by Jim Kingdon, 18-Jan-2025.)
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1))
4.3.8  Division
Syntax	cdiv 8631	Extend class notation to include division.
class /
Definition	df-div 8632*	Define division. Theorem divmulap 8634 relates it to multiplication, and divclap 8637 and redivclap 8690 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divvalap 8633 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.)
⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
Theorem	divvalap 8633*	Value of division: the (unique) element 𝑥 such that (𝐵 · 𝑥) = 𝐴. This is meaningful only when 𝐵 is apart from zero. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = (℩𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴))
Theorem	divmulap 8634	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	divmulap2 8635	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmulap3 8636	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divclap 8637	Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) ∈ ℂ)
Theorem	recclap 8638	Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) ∈ ℂ)
Theorem	divcanap2 8639	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divcanap1 8640	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	diveqap0 8641	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divap0b 8642	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 # 0 ↔ (𝐴 / 𝐵) # 0))
Theorem	divap0 8643	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 / 𝐵) # 0)
Theorem	recap0 8644	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) # 0)
Theorem	recidap 8645	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recidap2 8646	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((1 / 𝐴) · 𝐴) = 1)
Theorem	divrecap 8647	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrecap2 8648	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divassap 8649	An associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div23ap 8650	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	div32ap 8651	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13ap 8652	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	div12ap 8653	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	divmulassap 8654	An associative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷)))
Theorem	divmulasscomap 8655	An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷)))
Theorem	divdirap 8656	Distribution of division over addition. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divcanap3 8657	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4 8658	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	div11ap 8659	One-to-one relationship for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵))
Theorem	dividap 8660	A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 / 𝐴) = 1)
Theorem	div0ap 8661	Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (0 / 𝐴) = 0)
Theorem	div1 8662	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
Theorem	1div1e1 8663	1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ (1 / 1) = 1
Theorem	diveqap1 8664	Equality in terms of unit ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) = 1 ↔ 𝐴 = 𝐵))
Theorem	divnegap 8665	Move negative sign inside of a division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → -(𝐴 / 𝐵) = (-𝐴 / 𝐵))
Theorem	muldivdirap 8666	Distribution of division over addition with a multiplication. (Contributed by Jim Kingdon, 11-Nov-2021.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (((𝐶 · 𝐴) + 𝐵) / 𝐶) = (𝐴 + (𝐵 / 𝐶)))
Theorem	divsubdirap 8667	Distribution of division over subtraction. (Contributed by NM, 4-Mar-2005.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 − 𝐵) / 𝐶) = ((𝐴 / 𝐶) − (𝐵 / 𝐶)))
Theorem	recrecap 8668	A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / (1 / 𝐴)) = 𝐴)
Theorem	rec11ap 8669	Reciprocal is one-to-one. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) = (1 / 𝐵) ↔ 𝐴 = 𝐵))
Theorem	rec11rap 8670	Mutual reciprocals. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) = 𝐵 ↔ (1 / 𝐵) = 𝐴))
Theorem	divmuldivap 8671	Multiplication of two ratios. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 · 𝐵) / (𝐶 · 𝐷)))
Theorem	divdivdivap 8672	Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐵) / (𝐶 / 𝐷)) = ((𝐴 · 𝐷) / (𝐵 · 𝐶)))
Theorem	divcanap5 8673	Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐶 · 𝐴) / (𝐶 · 𝐵)) = (𝐴 / 𝐵))
Theorem	divmul13ap 8674	Swap the denominators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐵 / 𝐶) · (𝐴 / 𝐷)))
Theorem	divmul24ap 8675	Swap the numerators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) · (𝐵 / 𝐷)) = ((𝐴 / 𝐷) · (𝐵 / 𝐶)))
Theorem	divmuleqap 8676	Cross-multiply in an equality of ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) = (𝐵 / 𝐷) ↔ (𝐴 · 𝐷) = (𝐵 · 𝐶)))
Theorem	recdivap 8677	The reciprocal of a ratio. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (1 / (𝐴 / 𝐵)) = (𝐵 / 𝐴))
Theorem	divcanap6 8678	Cancellation of inverted fractions. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((𝐴 / 𝐵) · (𝐵 / 𝐴)) = 1)
Theorem	divdiv32ap 8679	Swap denominators in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐵) / 𝐶) = ((𝐴 / 𝐶) / 𝐵))
Theorem	divcanap7 8680	Cancel equal divisors in a division. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) / (𝐵 / 𝐶)) = (𝐴 / 𝐵))
Theorem	dmdcanap 8681	Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · (𝐶 / 𝐴)) = (𝐶 / 𝐵))
Theorem	divdivap1 8682	Division into a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐵) / 𝐶) = (𝐴 / (𝐵 · 𝐶)))
Theorem	divdivap2 8683	Division by a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 / (𝐵 / 𝐶)) = ((𝐴 · 𝐶) / 𝐵))
Theorem	recdivap2 8684	Division into a reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → ((1 / 𝐴) / 𝐵) = (1 / (𝐴 · 𝐵)))
Theorem	ddcanap 8685	Cancellation in a double division. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 / (𝐴 / 𝐵)) = 𝐵)
Theorem	divadddivap 8686	Addition of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) + (𝐵 / 𝐷)) = (((𝐴 · 𝐷) + (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	divsubdivap 8687	Subtraction of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ ((𝐶 ∈ ℂ ∧ 𝐶 # 0) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0))) → ((𝐴 / 𝐶) − (𝐵 / 𝐷)) = (((𝐴 · 𝐷) − (𝐵 · 𝐶)) / (𝐶 · 𝐷)))
Theorem	conjmulap 8688	Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ (((𝑃 ∈ ℂ ∧ 𝑃 # 0) ∧ (𝑄 ∈ ℂ ∧ 𝑄 # 0)) → (((1 / 𝑃) + (1 / 𝑄)) = 1 ↔ ((𝑃 − 1) · (𝑄 − 1)) = 1))
Theorem	rerecclap 8689	Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 # 0) → (1 / 𝐴) ∈ ℝ)
Theorem	redivclap 8690	Closure law for division of reals. (Contributed by Jim Kingdon, 26-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 # 0) → (𝐴 / 𝐵) ∈ ℝ)
Theorem	eqneg 8691	A number equal to its negative is zero. (Contributed by NM, 12-Jul-2005.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegd 8692	A complex number equals its negative iff it is zero. Deduction form of eqneg 8691. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    ⇒   ⊢ (𝜑 → (𝐴 = -𝐴 ↔ 𝐴 = 0))
Theorem	eqnegad 8693	If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 8691. (Contributed by David Moews, 28-Feb-2017.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 = -𝐴)    ⇒   ⊢ (𝜑 → 𝐴 = 0)
Theorem	div2negap 8694	Quotient of two negatives. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (-𝐴 / -𝐵) = (𝐴 / 𝐵))
Theorem	divneg2ap 8695	Move negative sign inside of a division. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → -(𝐴 / 𝐵) = (𝐴 / -𝐵))
Theorem	recclapzi 8696	Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) ∈ ℂ)
Theorem	recap0apzi 8697	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (1 / 𝐴) # 0)
Theorem	recidapzi 8698	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 # 0 → (𝐴 · (1 / 𝐴)) = 1)
Theorem	div1i 8699	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 / 1) = 𝐴
Theorem	eqnegi 8700	A number equal to its negative is zero. (Contributed by NM, 29-May-1999.)
⊢ 𝐴 ∈ ℂ    ⇒   ⊢ (𝐴 = -𝐴 ↔ 𝐴 = 0)