---

Step * of Lemma rat-zero-cases

∀x:ℤ × ℕ+. ((↓r0 ≤ ratreal(x)) ∨ (↓ratreal(x) ≤ r0))
BY
{ Intro }

1
1. x : ℤ × ℕ+
⊢ (↓r0 ≤ ratreal(x)) ∨ (↓ratreal(x) ≤ r0)

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  ((\mdownarrow{}r0  \mleq{}  ratreal(x))  \mvee{}  (\mdownarrow{}ratreal(x)  \mleq{}  r0))


By

---

Latex:
Intro

---

Home Index