---

Step * 1 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
{ ((RemoveDoubleNegation THEN Auto) THEN Decide ⌜i < a + (d - 1)⌝⋅ 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)])
8. i : {a..a + d-}
9. ¬i < a + (d - 1)
⊢ 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.  \mforall{}i:\{a..a  +  (d  -  1)\msupminus{}\}.  (P[i]  \mvee{}  (\mneg{}P[i]))
7.  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:
((RemoveDoubleNegation  THEN  Auto)  THEN  Decide  \mkleeneopen{}i  <  a  +  (d  -  1)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index