---

Step * of Lemma posint_fact_exists

∀i:ℕ+. (∃ps:{j:ℕ+| prime(j)}  List [(i = (Π ps) ∈ ℤ)])
BY
{ ((D 0) THENA Auto) }

1
1. i : ℕ+
⊢ ∃ps:{j:ℕ+| prime(j)}  List [(i = (Π ps) ∈ ℤ)]

---

Latex:

---

Latex:
\mforall{}i:\mBbbN{}\msupplus{}.  (\mexists{}ps:\{j:\mBbbN{}\msupplus{}|  prime(j)\}    List  [(i  =  (\mPi{}  ps))])


By

---

Latex:
((D  0)  THENA  Auto)

---

Home Index