---

Step * 1 of Lemma convex-comb-homog


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))
BY
{ ((Assert (s * t/(r * t) + (s * t)) = (s/r + s) BY (BLemma `fractions-req` THEN Auto)) THEN RWO "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  r  :  \mBbbR{}
4.  s  :  \{s:\mBbbR{}|  r  +  s  \mneq{}  r0\} 
5.  t  :  \{t:\mBbbR{}|  t  \mneq{}  r0\} 
6.  (r  *  t)  +  (s  *  t)  \mneq{}  r0
7.  r  +  s  \mneq{}  r0
\mvdash{}  (((r1  -  (s  *  t/(r  *  t)  +  (s  *  t)))  *  x)  +  ((s  *  t/(r  *  t)  +  (s  *  t))  *  y))
=  (((r1  -  (s/r  +  s))  *  x)  +  ((s/r  +  s)  *  y))


By

---

Latex:
((Assert  (s  *  t/(r  *  t)  +  (s  *  t))  =  (s/r  +  s)  BY
                (BLemma  `fractions-req`  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index