---

Step * 1 of Lemma nat_ind


1. [P] : ℕ ⟶ ℙ{k}
2. P[0]@k
3. ∀i:ℕ+. (P[i - 1] ⇒ P[i])@[k | i]
4. j : ℕ@i
⊢ P[j]
BY
{ (primNatInd 4 THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}
2.  P[0]@k
3.  \mforall{}i:\mBbbN{}\msupplus{}.  (P[i  -  1]  {}\mRightarrow{}  P[i])@[k  |  i]
4.  j  :  \mBbbN{}@i
\mvdash{}  P[j]


By

---

Latex:
(primNatInd  4  THEN  Auto)

---

Home Index