---

Step * of Lemma real-vec-between-symmetry

∀n:ℕ. ∀a,b,c:ℝ^n.  (a-b-c ⇒ c-b-a)
BY
{ ((Auto THEN ParallelLast THEN ExRepD) THEN D 0 With ⌜r1 - t⌝  THEN Auto) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. t : ℝ
6. t ∈ (r0, r1)
7. req-vec(n;b;t*a + r1 - t*c)
⊢ r1 - t ∈ (r0, r1)

2
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. t : ℝ
6. t ∈ (r0, r1)
7. req-vec(n;b;t*a + r1 - t*c)
8. r1 - t ∈ (r0, r1)
⊢ req-vec(n;b;r1 - t*c + r1 - r1 - t*a)

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  ParallelLast  THEN  ExRepD)  THEN  D  0  With  \mkleeneopen{}r1  -  t\mkleeneclose{}    THEN  Auto)

---

Home Index