---

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

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

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  \mneg{}(\mexists{}n:\mBbbN{}.  (\mneg{}A[n]))


By

---

Latex:
(ParallelLast  THEN  Auto)

---

Home Index