---

Step * 1 1 1 1 of Lemma rmax-minus-rmin


1. a : ℝ@i
2. b : ℝ@i
3. n : ℕ+@i
⊢ |imax((a n) + (-(b n));-((a n) + (-(b n)))) - imax(a n;b n) + (-imin(a n;b n))| ≤ 0
BY
{ TACTIC:((RWO "imax_unfold imin_unfold" 0 THENA Auto)
          THEN Repeat (AutoSplit)
          THEN Auto'
          THEN ((RW IntNormC 0 THENA Auto) THEN RWO "absval_unfold" 0 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  b  :  \mBbbR{}@i
3.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  |imax((a  n)  +  (-(b  n));-((a  n)  +  (-(b  n))))  -  imax(a  n;b  n)  +  (-imin(a  n;b  n))|  \mleq{}  0


By

---

Latex:
TACTIC:((RWO  "imax\_unfold  imin\_unfold"  0  THENA  Auto)
                THEN  Repeat  (AutoSplit)
                THEN  Auto'
                THEN  ((RW  IntNormC  0  THENA  Auto)  THEN  RWO  "absval\_unfold"  0  THEN  Auto)\mcdot{})

---

Home Index