---

Step * 1 of Lemma radd_functionality_wrt_rless1


1. x : ℝ
2. y : ℝ
3. z : ℝ
4. t : ℝ
5. rnonneg(z - x)
6. rpositive(t - y)
⊢ rpositive((z + t) - x + y)
BY
{ (((FLemma `rpositive-radd2` [-1; -2]) THENA Auto) THEN (nRNorm (-1)) THEN nRNorm 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  z  :  \mBbbR{}
4.  t  :  \mBbbR{}
5.  rnonneg(z  -  x)
6.  rpositive(t  -  y)
\mvdash{}  rpositive((z  +  t)  -  x  +  y)


By

---

Latex:
(((FLemma  `rpositive-radd2`  [-1;  -2])  THENA  Auto)  THEN  (nRNorm  (-1))  THEN  nRNorm  0  THEN  Auto)

---

Home Index