---

Step * of Lemma r2-left-right-lemma

∀a,b,x,y:ℝ^2.  (r2-left(x;a;b) ⇒ r2-left(y;b;a) ⇒ (∃t:ℝ. ((t ∈ [r0, r1]) ∧ (|t*x + r1 - t*yab| = r0))))
BY
{ (Unfold `r2-left` 0
   THEN Auto
   THEN (RWO "r2-det-add" 0 THENA Auto)
   THEN (RWO "r2-det-mul" 0 THENA Auto)
   THEN (nRNorm 0 THENA Auto)) }

1
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. r0 < |xab|
6. r0 < |yba|
⊢ ∃t:ℝ. (((r0 ≤ t) ∧ (t ≤ r1)) ∧ ((|yab| + (|xab| * t) + -(|yab| * t)) = r0))

---

Latex:

---

Latex:
\mforall{}a,b,x,y:\mBbbR{}\^{}2.
    (r2-left(x;a;b)  {}\mRightarrow{}  r2-left(y;b;a)  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  ((t  \mmember{}  [r0,  r1])  \mwedge{}  (|t*x  +  r1  -  t*yab|  =  r0))))


By

---

Latex:
(Unfold  `r2-left`  0
  THEN  Auto
  THEN  (RWO  "r2-det-add"  0  THENA  Auto)
  THEN  (RWO  "r2-det-mul"  0  THENA  Auto)
  THEN  (nRNorm  0  THENA  Auto))

---

Home Index