---

Step * 1 1 of Lemma rmin_ub


1. x : ℝ@i
2. y : ℝ@i
3. z : ℝ@i
4. rnonneg(x + -(z))@i
5. rnonneg(y + -(z))@i
⊢ rnonneg(rmin(x;y) + -(z))
BY
{ ((RWO "radd_comm" 0 THENA Auto) THEN (RWO "radd-rmin" 0 THENA Auto) THEN (RWO "radd_comm" 0 THENA Auto)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. z : ℝ@i
4. rnonneg(x + -(z))@i
5. rnonneg(y + -(z))@i
⊢ rnonneg(rmin(x + -(z);y + -(z)))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \mBbbR{}@i
3.  z  :  \mBbbR{}@i
4.  rnonneg(x  +  -(z))@i
5.  rnonneg(y  +  -(z))@i
\mvdash{}  rnonneg(rmin(x;y)  +  -(z))


By

---

Latex:
((RWO  "radd\_comm"  0  THENA  Auto)
  THEN  (RWO  "radd-rmin"  0  THENA  Auto)
  THEN  (RWO  "radd\_comm"  0  THENA  Auto))

---

Home Index