---

Step * 1 of Lemma rv-five-segment


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : ℝ^n
6. A : ℝ^n
7. B : ℝ^n
8. C : ℝ^n
9. D : ℝ^n
10. a-b-c
11. a ≠ c
12. A-B-C
13. A ≠ C
14. d(a;b) = d(A;B)
15. d(b;c) = d(B;C)
16. d(a;d) = d(A;D)
17. d(b;d) = d(B;D)
18. d(c;d) = rsqrt(d(c;d)^2)
19. d(C;D) = rsqrt(d(C;D)^2)
⊢ d(c;d)^2 = d(C;D)^2
BY
{ ((RWO "real-vec-dist-symmetry" 0 THENA Auto) THEN D -10 THEN D -8) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : ℝ^n
6. A : ℝ^n
7. B : ℝ^n
8. C : ℝ^n
9. D : ℝ^n
10. t : ℝ
11. (t ∈ (r0, r1)) ∧ req-vec(n;b;t*a + r1 - t*c)
12. a ≠ c
13. t1 : ℝ
14. (t1 ∈ (r0, r1)) ∧ req-vec(n;B;t1*A + r1 - t1*C)
15. A ≠ C
16. d(a;b) = d(A;B)
17. d(b;c) = d(B;C)
18. d(a;d) = d(A;D)
19. d(b;d) = d(B;D)
20. d(c;d) = rsqrt(d(c;d)^2)
21. d(C;D) = rsqrt(d(C;D)^2)
⊢ d(d;c)^2 = d(D;C)^2

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  d  :  \mBbbR{}\^{}n
6.  A  :  \mBbbR{}\^{}n
7.  B  :  \mBbbR{}\^{}n
8.  C  :  \mBbbR{}\^{}n
9.  D  :  \mBbbR{}\^{}n
10.  a-b-c
11.  a  \mneq{}  c
12.  A-B-C
13.  A  \mneq{}  C
14.  d(a;b)  =  d(A;B)
15.  d(b;c)  =  d(B;C)
16.  d(a;d)  =  d(A;D)
17.  d(b;d)  =  d(B;D)
18.  d(c;d)  =  rsqrt(d(c;d)\^{}2)
19.  d(C;D)  =  rsqrt(d(C;D)\^{}2)
\mvdash{}  d(c;d)\^{}2  =  d(C;D)\^{}2


By

---

Latex:
((RWO  "real-vec-dist-symmetry"  0  THENA  Auto)  THEN  D  -10  THEN  D  -8)

---

Home Index