---

Step * 1 of Lemma nat-inf-infinity-new


1. n : ℕ
2. ∞ = n∞ ∈ ℕ∞
⊢ False
BY
{ (ApFunToHypEquands `F' ⌜F n⌝ ⌜𝔹⌝ (-1)⋅ THEN Auto THEN RepUR ``nat-inf-infinity nat2inf`` -1) }

1
1. n : ℕ
2. ∞ = n∞ ∈ ℕ∞
3. tt = n <z n
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \minfty{}  =  n\minfty{}
\mvdash{}  False


By

---

Latex:
(ApFunToHypEquands  `F'  \mkleeneopen{}F  n\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto  THEN  RepUR  ``nat-inf-infinity  nat2inf``  -1)

---

Home Index