---

Step * of Lemma r2-left-right

∀a,b,x,y:ℝ^2.  (r2-left(x;a;b) ⇒ r2-left(y;b;a) ⇒ (∃z:ℝ^2. (rv-T(2;x;z;y) ∧ (¬rv-pos-angle(2;z;a;b)))))
BY
{ (InstLemma `r2-left-right-lemma` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN ExRepD
   THEN D 0 With ⌜t*x + r1 - t*y⌝ 
   THEN Auto) }

1
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. r2-left(x;a;b)
6. r2-left(y;b;a)
7. t : ℝ
8. t ∈ [r0, r1]
9. |t*x + r1 - t*yab| = r0
⊢ rv-T(2;x;t*x + r1 - t*y;y)

2
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. r2-left(x;a;b)
6. r2-left(y;b;a)
7. t : ℝ
8. t ∈ [r0, r1]
9. |t*x + r1 - t*yab| = r0
10. rv-T(2;x;t*x + r1 - t*y;y)
⊢ ¬rv-pos-angle(2;t*x + r1 - t*y;a;b)

---

Latex:

---

Latex:
\mforall{}a,b,x,y:\mBbbR{}\^{}2.
    (r2-left(x;a;b)  {}\mRightarrow{}  r2-left(y;b;a)  {}\mRightarrow{}  (\mexists{}z:\mBbbR{}\^{}2.  (rv-T(2;x;z;y)  \mwedge{}  (\mneg{}rv-pos-angle(2;z;a;b)))))


By

---

Latex:
(InstLemma  `r2-left-right-lemma`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}t*x  +  r1  -  t*y\mkleeneclose{} 
  THEN  Auto)

---

Home Index