---

Step * of Lemma rmax-ub-convex

∀a,b,t:ℝ.  ((r0 ≤ t) ⇒ (t ≤ r1) ⇒ (((t * a) + ((r1 - t) * b)) ≤ rmax(a;b)))
BY
{ (Auto
   THEN (Assert (t * a) ≤ (t * rmax(a;b)) BY
               ((Assert a ≤ rmax(a;b) BY Auto) THEN nRMul ⌜t⌝ (-1)⋅ THEN Auto))
   THEN (Assert ((r1 - t) * b) ≤ ((r1 - t) * rmax(a;b)) BY
               ((Assert b ≤ rmax(a;b) BY Auto) THEN nRMul ⌜r1 - t⌝ (-1)⋅ THEN Auto))
   THEN RWO "-1 -2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b,t:\mBbbR{}.    ((r0  \mleq{}  t)  {}\mRightarrow{}  (t  \mleq{}  r1)  {}\mRightarrow{}  (((t  *  a)  +  ((r1  -  t)  *  b))  \mleq{}  rmax(a;b)))


By

---

Latex:
(Auto
  THEN  (Assert  (t  *  a)  \mleq{}  (t  *  rmax(a;b))  BY
                          ((Assert  a  \mleq{}  rmax(a;b)  BY  Auto)  THEN  nRMul  \mkleeneopen{}t\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  (Assert  ((r1  -  t)  *  b)  \mleq{}  ((r1  -  t)  *  rmax(a;b))  BY
                          ((Assert  b  \mleq{}  rmax(a;b)  BY  Auto)  THEN  nRMul  \mkleeneopen{}r1  -  t\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  RWO  "-1  -2"  0
  THEN  Auto)

---

Home Index