---

Step * of Lemma not-all-int_seg

∀i,j:ℤ.  ∀[P:{i..j-} ⟶ ℙ]. ((∀x:{i..j-}. Dec(P[x])) ⇒ (¬(∀x:{i..j-}. P[x]) ⇐⇒ ∃x:{i..j-}. (¬P[x])))
BY
{ Auto }

1
1. i : ℤ
2. j : ℤ
3. [P] : {i..j-} ⟶ ℙ
4. ∀x:{i..j-}. Dec(P[x])
5. ¬(∀x:{i..j-}. P[x])
⊢ ∃x:{i..j-}. (¬P[x])

2
1. i : ℤ
2. j : ℤ
3. P : {i..j-} ⟶ ℙ
4. ∀x:{i..j-}. Dec(P[x])
5. ∃x:{i..j-}. (¬P[x])
⊢ ¬(∀x:{i..j-}. P[x])

---

Latex:

---

Latex:
\mforall{}i,j:\mBbbZ{}.
    \mforall{}[P:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x:\{i..j\msupminus{}\}.  Dec(P[x]))  {}\mRightarrow{}  (\mneg{}(\mforall{}x:\{i..j\msupminus{}\}.  P[x])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:\{i..j\msupminus{}\}.  (\mneg{}P[x])))


By

---

Latex:
Auto

---

Home Index