---

Step * 1 1 1 of Lemma weakly-infinite-cases


1. S : ℕ ⟶ ℙ
2. w∃∞x.S[x]
3. A : ℕ ⟶ ℙ
4. ∀n:ℕ. (A[n] ⇒ S[n])
5. ¬w∃∞n.A[n]
6. n : ℕ
7. ∀q:ℕ. (¬(n < q ∧ A[q]))
8. n1 : ℕ
9. m : ℕ
10. (n ≤ m) ∧ (n1 ≤ m)
⊢ ¬¬(∃q:ℕ. (n1 < q ∧ S[q] ∧ (¬A[q])))
BY
{ ((With ⌜m⌝ (D 2)⋅ THENA Auto) THEN RepeatFor 4 (ParallelLast) THEN Auto) }

1
1. S : ℕ ⟶ ℙ
2. A : ℕ ⟶ ℙ
3. ∀n:ℕ. (A[n] ⇒ S[n])
4. ¬w∃∞n.A[n]
5. n : ℕ
6. ∀q:ℕ. (¬(n < q ∧ A[q]))
7. n1 : ℕ
8. m : ℕ
9. n ≤ m
10. n1 ≤ m
11. q : ℕ
12. m < q
13. S[q]
14. S[q]
⊢ ¬A[q]

---

Latex:

---

Latex:

1.  S  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  w\mexists{}\minfty{}x.S[x]
3.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}n:\mBbbN{}.  (A[n]  {}\mRightarrow{}  S[n])
5.  \mneg{}w\mexists{}\minfty{}n.A[n]
6.  n  :  \mBbbN{}
7.  \mforall{}q:\mBbbN{}.  (\mneg{}(n  <  q  \mwedge{}  A[q]))
8.  n1  :  \mBbbN{}
9.  m  :  \mBbbN{}
10.  (n  \mleq{}  m)  \mwedge{}  (n1  \mleq{}  m)
\mvdash{}  \mneg{}\mneg{}(\mexists{}q:\mBbbN{}.  (n1  <  q  \mwedge{}  S[q]  \mwedge{}  (\mneg{}A[q])))


By

---

Latex:
((With  \mkleeneopen{}m\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)  THEN  RepeatFor  4  (ParallelLast)  THEN  Auto)

---

Home Index