---

Step * of Lemma rminus-nonneg

∀[x:ℝ]. (x = r0) supposing (rnonneg(-(x)) and rnonneg(x))
BY
{ (Auto
   THEN All (RepUR ``rnonneg rminus``)
   THEN (D 0 THEN Auto)
   THEN RepUR ``int-to-real`` 0
   THEN RW IntNormC 0
   THEN Auto
   THEN ∀h:hyp. (InstHyp [⌜n⌝] h⋅ THEN Auto) 
   THEN (RWO "absval_unfold" 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (x  =  r0)  supposing  (rnonneg(-(x))  and  rnonneg(x))


By

---

Latex:
(Auto
  THEN  All  (RepUR  ``rnonneg  rminus``)
  THEN  (D  0  THEN  Auto)
  THEN  RepUR  ``int-to-real``  0
  THEN  RW  IntNormC  0
  THEN  Auto
  THEN  \mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THEN  Auto) 
  THEN  (RWO  "absval\_unfold"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index