---

Step * of Lemma rv-between-translation

∀n:ℕ. ∀a,b,c,z:ℝ^n.  (z + a-z + b-z + c ⇐⇒ a-b-c)
BY
{ (Auto
   THEN RepeatFor 3 (ParallelLast)
   THEN Try ((RWO "real-vec-dist-translation2" 0 THEN Auto))
   THEN Try ((RWO "real-vec-dist-translation2" (-1) THEN Auto))
   THEN RepeatFor 4 (ParallelLast)
   THEN RepUR ``real-vec-add real-vec-sub real-vec-mul`` -1
   THEN RepUR ``real-vec-add real-vec-sub real-vec-mul`` 0) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. z : ℝ^n
6. z + a ≠ z + c
7. t : ℝ
8. t ∈ (r0, r1)
9. ∀i:ℕn. ((z + b i) = (t*z + a + r1 - t*z + c i))
10. i : ℕn
11. ((z i) + (b i)) = ((t * ((z i) + (a i))) + ((r1 - t) * ((z i) + (c i))))
⊢ (b i) = ((t * (a i)) + ((r1 - t) * (c i)))

2
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. z : ℝ^n
6. a ≠ c
7. t : ℝ
8. t ∈ (r0, r1)
9. ∀i:ℕn. ((b i) = (t*a + r1 - t*c i))
10. i : ℕn
11. (b i) = ((t * (a i)) + ((r1 - t) * (c i)))
⊢ ((z i) + (b i)) = ((t * ((z i) + (a i))) + ((r1 - t) * ((z i) + (c i))))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c,z:\mBbbR{}\^{}n.    (z  +  a-z  +  b-z  +  c  \mLeftarrow{}{}\mRightarrow{}  a-b-c)


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (ParallelLast)
  THEN  Try  ((RWO  "real-vec-dist-translation2"  0  THEN  Auto))
  THEN  Try  ((RWO  "real-vec-dist-translation2"  (-1)  THEN  Auto))
  THEN  RepeatFor  4  (ParallelLast)
  THEN  RepUR  ``real-vec-add  real-vec-sub  real-vec-mul``  -1
  THEN  RepUR  ``real-vec-add  real-vec-sub  real-vec-mul``  0)

---

Home Index