---

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

.....equality..... 
1. r : ℝ
2. n : ℕ+
3. v : ℤ
4. (r n) = v ∈ ℤ
⊢ imin(|v|;imax(0;v)) + imax(-|v|;imin(0;v)) ~ v
BY
{ ((RWO "absval_unfold" 0 THENA Auto) THEN AutoSplit THEN (RWW "imin_unfold imax_unfold" 0 THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:
.....equality..... 
1.  r  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  v  :  \mBbbZ{}
4.  (r  n)  =  v
\mvdash{}  imin(|v|;imax(0;v))  +  imax(-|v|;imin(0;v))  \msim{}  v


By

---

Latex:
((RWO  "absval\_unfold"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (RWW  "imin\_unfold  imax\_unfold"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index