---

Step * 1 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)
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
BY
{ ((Assert (t - r1) < r0 BY
          (All Reduce THEN nRAdd ⌜r1⌝ 0⋅ THEN Auto))
   THEN (Assert (t1 - r1) < r0 BY
               (All Reduce THEN nRAdd ⌜r1⌝ 0⋅ THEN Auto))
   ) }

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)))
26. (t - r1) < r0
27. (t1 - r1) < r0
⊢ 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)
12.  req-vec(n;b;t*a  +  r1  -  t*c)
13.  a  \mneq{}  c
14.  t1  :  \mBbbR{}
15.  t1  \mmember{}  (r0,  r1)
16.  req-vec(n;B;t1*A  +  r1  -  t1*C)
17.  A  \mneq{}  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)))
\mvdash{}  d(d;c)\^{}2  =  d(D;C)\^{}2


By

---

Latex:
((Assert  (t  -  r1)  <  r0  BY
                (All  Reduce  THEN  nRAdd  \mkleeneopen{}r1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (Assert  (t1  -  r1)  <  r0  BY
                          (All  Reduce  THEN  nRAdd  \mkleeneopen{}r1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  )

---

Home Index