Step * 1 1 1 of Lemma rmax_lb

.....assertion..... 
1. : ℝ
2. : ℝ
3. : ℝ
4. rnonneg(z -(x))
5. rnonneg(z -(y))
⊢ -(rmax(x;y)) rmin(-(x);-(y))
BY
(RWW "rmin-req-rminus-rmax rminus-rminus" THEN Auto) }


Latex:


Latex:
.....assertion..... 
1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  z  :  \mBbbR{}
4.  rnonneg(z  +  -(x))
5.  rnonneg(z  +  -(y))
\mvdash{}  -(rmax(x;y))  =  rmin(-(x);-(y))


By


Latex:
(RWW  "rmin-req-rminus-rmax  rminus-rminus"  0  THEN  Auto)




Home Index