---

Step * 1 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. 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
BY
{ (((InstLemma `rv-five-segment-lemma` [⌜n⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝;⌜t⌝]⋅ THENA Auto) THEN RepUR ``let`` -1 THEN ExRepD)
   THEN (InstLemma `rv-five-segment-lemma` [⌜n⌝;⌜A⌝;⌜B⌝;⌜C⌝;⌜D⌝;⌜t1⌝]⋅ THENA Auto)
   THEN RepUR ``let`` -1
   THEN ExRepD) }

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)
12. req-vec(n;b;t*a + r1 - t*c)
13. a ≠ c
14. t1 : ℝ
15. t1 ∈ (r0, r1)
16. req-vec(n;B;t1*A + r1 - t1*C)
17. A ≠ C
18. d(a;b) = d(A;B)
19. d(b;c) = d(B;C)
20. d(a;d) = d(A;D)
21. d(b;d) = d(B;D)
22. d(c;d) = rsqrt(d(c;d)^2)
23. d(C;D) = rsqrt(d(C;D)^2)
24. d(d;c)^2 = (d(b;c)^2 + d(d;b)^2 + ((t/t - r1) * (d(a;d)^2 - d(a;b)^2 + d(d;b)^2)))
25. d(D;C)^2 = (d(B;C)^2 + d(D;B)^2 + ((t1/t1 - r1) * (d(A;D)^2 - d(A;B)^2 + d(D;B)^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.  t  :  \mBbbR{}
11.  (t  \mmember{}  (r0,  r1))  \mwedge{}  req-vec(n;b;t*a  +  r1  -  t*c)
12.  a  \mneq{}  c
13.  t1  :  \mBbbR{}
14.  (t1  \mmember{}  (r0,  r1))  \mwedge{}  req-vec(n;B;t1*A  +  r1  -  t1*C)
15.  A  \mneq{}  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)
\mvdash{}  d(d;c)\^{}2  =  d(D;C)\^{}2


By

---

Latex:
(((InstLemma  `rv-five-segment-lemma`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  RepUR  ``let``  -1
    THEN  ExRepD)
  THEN  (InstLemma  `rv-five-segment-lemma`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}t1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``let``  -1
  THEN  ExRepD)

---

Home Index