---

Step * of Lemma divides_invar_1

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

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

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

---

Latex:

---

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


By

---

Latex:
((Unfold  `divides`  0  THEN  GenUnivCD)  THENA  Auto)

---

Home Index