---

Step * 1 1 2 1 1 of Lemma posint_well_fnd


1. ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b}
2. [P] : ℕ+ ⟶ ℙ
3. ∀j:ℕ+. ((∀k:ℕ+. (k < j ⇒ P[k])) ⇒ P[j])
4. n : ℕ+
⊢ P[n]
BY
{ TACTIC:Assert ⌜∀m:ℕ. P[m + 1]⌝⋅ }

1
.....assertion..... 
1. ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b}
2. [P] : ℕ+ ⟶ ℙ
3. ∀j:ℕ+. ((∀k:ℕ+. (k < j ⇒ P[k])) ⇒ P[j])
4. n : ℕ+
⊢ ∀m:ℕ. P[m + 1]

2
1. ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b}
2. [P] : ℕ+ ⟶ ℙ
3. ∀j:ℕ+. ((∀k:ℕ+. (k < j ⇒ P[k])) ⇒ P[j])
4. n : ℕ+
5. ∀m:ℕ. P[m + 1]
⊢ P[n]

---

Latex:

---

Latex:

1.  \mforall{}a,b:\mBbbN{}\msupplus{}.    \{((a  |  b)  \mwedge{}  (\mneg{}(b  |  a)))  {}\mRightarrow{}  a  <  b\}
2.  [P]  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}j:\mBbbN{}\msupplus{}.  ((\mforall{}k:\mBbbN{}\msupplus{}.  (k  <  j  {}\mRightarrow{}  P[k]))  {}\mRightarrow{}  P[j])
4.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  P[n]


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}m:\mBbbN{}.  P[m  +  1]\mkleeneclose{}\mcdot{}

---

Home Index