---

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


1. P : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. 0 < n@i
5. y : ℕ@i
6. y ≤ (n - 1)@i
7. P[y]@i
8. ∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ (n - 1))@i
9. ¬P[n]
10. y ≤ n
11. P[y]
12. x : ℕ@i
13. y < x
14. x ≤ n
⊢ ¬P[x]
BY
{ Assert ⌈(x ≤ (n - 1)) ∨ (x = n ∈ ℤ)⌉⋅ }

1
.....assertion..... 
1. P : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. 0 < n@i
5. y : ℕ@i
6. y ≤ (n - 1)@i
7. P[y]@i
8. ∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ (n - 1))@i
9. ¬P[n]
10. y ≤ n
11. P[y]
12. x : ℕ@i
13. y < x
14. x ≤ n
⊢ (x ≤ (n - 1)) ∨ (x = n ∈ ℤ)

2
1. P : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. 0 < n@i
5. y : ℕ@i
6. y ≤ (n - 1)@i
7. P[y]@i
8. ∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ (n - 1))@i
9. ¬P[n]
10. y ≤ n
11. P[y]
12. x : ℕ@i
13. y < x
14. x ≤ n
15. (x ≤ (n - 1)) ∨ (x = n ∈ ℤ)
⊢ ¬P[x]

---

Latex:



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


By

Assert  \mkleeneopen{}(x  \mleq{}  (n  -  1))  \mvee{}  (x  =  n)\mkleeneclose{}\mcdot{}

---

Home Index