---

Step * of Lemma divides_nchar

∀a,b:ℕ+.  (a | b ⇐⇒ ∃c:ℕ+. (b = (a * c) ∈ ℕ+))
BY
{ ((Unfold `divides` 0 THEN GenRepD) 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:\mBbbN{}\msupplus{}.    (a  |  b  \mLeftarrow{}{}\mRightarrow{}  \mexists{}c:\mBbbN{}\msupplus{}.  (b  =  (a  *  c)))


By

---

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

---

Home Index