---

Step * of Lemma between-rmin-rmax

No Annotations
∀[x,y,t:ℝ].  uiff((rmin(x;y) ≤ t) ∧ (t ≤ rmax(x;y));(|t - x| ≤ |y - x|) ∧ (|t - y| ≤ |y - x|))
BY
{ (Intros
   THEN (D 0 THENA Auto)
   THEN Intro
   THEN (Unhide THENA Auto)
   THEN (StableCases ⌜x < y⌝⋅ THENA (Auto THEN BLemma `stable__and` THEN Auto))
   THEN Try (((FLemma `not-rless` [-1] THENA Auto)
              THEN Thin (-2)
              THEN SwapVars `x' `y'
              THEN (All (RWO "rmin-com rmax-com") THENA Auto)))
   THEN (Assert rmin(x;y) = x BY
               Auto)
   THEN (Assert rmax(x;y) = y BY
               Auto)
   THEN ((RWO "-1 -2" 4 ORELSE RWO "-1 -2" 0) THENA Auto)
   THEN RepeatFor 2 (Thin (-1))
   THEN Try (((Assert |y - x| = (y - x) BY
                     (RWO "rabs-of-nonneg" 0 THEN Auto))
              THEN ((RWO "-1" 4 ORELSE RWO "-1" 0) THENA Auto)
              THEN Thin (-1)))
   THEN Try (((Assert |x - y| = (y - x) BY
                     (RWO "rabs-of-nonpos" 0 THEN Auto))
              THEN ((RWO "-1" 4 ORELSE RWO "-1" 0) THENA Auto)
              THEN Thin (-1)))
   THEN All (RWO "rabs-difference-bound-rleq")
   THEN Auto
   THEN (RWO "4<" 0 ORELSE RWO "5" 0)⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y,t:\mBbbR{}].    uiff((rmin(x;y)  \mleq{}  t)  \mwedge{}  (t  \mleq{}  rmax(x;y));(|t  -  x|  \mleq{}  |y  -  x|)  \mwedge{}  (|t  -  y|  \mleq{}  |y  -  x|))


By

---

Latex:
(Intros
  THEN  (D  0  THENA  Auto)
  THEN  Intro
  THEN  (Unhide  THENA  Auto)
  THEN  (StableCases  \mkleeneopen{}x  <  y\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  BLemma  `stable\_\_and`  THEN  Auto))
  THEN  Try  (((FLemma  `not-rless`  [-1]  THENA  Auto)
                        THEN  Thin  (-2)
                        THEN  SwapVars  `x'  `y'
                        THEN  (All  (RWO  "rmin-com  rmax-com")  THENA  Auto)))
  THEN  (Assert  rmin(x;y)  =  x  BY
                          Auto)
  THEN  (Assert  rmax(x;y)  =  y  BY
                          Auto)
  THEN  ((RWO  "-1  -2"  4  ORELSE  RWO  "-1  -2"  0)  THENA  Auto)
  THEN  RepeatFor  2  (Thin  (-1))
  THEN  Try  (((Assert  |y  -  x|  =  (y  -  x)  BY
                                      (RWO  "rabs-of-nonneg"  0  THEN  Auto))
                        THEN  ((RWO  "-1"  4  ORELSE  RWO  "-1"  0)  THENA  Auto)
                        THEN  Thin  (-1)))
  THEN  Try  (((Assert  |x  -  y|  =  (y  -  x)  BY
                                      (RWO  "rabs-of-nonpos"  0  THEN  Auto))
                        THEN  ((RWO  "-1"  4  ORELSE  RWO  "-1"  0)  THENA  Auto)
                        THEN  Thin  (-1)))
  THEN  All  (RWO  "rabs-difference-bound-rleq")
  THEN  Auto
  THEN  (RWO  "4<"  0  ORELSE  RWO  "5"  0)\mcdot{}
  THEN  Auto)

---

Home Index