---

Step * of Lemma accum-induction-factorial

∀n:ℕ. (∃x:{ℤ| ((n)! = x ∈ ℤ)})
BY
{ (InstLemma `accum-induction-ext` [⌜λ2n.∃x:{ℤ| ((n)! = x ∈ ℤ)}⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}x:\{\mBbbZ{}|  ((n)!  =  x)\})


By

---

Latex:
(InstLemma  `accum-induction-ext`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.\mexists{}x:\{\mBbbZ{}|  ((n)!  =  x)\}\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index