---

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

∀[A:ℕ ⟶ ℙ]. (DNSi.A[i] ⇐⇒ ¬¬GMPi.A[i]))
BY
{ Auto }

1
1. A : ℕ ⟶ ℙ
2. DNSi.A[i]@i
⊢ ¬¬GMPi.A[i])

2
1. A : ℕ ⟶ ℙ
2. ¬¬GMPi.A[i])@i
⊢ DNSi.A[i]

---

Latex:

---

Latex:
\mforall{}[A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (DNSi.A[i]  \mLeftarrow{}{}\mRightarrow{}  \mneg{}\mneg{}GMPi.A[i]))


By

---

Latex:
Auto

---

Home Index