---

Step * 1 1 of Lemma rat-zero-cases

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

1
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>))

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
\mvdash{}  (\mdownarrow{}ratreal(ɘ,  1>)  \mleq{}  ratreal(x))  \mvee{}  (\mdownarrow{}ratreal(x)  \mleq{}  ratreal(ɘ,  1>))


By

---

Latex:
(Assert  TERMOF\{rat-rleq-cases-ext:o,  \mbackslash{}\mbackslash{}v:l\}  ɘ,  1>  x  \mmember{}  (\mdownarrow{}ratreal(ɘ,  1>)  \mleq{}  ratreal(x))  \mvee{}  (\mdownarrow{}ratreal(x\000C)  \mleq{}  ratreal(ɘ,  1>))  BY
              Auto)

---

Home Index