---

Step * of Lemma prime-factors2

No Annotations
∀n:{2...}. (∃factors:{m:{2...}| prime(m)}  List [(n = Π(factors)  ∈ ℤ)])
BY
{ (InductionOnIntUpper THENA Auto) }

1
1. n : {2...}
2. ∀n1:{2..n-}. (∃factors:{m:{2...}| prime(m)}  List [(n1 = Π(factors)  ∈ ℤ)])
⊢ ∃factors:{m:{2...}| prime(m)}  List [(n = Π(factors)  ∈ ℤ)]

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\{2...\}.  (\mexists{}factors:\{m:\{2...\}|  prime(m)\}    List  [(n  =  \mPi{}(factors)  )])


By

---

Latex:
(InductionOnIntUpper  THENA  Auto)

---

Home Index