---

Step * of Lemma not-not-all-int_seg-xmiddle

No Annotations
∀a,b:ℤ. ∀P:{a..b-} ⟶ ℙ.  (¬¬(∀i:{a..b-}. (P[i] ∨ (¬P[i]))))
BY
{ Assert ⌜∀d:ℕ. ∀a:ℤ. ∀P:{a..a + d-} ⟶ ℙ.  (¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i]))))⌝⋅ }

1
.....assertion..... 
∀d:ℕ. ∀a:ℤ. ∀P:{a..a + d-} ⟶ ℙ.  (¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i]))))

2
1. ∀d:ℕ. ∀a:ℤ. ∀P:{a..a + d-} ⟶ ℙ.  (¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i]))))
⊢ ∀a,b:ℤ. ∀P:{a..b-} ⟶ ℙ.  (¬¬(∀i:{a..b-}. (P[i] ∨ (¬P[i]))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:\mBbbZ{}.  \mforall{}P:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}.    (\mneg{}\mneg{}(\mforall{}i:\{a..b\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i]))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}a:\mBbbZ{}.  \mforall{}P:\{a..a  +  d\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}.    (\mneg{}\mneg{}(\mforall{}i:\{a..a  +  d\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i]))))\mkleeneclose{}\mcdot{}

---

Home Index