---

Step * 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-} ⟶ ℙ
⊢ ¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i])))
BY
{ ((Assert ¬¬(∀i:{a..a + (d - 1)-}. (P[i] ∨ (¬P[i]))) BY
          Auto)
   THEN (Assert ¬¬(P[a + (d - 1)] ∨ (¬P[a + (d - 1)])) BY
               (BLemma `not-not-1-xmiddle` THEN 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{}
\mvdash{}  \mneg{}\mneg{}(\mforall{}i:\{a..a  +  d\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i])))


By

---

Latex:
((Assert  \mneg{}\mneg{}(\mforall{}i:\{a..a  +  (d  -  1)\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i])))  BY
                Auto)
  THEN  (Assert  \mneg{}\mneg{}(P[a  +  (d  -  1)]  \mvee{}  (\mneg{}P[a  +  (d  -  1)]))  BY
                          (BLemma  `not-not-1-xmiddle`  THEN  Auto))
  )

---

Home Index