---

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


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

1
1. A : ℕ ⟶ ℙ
2. (∀i:ℕ. (¬¬A[i])) ⇒ (¬¬(∀i:ℕ. A[i]))@i
3. ¬((¬(∀i:ℕ. A[i])) ⇒ (∃n:ℕ. (¬A[n])))@i
⊢ False

---

Latex:

---

Latex:

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


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index