---

Step * 1 1 1 2 of Lemma DNS-iff-not-not-GMP


1. A : ℕ ⟶ ℙ
2. (∀i:ℕ. (¬¬A[i])) ⇒ (¬¬(∀i:ℕ. A[i]))@i
3. ¬((¬(∀i:ℕ. A[i])) ⇒ (∃n:ℕ. (¬A[n])))@i
4. ¬(∃n:ℕ. (¬A[n]))
⊢ False
BY
{ (D 2 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  (\mforall{}i:\mBbbN{}.  (\mneg{}\mneg{}A[i]))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mforall{}i:\mBbbN{}.  A[i]))@i
3.  \mneg{}((\mneg{}(\mforall{}i:\mBbbN{}.  A[i]))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  (\mneg{}A[n])))@i
4.  \mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}A[n]))
\mvdash{}  False


By

---

Latex:
(D  2  THEN  Auto)

---

Home Index