---

Step * of Lemma rv-five-segment

∀[n:ℕ]. ∀[a,b,c,d,A,B,C,D:ℝ^n].  (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A-B-C and a-b-c)
BY
{ (RepUR ``rv-congruent rv-between`` 0
   THEN Auto
   THEN ((Assert d(c;d) = rsqrt(d(c;d)^2) BY (RWW "rnexp2 rsqrt-of-square" 0 THEN Auto)) THEN (RWO "-1" 0 THENA Auto))
   THEN (Assert d(C;D) = rsqrt(d(C;D)^2) BY
               (RWW "rnexp2 rsqrt-of-square" 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN (BLemma `rsqrt_functionality` THENA 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. 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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b,c,d,A,B,C,D:\mBbbR{}\^{}n].
    (cd=CD)  supposing  (bd=BD  and  ad=AD  and  bc=BC  and  ab=AB  and  A-B-C  and  a-b-c)


By

---

Latex:
(RepUR  ``rv-congruent  rv-between``  0
  THEN  Auto
  THEN  ((Assert  d(c;d)  =  rsqrt(d(c;d)\^{}2)  BY
                            (RWW  "rnexp2  rsqrt-of-square"  0  THEN  Auto))
              THEN  (RWO  "-1"  0  THENA  Auto)
              )
  THEN  (Assert  d(C;D)  =  rsqrt(d(C;D)\^{}2)  BY
                          (RWW  "rnexp2  rsqrt-of-square"  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (BLemma  `rsqrt\_functionality`  THENA  Auto))

---

Home Index