---

Step * 2 2 2 1 1 of Lemma max-of-intset


1. P : ℕ ⟶ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. 0 < n@i
5. ∀y:ℕ. ¬P[y] supposing y ≤ (n - 1)@i
6. ¬P[n]
7. y : ℕ@i
8. y ≤ n
⊢ ¬P[y]
BY
{ Assert ⌜(y ≤ (n - 1)) ∨ (y = n ∈ ℤ)⌝⋅ }

1
.....assertion..... 
1. P : ℕ ⟶ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. 0 < n@i
5. ∀y:ℕ. ¬P[y] supposing y ≤ (n - 1)@i
6. ¬P[n]
7. y : ℕ@i
8. y ≤ n
⊢ (y ≤ (n - 1)) ∨ (y = n ∈ ℤ)

2
1. P : ℕ ⟶ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. 0 < n@i
5. ∀y:ℕ. ¬P[y] supposing y ≤ (n - 1)@i
6. ¬P[n]
7. y : ℕ@i
8. y ≤ n
9. (y ≤ (n - 1)) ∨ (y = n ∈ ℤ)
⊢ ¬P[y]

---

Latex:

---

Latex:

1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}n:\mBbbN{}.  Dec(P[n])@i
3.  n  :  \mBbbZ{}@i
4.  0  <  n@i
5.  \mforall{}y:\mBbbN{}.  \mneg{}P[y]  supposing  y  \mleq{}  (n  -  1)@i
6.  \mneg{}P[n]
7.  y  :  \mBbbN{}@i
8.  y  \mleq{}  n
\mvdash{}  \mneg{}P[y]


By

---

Latex:
Assert  \mkleeneopen{}(y  \mleq{}  (n  -  1))  \mvee{}  (y  =  n)\mkleeneclose{}\mcdot{}

---

Home Index