---

Step * 2 of Lemma real-vec-between_functionality


1. n : ℕ
2. a1 : ℝ^n
3. a2 : ℝ^n
4. b1 : ℝ^n
5. b2 : ℝ^n
6. c1 : ℝ^n
7. c2 : ℝ^n
8. req-vec(n;a1;a2)
9. req-vec(n;b1;b2)
10. req-vec(n;c1;c2)
11. t : ℝ
12. t ∈ (r0, r1)
13. req-vec(n;b2;t*a2 + r1 - t*c2)
⊢ req-vec(n;b1;t*a1 + r1 - t*c1)
BY
{ (RWO  "8< 9< 10<" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a1  :  \mBbbR{}\^{}n
3.  a2  :  \mBbbR{}\^{}n
4.  b1  :  \mBbbR{}\^{}n
5.  b2  :  \mBbbR{}\^{}n
6.  c1  :  \mBbbR{}\^{}n
7.  c2  :  \mBbbR{}\^{}n
8.  req-vec(n;a1;a2)
9.  req-vec(n;b1;b2)
10.  req-vec(n;c1;c2)
11.  t  :  \mBbbR{}
12.  t  \mmember{}  (r0,  r1)
13.  req-vec(n;b2;t*a2  +  r1  -  t*c2)
\mvdash{}  req-vec(n;b1;t*a1  +  r1  -  t*c1)


By

---

Latex:
(RWO    "8<  9<  10<"  (-1)  THEN  Auto)

---

Home Index