---

Step * 1 1 2 1 2 of Lemma real-vec-between-inner-trans


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : ℝ^n
6. s : ℝ
7. s ∈ (r0, r1)
8. req-vec(n;b;s*a + r1 - s*d)
9. t : ℝ
10. t ∈ (r0, r1)
11. req-vec(n;c;t*s*a + r1 - s*d + r1 - t*d)
12. r0 < (t * s)
13. (t * s) < r1
14. r0 < (r1 - t * s)
15. (s - t * s/r1 - t * s) ∈ (r0, r1)
⊢ req-vec(n;s*a + r1 - s*d;(s - t * s/r1 - t * s)*a + r1 - (s - t * s/r1 - t * s)*c)
BY
{ (RepUR ``req-vec real-vec-add real-vec-mul`` 0
   THEN Auto
   THEN MoveToConcl (-3)
   THEN (GenConclTerm ⌜r1 - t * s⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (D -8 With ⌜i⌝  THENA Auto)
   THEN RepUR ``req-vec real-vec-add real-vec-mul`` -1
   THEN (RWO "-1" 0 THENA Auto)
   THEN GenConclTerms Auto [⌜a i⌝;⌜d i⌝]⋅) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : ℝ^n
6. s : ℝ
7. s ∈ (r0, r1)
8. req-vec(n;b;s*a + r1 - s*d)
9. t : ℝ
10. t ∈ (r0, r1)
11. r0 < (t * s)
12. (t * s) < r1
13. (s - t * s/r1 - t * s) ∈ (r0, r1)
14. i : ℕn
15. v : ℝ
16. (r1 - t * s) = v ∈ ℝ
17. r0 < v
18. (c i) = ((t * ((s * (a i)) + ((r1 - s) * (d i)))) + ((r1 - t) * (d i)))
19. v1 : ℝ
20. (a i) = v1 ∈ ℝ
21. v2 : ℝ
22. (d i) = v2 ∈ ℝ
⊢ ((s * v1) + ((r1 - s) * v2))
= (((s - t * s/v) * v1) + ((r1 - (s - t * s/v)) * ((t * ((s * v1) + ((r1 - s) * v2))) + ((r1 - t) * v2))))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  d  :  \mBbbR{}\^{}n
6.  s  :  \mBbbR{}
7.  s  \mmember{}  (r0,  r1)
8.  req-vec(n;b;s*a  +  r1  -  s*d)
9.  t  :  \mBbbR{}
10.  t  \mmember{}  (r0,  r1)
11.  req-vec(n;c;t*s*a  +  r1  -  s*d  +  r1  -  t*d)
12.  r0  <  (t  *  s)
13.  (t  *  s)  <  r1
14.  r0  <  (r1  -  t  *  s)
15.  (s  -  t  *  s/r1  -  t  *  s)  \mmember{}  (r0,  r1)
\mvdash{}  req-vec(n;s*a  +  r1  -  s*d;(s  -  t  *  s/r1  -  t  *  s)*a  +  r1  -  (s  -  t  *  s/r1  -  t  *  s)*c)


By

---

Latex:
(RepUR  ``req-vec  real-vec-add  real-vec-mul``  0
  THEN  Auto
  THEN  MoveToConcl  (-3)
  THEN  (GenConclTerm  \mkleeneopen{}r1  -  t  *  s\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (D  -8  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``req-vec  real-vec-add  real-vec-mul``  -1
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};\mkleeneopen{}d  i\mkleeneclose{}]\mcdot{})

---

Home Index