---

Step * 1 1 1 1 of Lemma not-d-CCC-nat


1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
2. ∀h:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:ℕ. ((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ)))
3. ∀h:ℕ ⟶ ℕ. ((∃l:ℕ. 0 < h l) ∨ (∀l:ℕ. ((h l) = 0 ∈ ℤ)))
⊢ ∀f:ℕ ⟶ ℕ. ((∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ))))
BY
{ (ParallelLast THEN D -1 THEN Auto) }

1
1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) ⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
2. ∀h:ℕ ⟶ ℕ. ∃n:ℕ. ∀m:ℕ. ((∃l:ℕn. 0 < h l) ∨ (∀l:ℕm. ((h l) = 0 ∈ ℤ)))
3. ∀h:ℕ ⟶ ℕ. ((∃l:ℕ. 0 < h l) ∨ (∀l:ℕ. ((h l) = 0 ∈ ℤ)))
4. f : ℕ ⟶ ℕ
5. ∃l:ℕ. 0 < f l
⊢ (∀n:ℕ. ((f n) = 0 ∈ ℤ)) ∨ (¬(∀n:ℕ. ((f n) = 0 ∈ ℤ)))

---

Latex:

---

Latex:

1.  \mforall{}R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  (\muparrow{}(R  n  (g  n))))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  (\muparrow{}(R  n  m))))
2.  \mforall{}h:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}.  ((\mexists{}l:\mBbbN{}n.  0  <  h  l)  \mvee{}  (\mforall{}l:\mBbbN{}m.  ((h  l)  =  0)))
3.  \mforall{}h:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mexists{}l:\mBbbN{}.  0  <  h  l)  \mvee{}  (\mforall{}l:\mBbbN{}.  ((h  l)  =  0)))
\mvdash{}  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}n:\mBbbN{}.  ((f  n)  =  0))  \mvee{}  (\mneg{}(\mforall{}n:\mBbbN{}.  ((f  n)  =  0))))


By

---

Latex:
(ParallelLast  THEN  D  -1  THEN  Auto)

---

Home Index