---

Step * of Lemma convex-comb-homog

∀[x,y,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ]. ∀[t:{t:ℝ| t ≠ r0} ].  (convex-comb(x;y;r * t;s * t) = convex-comb(x;y;r;s))
BY
{ (Intros
   THEN (Unhide THENW Auto)
   THEN (Assert (r * t) + (s * t) ≠ r0 BY
               (DSetVars THEN Unhide THEN Auto THEN nRMul ⌜t⌝ 5⋅ THEN Auto THEN nRNorm (-1) THEN Auto))
   THEN Auto
   THEN (Assert r + s ≠ r0 BY
               (DVar `s' THEN Unhide THEN Auto))
   THEN (RWO "convex-comb-req" 0 THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. r : ℝ
4. s : {s:ℝ| r + s ≠ r0} 
5. t : {t:ℝ| t ≠ r0} 
6. (r * t) + (s * t) ≠ r0
7. r + s ≠ r0
⊢ (((r1 - (s * t/(r * t) + (s * t))) * x) + ((s * t/(r * t) + (s * t)) * y))
= (((r1 - (s/r + s)) * x) + ((s/r + s) * y))

---

Latex:

---

Latex:
\mforall{}[x,y,r:\mBbbR{}].  \mforall{}[s:\{s:\mBbbR{}|  r  +  s  \mneq{}  r0\}  ].  \mforall{}[t:\{t:\mBbbR{}|  t  \mneq{}  r0\}  ].
    (convex-comb(x;y;r  *  t;s  *  t)  =  convex-comb(x;y;r;s))


By

---

Latex:
(Intros
  THEN  (Unhide  THENW  Auto)
  THEN  (Assert  (r  *  t)  +  (s  *  t)  \mneq{}  r0  BY
                          (DSetVars
                            THEN  Unhide
                            THEN  Auto
                            THEN  nRMul  \mkleeneopen{}t\mkleeneclose{}  5\mcdot{}
                            THEN  Auto
                            THEN  nRNorm  (-1)
                            THEN  Auto))
  THEN  Auto
  THEN  (Assert  r  +  s  \mneq{}  r0  BY
                          (DVar  `s'  THEN  Unhide  THEN  Auto))
  THEN  (RWO  "convex-comb-req"  0  THENA  Auto))

---

Home Index