---

Step * of Lemma divisor_of_minus

∀a,b:ℤ.  ((a | b) ⇒ (a | (-b)))
BY
{ (Unfold `divides` 0 THEN Auto) }

1
1. a : ℤ@i
2. b : ℤ@i
3. ∃c:ℤ. (b = (a * c) ∈ ℤ)@i
⊢ ∃c:ℤ. ((-b) = (a * c) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}.    ((a  |  b)  {}\mRightarrow{}  (a  |  (-b)))


By

---

Latex:
(Unfold  `divides`  0  THEN  Auto)

---

Home Index