---

Step * 1 of Lemma r-triangle-inequality


1. x : ℝ
2. y : ℝ
⊢ rnonneg2((|x| + |y|) - |x + y|)
BY
{ ((RepUR ``rsub`` 0⋅ THEN (RWW "radd-bdd-diff" 0 THENA Auto))
   THEN (Assert bdd-diff(-(|x + y|);-(|λn.((x n) + (y n))|)) BY
               ((BLemma `rminus_functionality_wrt_bdd-diff`
                 THENA (Try (Complete (Auto)) THEN RepUR ``rabs rmax rminus`` 0 THEN Auto)
                 )
                THEN (BLemma `rabs_functionality_wrt_bdd-diff`
                      THENA (Try (Complete (Auto)) THEN RepUR ``rabs rmax rminus`` 0 THEN Auto)
                      )⋅
                THEN Auto))
   ) }

1
1. x : ℝ
2. y : ℝ
3. bdd-diff(-(|x + y|);-(|λn.((x n) + (y n))|))
⊢ rnonneg2(λn.(((|x| + |y|) n) + (-(|x + y|) n)))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
\mvdash{}  rnonneg2((|x|  +  |y|)  -  |x  +  y|)


By

---

Latex:
((RepUR  ``rsub``  0\mcdot{}  THEN  (RWW  "radd-bdd-diff"  0  THENA  Auto))
  THEN  (Assert  bdd-diff(-(|x  +  y|);-(|\mlambda{}n.((x  n)  +  (y  n))|))  BY
                          ((BLemma  `rminus\_functionality\_wrt\_bdd-diff`
                              THENA  (Try  (Complete  (Auto))  THEN  RepUR  ``rabs  rmax  rminus``  0  THEN  Auto)
                              )
                            THEN  (BLemma  `rabs\_functionality\_wrt\_bdd-diff`
                                        THENA  (Try  (Complete  (Auto))  THEN  RepUR  ``rabs  rmax  rminus``  0  THEN  Auto)
                                        )\mcdot{}
                            THEN  Auto))
  )

---

Home Index