P. 86 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8501-8600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	apreim 8501	Complex apartness in terms of real and imaginary parts. (Contributed by Jim Kingdon, 12-Feb-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) # (𝐶 + (i · 𝐷)) ↔ (𝐴 # 𝐶 ∨ 𝐵 # 𝐷)))
Theorem	mulreim 8502	Complex multiplication in terms of real and imaginary parts. (Contributed by Jim Kingdon, 23-Feb-2020.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 + (i · 𝐵)) · (𝐶 + (i · 𝐷))) = (((𝐴 · 𝐶) + -(𝐵 · 𝐷)) + (i · ((𝐶 · 𝐵) + (𝐷 · 𝐴)))))
Theorem	apirr 8503	Apartness is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2020.)
⊢ (𝐴 ∈ ℂ → ¬ 𝐴 # 𝐴)
Theorem	apsym 8504	Apartness is symmetric. This theorem for real numbers is part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 ↔ 𝐵 # 𝐴))
Theorem	apcotr 8505	Apartness is cotransitive. (Contributed by Jim Kingdon, 16-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 # 𝐵 → (𝐴 # 𝐶 ∨ 𝐵 # 𝐶)))
Theorem	apadd1 8506	Addition respects apartness. Analogue of addcan 8078 for apartness. (Contributed by Jim Kingdon, 13-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 # 𝐵 ↔ (𝐴 + 𝐶) # (𝐵 + 𝐶)))
Theorem	apadd2 8507	Addition respects apartness. (Contributed by Jim Kingdon, 16-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 # 𝐵 ↔ (𝐶 + 𝐴) # (𝐶 + 𝐵)))
Theorem	addext 8508	Strong extensionality for addition. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 5851. For us, it is proved a different way. (Contributed by Jim Kingdon, 15-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 + 𝐵) # (𝐶 + 𝐷) → (𝐴 # 𝐶 ∨ 𝐵 # 𝐷)))
Theorem	apneg 8509	Negation respects apartness. (Contributed by Jim Kingdon, 14-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 ↔ -𝐴 # -𝐵))
Theorem	mulext1 8510	Left extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐶) # (𝐵 · 𝐶) → 𝐴 # 𝐵))
Theorem	mulext2 8511	Right extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐶 · 𝐴) # (𝐶 · 𝐵) → 𝐴 # 𝐵))
Theorem	mulext 8512	Strong extensionality for multiplication. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 5851. For us, it is proved a different way. (Contributed by Jim Kingdon, 23-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → ((𝐴 · 𝐵) # (𝐶 · 𝐷) → (𝐴 # 𝐶 ∨ 𝐵 # 𝐷)))
Theorem	mulap0r 8513	A product apart from zero. Lemma 2.13 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐴 · 𝐵) # 0) → (𝐴 # 0 ∧ 𝐵 # 0))
Theorem	msqge0 8514	A square is nonnegative. Lemma 2.35 of [Geuvers], p. 9. (Contributed by NM, 23-May-2007.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℝ → 0 ≤ (𝐴 · 𝐴))
Theorem	msqge0i 8515	A square is nonnegative. (Contributed by NM, 14-May-1999.) (Proof shortened by Andrew Salmon, 19-Nov-2011.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ 0 ≤ (𝐴 · 𝐴)
Theorem	msqge0d 8516	A square is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐴))
Theorem	mulge0 8517	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999.) (Revised by Mario Carneiro, 27-May-2016.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 · 𝐵))
Theorem	mulge0i 8518	The product of two nonnegative numbers is nonnegative. (Contributed by NM, 30-Jul-1999.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((0 ≤ 𝐴 ∧ 0 ≤ 𝐵) → 0 ≤ (𝐴 · 𝐵))
Theorem	mulge0d 8519	The product of two nonnegative numbers is nonnegative. (Contributed by Mario Carneiro, 27-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴 · 𝐵))
Theorem	apti 8520	Complex apartness is tight. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 = 𝐵 ↔ ¬ 𝐴 # 𝐵))
Theorem	apne 8521	Apartness implies negated equality. We cannot in general prove the converse (as shown at neapmkv 13946), which is the whole point of having separate notations for apartness and negated equality. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 # 𝐵 → 𝐴 ≠ 𝐵))
Theorem	apcon4bid 8522	Contrapositive law deduction for apartness. (Contributed by Jim Kingdon, 31-Jul-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 # 𝐵 ↔ 𝐶 # 𝐷))    ⇒   ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
Theorem	leltap 8523	≤ implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (𝐴 < 𝐵 ↔ 𝐵 # 𝐴))
Theorem	gt0ap0 8524	Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → 𝐴 # 0)
Theorem	gt0ap0i 8525	Positive means apart from zero (useful for ordering theorems involving division). (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℝ    ⇒   ⊢ (0 < 𝐴 → 𝐴 # 0)
Theorem	gt0ap0ii 8526	Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 0 < 𝐴    ⇒   ⊢ 𝐴 # 0
Theorem	gt0ap0d 8527	Positive implies apart from zero. Because of the way we define #, 𝐴 must be an element of ℝ, not just ℝ*. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → 𝐴 # 0)
Theorem	negap0 8528	A number is apart from zero iff its negative is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.)
⊢ (𝐴 ∈ ℂ → (𝐴 # 0 ↔ -𝐴 # 0))
Theorem	negap0d 8529	The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → -𝐴 # 0)
Theorem	ltleap 8530	Less than in terms of non-strict order and apartness. (Contributed by Jim Kingdon, 28-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐴 # 𝐵)))
Theorem	ltap 8531	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐵 # 𝐴)
Theorem	gtapii 8532	'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ 𝐵 # 𝐴
Theorem	ltapii 8533	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ 𝐴 # 𝐵
Theorem	ltapi 8534	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ 𝐴 ∈ ℝ    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴 < 𝐵 → 𝐵 # 𝐴)
Theorem	gtapd 8535	'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐵 # 𝐴)
Theorem	ltapd 8536	'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 # 𝐵)
Theorem	leltapd 8537	≤ implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐵 # 𝐴))
Theorem	ap0gt0 8538	A nonnegative number is apart from zero if and only if it is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (𝐴 # 0 ↔ 0 < 𝐴))
Theorem	ap0gt0d 8539	A nonzero nonnegative number is positive. (Contributed by Jim Kingdon, 11-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐴 # 0)    ⇒   ⊢ (𝜑 → 0 < 𝐴)
Theorem	apsub1 8540	Subtraction respects apartness. Analogue of subcan2 8123 for apartness. (Contributed by Jim Kingdon, 6-Jan-2022.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 # 𝐵 ↔ (𝐴 − 𝐶) # (𝐵 − 𝐶)))
Theorem	subap0 8541	Two numbers being apart is equivalent to their difference being apart from zero. (Contributed by Jim Kingdon, 25-Dec-2022.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 − 𝐵) # 0 ↔ 𝐴 # 𝐵))
Theorem	subap0d 8542	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 8543	Equality of complex numbers is stable. Stability here means ¬ ¬ 𝐴 = 𝐵 → 𝐴 = 𝐵 as defined at df-stab 821. 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 8544	Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.)
⊢ (𝐴 # 𝐵 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))
Theorem	apsscn 8545*	The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.)
⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 # 𝐵} ⊆ ℂ
Theorem	lt0ap0 8546	A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → 𝐴 # 0)
Theorem	lt0ap0d 8547	A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 0)    ⇒   ⊢ (𝜑 → 𝐴 # 0)
4.3.7  Reciprocals
Theorem	recextlem1 8548	Lemma for recexap 8550. (Contributed by Eric Schmidt, 23-May-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + (i · 𝐵)) · (𝐴 − (i · 𝐵))) = ((𝐴 · 𝐴) + (𝐵 · 𝐵)))
Theorem	recexaplem2 8549	Lemma for recexap 8550. (Contributed by Jim Kingdon, 20-Feb-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 + (i · 𝐵)) # 0) → ((𝐴 · 𝐴) + (𝐵 · 𝐵)) # 0)
Theorem	recexap 8550*	Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ∃𝑥 ∈ ℂ (𝐴 · 𝑥) = 1)
Theorem	mulap0 8551	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 8552	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 # 0 ∧ 𝐵 # 0) ↔ (𝐴 · 𝐵) # 0))
Theorem	mulap0i 8553	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐴 # 0    &   ⊢ 𝐵 # 0    ⇒   ⊢ (𝐴 · 𝐵) # 0
Theorem	mulap0bd 8554	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 8555	The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 # 0)    &   ⊢ (𝜑 → 𝐵 # 0)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) # 0)
Theorem	mulap0bad 8556	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8555 and consequence of mulap0bd 8554. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) # 0)    ⇒   ⊢ (𝜑 → 𝐴 # 0)
Theorem	mulap0bbd 8557	A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 8555 and consequence of mulap0bd 8554. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → (𝐴 · 𝐵) # 0)    ⇒   ⊢ (𝜑 → 𝐵 # 0)
Theorem	mulcanapd 8558	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	mulcanap2d 8559	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    ⇒   ⊢ (𝜑 → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulcanapad 8560	Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcanapd 8558. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    &   ⊢ (𝜑 → (𝐶 · 𝐴) = (𝐶 · 𝐵))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	mulcanap2ad 8561	Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcanap2d 8559. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 # 0)    &   ⊢ (𝜑 → (𝐴 · 𝐶) = (𝐵 · 𝐶))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	mulcanap 8562	Cancellation law for multiplication (full theorem form). (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵))
Theorem	mulcanap2 8563	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐶) = (𝐵 · 𝐶) ↔ 𝐴 = 𝐵))
Theorem	mulcanapi 8564	Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ 𝐴 ∈ ℂ    &   ⊢ 𝐵 ∈ ℂ    &   ⊢ 𝐶 ∈ ℂ    &   ⊢ 𝐶 # 0    ⇒   ⊢ ((𝐶 · 𝐴) = (𝐶 · 𝐵) ↔ 𝐴 = 𝐵)
Theorem	muleqadd 8565	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 8566*	Existential uniqueness of reciprocals. (Contributed by Jim Kingdon, 21-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ∃!𝑥 ∈ ℂ (𝐵 · 𝑥) = 𝐴)
Theorem	mul0eqap 8567	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))
4.3.8  Division
Syntax	cdiv 8568	Extend class notation to include division.
class /
Definition	df-div 8569*	Define division. Theorem divmulap 8571 relates it to multiplication, and divclap 8574 and redivclap 8627 prove its closure laws. (Contributed by NM, 2-Feb-1995.) Use divvalap 8570 instead. (Revised by Mario Carneiro, 1-Apr-2014.) (New usage is discouraged.)
⊢ / = (𝑥 ∈ ℂ, 𝑦 ∈ (ℂ ∖ {0}) ↦ (℩𝑧 ∈ ℂ (𝑦 · 𝑧) = 𝑥))
Theorem	divvalap 8570*	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 8571	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ (𝐶 · 𝐵) = 𝐴))
Theorem	divmulap2 8572	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐶 · 𝐵)))
Theorem	divmulap3 8573	Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = 𝐵 ↔ 𝐴 = (𝐵 · 𝐶)))
Theorem	divclap 8574	Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) ∈ ℂ)
Theorem	recclap 8575	Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) ∈ ℂ)
Theorem	divcanap2 8576	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐵 · (𝐴 / 𝐵)) = 𝐴)
Theorem	divcanap1 8577	A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) · 𝐵) = 𝐴)
Theorem	diveqap0 8578	A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 / 𝐵) = 0 ↔ 𝐴 = 0))
Theorem	divap0b 8579	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 # 0 ↔ (𝐴 / 𝐵) # 0))
Theorem	divap0 8580	The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐴 # 0) ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0)) → (𝐴 / 𝐵) # 0)
Theorem	recap0 8581	The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (1 / 𝐴) # 0)
Theorem	recidap 8582	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 · (1 / 𝐴)) = 1)
Theorem	recidap2 8583	Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → ((1 / 𝐴) · 𝐴) = 1)
Theorem	divrecap 8584	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = (𝐴 · (1 / 𝐵)))
Theorem	divrecap2 8585	Relationship between division and reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → (𝐴 / 𝐵) = ((1 / 𝐵) · 𝐴))
Theorem	divassap 8586	An associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = (𝐴 · (𝐵 / 𝐶)))
Theorem	div23ap 8587	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 · 𝐵) / 𝐶) = ((𝐴 / 𝐶) · 𝐵))
Theorem	div32ap 8588	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = (𝐴 · (𝐶 / 𝐵)))
Theorem	div13ap 8589	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐵 # 0) ∧ 𝐶 ∈ ℂ) → ((𝐴 / 𝐵) · 𝐶) = ((𝐶 / 𝐵) · 𝐴))
Theorem	div12ap 8590	A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → (𝐴 · (𝐵 / 𝐶)) = (𝐵 · (𝐴 / 𝐶)))
Theorem	divmulassap 8591	An associative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = ((𝐴 · 𝐵) · (𝐶 / 𝐷)))
Theorem	divmulasscomap 8592	An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) ∧ (𝐷 ∈ ℂ ∧ 𝐷 # 0)) → ((𝐴 · (𝐵 / 𝐷)) · 𝐶) = (𝐵 · ((𝐴 · 𝐶) / 𝐷)))
Theorem	divdirap 8593	Distribution of division over addition. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶)))
Theorem	divcanap3 8594	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐵 · 𝐴) / 𝐵) = 𝐴)
Theorem	divcanap4 8595	A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 # 0) → ((𝐴 · 𝐵) / 𝐵) = 𝐴)
Theorem	div11ap 8596	One-to-one relationship for division. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ (𝐶 ∈ ℂ ∧ 𝐶 # 0)) → ((𝐴 / 𝐶) = (𝐵 / 𝐶) ↔ 𝐴 = 𝐵))
Theorem	dividap 8597	A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (𝐴 / 𝐴) = 1)
Theorem	div0ap 8598	Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 # 0) → (0 / 𝐴) = 0)
Theorem	div1 8599	A number divided by 1 is itself. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Mario Carneiro, 27-May-2016.)
⊢ (𝐴 ∈ ℂ → (𝐴 / 1) = 𝐴)
Theorem	1div1e1 8600	1 divided by 1 is 1 (common case). (Contributed by David A. Wheeler, 7-Dec-2018.)
⊢ (1 / 1) = 1