---

Step * 1 1 1 of Lemma rat-zero-cases


1. x : ℤ × ℕ+
2. TERMOF{rat-rleq-cases-ext:o, \\v:l} <0, 1> x ∈ (↓ratreal(<0, 1>) ≤ ratreal(x)) ∨ (↓ratreal(x) ≤ ratreal(<0, 1>))
⊢ (↓ratreal(<0, 1>) ≤ ratreal(x)) ∨ (↓ratreal(x) ≤ ratreal(<0, 1>))
BY
{ D 1 }

1
1. x1 : ℤ
2. x2 : ℕ+
3. TERMOF{rat-rleq-cases-ext:o, \\v:l} <0, 1> <x1, x2> ∈ (↓ratreal(<0, 1>) ≤ ratreal(<x1, x2>)) ∨ (↓ratreal(<x1, x2>) ≤ \000Cratreal(<0, 1>))
⊢ (↓ratreal(<0, 1>) ≤ ratreal(<x1, x2>)) ∨ (↓ratreal(<x1, x2>) ≤ ratreal(<0, 1>))

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  TERMOF\{rat-rleq-cases-ext:o,  \mbackslash{}\mbackslash{}v:l\}  ɘ,  1>  x  \mmember{}  (\mdownarrow{}ratreal(ɘ,  1>)  \mleq{}  ratreal(x))  \mvee{}  (\mdownarrow{}ratreal(x)  \mleq{}  r\000Catreal(ɘ,  1>))
\mvdash{}  (\mdownarrow{}ratreal(ɘ,  1>)  \mleq{}  ratreal(x))  \mvee{}  (\mdownarrow{}ratreal(x)  \mleq{}  ratreal(ɘ,  1>))


By

---

Latex:
D  1

---

Home Index