---

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


1. [P] : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. \\%2 : 0 < n@i
5. y : ℕ@i
6. (y ≤ (n - 1)) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ (n - 1)))@i
7. ¬P[n]
⊢ (∀y:ℕ. ¬P[y] supposing y ≤ n) ∨ (∃y:ℕ. ((y ≤ n) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ n))))
BY
{ (OrRight THENA Auto) }

1
1. [P] : ℕ ─→ ℙ
2. ∀n:ℕ. Dec(P[n])@i
3. n : ℤ@i
4. \\%2 : 0 < n@i
5. y : ℕ@i
6. (y ≤ (n - 1)) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ (n - 1)))@i
7. ¬P[n]
⊢ ∃y:ℕ. ((y ≤ n) ∧ P[y] ∧ (∀x:ℕ. ¬P[x] supposing y < x ∧ (x ≤ n)))

---

Latex:



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


By

(OrRight  THENA  Auto)

---

Home Index