---

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


1. d : ℤ
2. 0 < d
3. ∀a:ℤ. ∀P:{a..a + (d - 1)-} ⟶ ℙ.  (¬¬(∀i:{a..a + (d - 1)-}. (P[i] ∨ (¬P[i]))))
4. a : ℤ
5. P : {a..a + d-} ⟶ ℙ
6. ¬¬(∀i:{a..a + (d - 1)-}. (P[i] ∨ (¬P[i])))
7. ¬¬(P[a + (d - 1)] ∨ (¬P[a + (d - 1)]))
⊢ ¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i])))
BY
{ RepeatFor 2 ((SupposeMore (-2) THENA Auto)) }

1
1. d : ℤ
2. 0 < d
3. ∀a:ℤ. ∀P:{a..a + (d - 1)-} ⟶ ℙ.  (¬¬(∀i:{a..a + (d - 1)-}. (P[i] ∨ (¬P[i]))))
4. a : ℤ
5. P : {a..a + d-} ⟶ ℙ
6. ∀i:{a..a + (d - 1)-}. (P[i] ∨ (¬P[i]))
7. P[a + (d - 1)] ∨ (¬P[a + (d - 1)])
⊢ ¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i])))

---

Latex:

---

Latex:

1.  d  :  \mBbbZ{}
2.  0  <  d
3.  \mforall{}a:\mBbbZ{}.  \mforall{}P:\{a..a  +  (d  -  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}.    (\mneg{}\mneg{}(\mforall{}i:\{a..a  +  (d  -  1)\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i]))))
4.  a  :  \mBbbZ{}
5.  P  :  \{a..a  +  d\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}
6.  \mneg{}\mneg{}(\mforall{}i:\{a..a  +  (d  -  1)\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i])))
7.  \mneg{}\mneg{}(P[a  +  (d  -  1)]  \mvee{}  (\mneg{}P[a  +  (d  -  1)]))
\mvdash{}  \mneg{}\mneg{}(\mforall{}i:\{a..a  +  d\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i])))


By

---

Latex:
RepeatFor  2  ((SupposeMore  (-2)  THENA  Auto))

---

Home Index