---

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


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]))))
BY
{ (Auto
   THEN ((Decide ⌜a ≤ b⌝⋅ THENA Auto)
         THENL [(InstHyp [⌜b - a⌝;⌜a⌝;⌜P⌝] 1⋅ THEN Auto); (RemoveDoubleNegation THEN Auto)]
        )
   ) }

---

Latex:

---

Latex:

1.  \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]))))
\mvdash{}  \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:
(Auto
  THEN  ((Decide  \mkleeneopen{}a  \mleq{}  b\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(InstHyp  [\mkleeneopen{}b  -  a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]  1\mcdot{}  THEN  Auto);  (RemoveDoubleNegation  THEN  Auto)]
            )
  )

---

Home Index