---

Step * of Lemma real-vec-between_functionality

∀n:ℕ. ∀a1,a2,b1,b2,c1,c2:ℝ^n.  (req-vec(n;a1;a2) ⇒ req-vec(n;b1;b2) ⇒ req-vec(n;c1;c2) ⇒ (a1-b1-c1 ⇐⇒ a2-b2-c2))
BY
{ (Auto THEN RepeatFor 3 (ParallelLast)) }

1
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;b1;t*a1 + r1 - t*c1)
⊢ req-vec(n;b2;t*a2 + r1 - t*c2)

2
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)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a1,a2,b1,b2,c1,c2:\mBbbR{}\^{}n.
    (req-vec(n;a1;a2)  {}\mRightarrow{}  req-vec(n;b1;b2)  {}\mRightarrow{}  req-vec(n;c1;c2)  {}\mRightarrow{}  (a1-b1-c1  \mLeftarrow{}{}\mRightarrow{}  a2-b2-c2))


By

---

Latex:
(Auto  THEN  RepeatFor  3  (ParallelLast))

---

Home Index