---

Step * of Lemma primefactors_wf

∀n:{2...}. (primefactors(n) ∈ {factors:{m:{2...}| prime(m)}  List| n = Π(factors)  ∈ ℤ} )
BY
{ (Auto THEN Unfold `primefactors` 0 THEN GenConclAtAddr [2;1] THEN Unfold `sq_exists` -2 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\{2...\}.  (primefactors(n)  \mmember{}  \{factors:\{m:\{2...\}|  prime(m)\}    List|  n  =  \mPi{}(factors)  \}  )


By

---

Latex:
(Auto  THEN  Unfold  `primefactors`  0  THEN  GenConclAtAddr  [2;1]  THEN  Unfold  `sq\_exists`  -2  THEN  Auto)

---

Home Index