---

Step * of Lemma r2-equidistant-implies

∀a,b:ℝ^2.  (a ≠ b ⇒ (∀x:ℝ^2. (ax=bx ⇒ (∃t:ℝ. req-vec(2;x;vec-midpoint(a;b) + t*r2-perp(b - a))))))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (Assert r0 < ||b - a|| BY
               (Fold `real-vec-dist` 0 THEN RWO "real-vec-dist-symmetry" 0 THEN Auto))
   THEN Auto
   THEN Assert ⌜x - vec-midpoint(a;b)⋅b - a = r0⌝⋅) }

1
.....assertion..... 
1. a : ℝ^2
2. b : ℝ^2
3. a ≠ b
4. r0 < ||b - a||
5. x : ℝ^2
6. ax=bx
⊢ x - vec-midpoint(a;b)⋅b - a = r0

2
1. a : ℝ^2
2. b : ℝ^2
3. a ≠ b
4. r0 < ||b - a||
5. x : ℝ^2
6. ax=bx
7. x - vec-midpoint(a;b)⋅b - a = r0
⊢ ∃t:ℝ. req-vec(2;x;vec-midpoint(a;b) + t*r2-perp(b - a))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}\^{}2.    (a  \mneq{}  b  {}\mRightarrow{}  (\mforall{}x:\mBbbR{}\^{}2.  (ax=bx  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  req-vec(2;x;vec-midpoint(a;b)  +  t*r2-perp(b  -  a))))))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (Assert  r0  <  ||b  -  a||  BY
                          (Fold  `real-vec-dist`  0  THEN  RWO  "real-vec-dist-symmetry"  0  THEN  Auto))
  THEN  Auto
  THEN  Assert  \mkleeneopen{}x  -  vec-midpoint(a;b)\mcdot{}b  -  a  =  r0\mkleeneclose{}\mcdot{})

---

Home Index