---

Step * of Lemma r-bound-property

∀[x:ℝ]. ((r(-r-bound(x)) ≤ x) ∧ (x ≤ r(r-bound(x))))
BY
{ xxx(Auto
      THEN Unfold `r-bound` 0
      THEN (GenConclTerm ⌜TERMOF{integer-bound:o, 1:l} x⌝⋅ THENA Auto)
      THEN Thin (-1)
      THEN D -1
      THEN Reduce 0
      THEN (RenameVar `%' (-1)))xxx }

1
1. x : ℝ
2. n : ℕ+
3. |x| ≤ r(n)
⊢ r(-n) ≤ x

2
1. x : ℝ
2. r(-r-bound(x)) ≤ x
3. n : ℕ+
4. |x| ≤ r(n)
⊢ x ≤ r(n)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  ((r(-r-bound(x))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r(r-bound(x))))


By

---

Latex:
xxx(Auto
        THEN  Unfold  `r-bound`  0
        THEN  (GenConclTerm  \mkleeneopen{}TERMOF\{integer-bound:o,  1:l\}  x\mkleeneclose{}\mcdot{}  THENA  Auto)
        THEN  Thin  (-1)
        THEN  D  -1
        THEN  Reduce  0
        THEN  (RenameVar  `\%'  (-1)))xxx

---

Home Index