---

Step * 1 of Lemma rmin-rmax-real-decomp


1. r : ℝ
⊢ (rmin(|r|;rmax(r0;r)) + rmax(-(|r|);rmin(r0;r))) = r
BY
{ ((BLemma `req-iff-bdd-diff` THENA Auto)
   THEN (RWO "radd-bdd-diff" 0 THENA Auto)
   THEN (D 0 With ⌜1⌝  THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepUR ``rmax rmin rabs rminus int-to-real`` 0
   THEN (GenConclTerm ⌜r n⌝⋅ THENA Auto)
   THEN (Subst' 2 * n * 0 ~ 0 0 THENA Auto)) }

1
1. r : ℝ
2. n : ℕ+
3. v : ℤ
4. (r n) = v ∈ ℤ
⊢ |(imin(|v|;imax(0;v)) + imax(-|v|;imin(0;v))) - v| ≤ 1

---

Latex:

---

Latex:

1.  r  :  \mBbbR{}
\mvdash{}  (rmin(|r|;rmax(r0;r))  +  rmax(-(|r|);rmin(r0;r)))  =  r


By

---

Latex:
((BLemma  `req-iff-bdd-diff`  THENA  Auto)
  THEN  (RWO  "radd-bdd-diff"  0  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``rmax  rmin  rabs  rminus  int-to-real``  0
  THEN  (GenConclTerm  \mkleeneopen{}r  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Subst'  2  *  n  *  0  \msim{}  0  0  THENA  Auto))

---

Home Index