---

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

.....assertion..... 
∀d:ℕ. ∀a:ℤ. ∀P:{a..a + d-} ⟶ ℙ.  (¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i]))))
BY
{ (InductionOnNat 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-} ⟶ ℙ
⊢ ¬¬(∀i:{a..a + d-}. (P[i] ∨ (¬P[i])))

---

Latex:

---

Latex:
.....assertion..... 
\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]))))


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index