---

Step * of Lemma rmax-minus-rmin

∀a,b:ℝ.  (|a - b| = (rmax(a;b) - rmin(a;b)))
BY
{ (Auto THEN (RWO "rabs-as-rmax" 0 THENA Auto)) }

1
1. a : ℝ@i
2. b : ℝ@i
⊢ rmax(a - b;-(a - b)) = (rmax(a;b) - rmin(a;b))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    (|a  -  b|  =  (rmax(a;b)  -  rmin(a;b)))


By

---

Latex:
(Auto  THEN  (RWO  "rabs-as-rmax"  0  THENA  Auto))

---

Home Index