---

Step * 1 of Lemma not-assert-bdd-all


1. n : ℕ
2. P : ℕn ⟶ 𝔹
3. ¬(∀i:ℕn. (↑P[i]))
⊢ ∃i:ℕn. (¬↑P[i])
BY
{ (SupposeNot THEN D -2 THEN Auto THEN SupposeNot) }

1
1. n : ℕ
2. P : ℕn ⟶ 𝔹
3. ¬(∃i:ℕn. (¬↑P[i]))
4. i : ℕn
5. ¬↑P[i]
⊢ ↑P[i]

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  P  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
3.  \mneg{}(\mforall{}i:\mBbbN{}n.  (\muparrow{}P[i]))
\mvdash{}  \mexists{}i:\mBbbN{}n.  (\mneg{}\muparrow{}P[i])


By

---

Latex:
(SupposeNot  THEN  D  -2  THEN  Auto  THEN  SupposeNot)

---

Home Index