Step * of Lemma cont-induction-factorial

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


Latex:


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


By


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




Home Index