---

Step * of Lemma divides_invar_2

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

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

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

---

Latex:

---

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


By

---

Latex:
(Unfold  `divides`  0  THEN  Auto)

---

Home Index