---

Step * of Lemma div-search-lemma

∀a:ℤ. ∀b:{a + 1...}. ∀f:ℤ ⟶ 𝔹.
  ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))] 
  supposing ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))]
BY
{ Auto }

1
1. a : ℤ
2. b : {a + 1...}
3. f : ℤ ⟶ 𝔹
4. [%] : ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))]
⊢ ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))]

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  \mforall{}b:\{a  +  1...\}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.
    \mexists{}x:\{a..b\msupminus{}\}  [((\mforall{}y:\{a..x  +  1\msupminus{}\}.  (\mneg{}\muparrow{}(f  y)))  \mwedge{}  (\mforall{}z:\{x  +  1..b  +  1\msupminus{}\}.  (\muparrow{}(f  z))))] 
    supposing  \mexists{}x:\{a..b\msupminus{}\}  [((\mforall{}y:\{a..x  +  1\msupminus{}\}.  (\mneg{}\muparrow{}(f  y)))  \mwedge{}  (\mforall{}z:\{x  +  1..b  +  1\msupminus{}\}.  (\muparrow{}(f  z))))]


By

---

Latex:
Auto

---

Home Index