---

Step * of Lemma rmax_wf

∀[x,y:ℝ].  (rmax(x;y) ∈ ℝ)
BY
{ (ProveWfLemma
   THEN D 1
   THEN D -1
   THEN (MemTypeCD THEN Auto)
   THEN All (Unfold `regular-int-seq`)
   THEN Reduce 0
   THEN Auto
   THEN RWO "mul-imax" 0
   THEN Auto
   THEN (RWO "absval-imax-difference" 0 THENA Auto)
   THEN BLemma `imax_lb`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (rmax(x;y)  \mmember{}  \mBbbR{})


By

---

Latex:
(ProveWfLemma
  THEN  D  1
  THEN  D  -1
  THEN  (MemTypeCD  THEN  Auto)
  THEN  All  (Unfold  `regular-int-seq`)
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "mul-imax"  0
  THEN  Auto
  THEN  (RWO  "absval-imax-difference"  0  THENA  Auto)
  THEN  BLemma  `imax\_lb`
  THEN  Auto)

---

Home Index