---

Step * 2 of Lemma fund-theorem-arithmetic


1. b : bag(Prime)
⊢ ∃a:ℕ+. (factors(a) = b ∈ bag(Prime))
BY
{ xxx(With ⌜Π(b)⌝ (D 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  b  :  bag(Prime)
\mvdash{}  \mexists{}a:\mBbbN{}\msupplus{}.  (factors(a)  =  b)


By

---

Latex:
xxx(With  \mkleeneopen{}\mPi{}(b)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index