---

Step * of Lemma rv-pos-angle-implies

∀n:ℕ. ∀a,b,c:ℝ^n.
  (rv-pos-angle(n;a;b;c)
  ⇒ (rv-pos-angle(n;c;b;a)
     ∧ rv-pos-angle(n;c;a;b)
     ∧ a ≠ c
     ∧ (¬a-b-c)
     ∧ (∀z:ℝ^n. (z ≠ b ⇒ (¬rv-pos-angle(n;a;b;z)) ⇒ rv-pos-angle(n;z;b;c)))))
BY
{ (EAuto 1
   THEN Try ((FLemma `rv-pos-angle-implies-separated` [-3] THEN Auto))
   THEN InstLemma `rv-pos-angle-shift` [⌜n⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜z⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.
    (rv-pos-angle(n;a;b;c)
    {}\mRightarrow{}  (rv-pos-angle(n;c;b;a)
          \mwedge{}  rv-pos-angle(n;c;a;b)
          \mwedge{}  a  \mneq{}  c
          \mwedge{}  (\mneg{}a-b-c)
          \mwedge{}  (\mforall{}z:\mBbbR{}\^{}n.  (z  \mneq{}  b  {}\mRightarrow{}  (\mneg{}rv-pos-angle(n;a;b;z))  {}\mRightarrow{}  rv-pos-angle(n;z;b;c)))))


By

---

Latex:
(EAuto  1
  THEN  Try  ((FLemma  `rv-pos-angle-implies-separated`  [-3]  THEN  Auto))
  THEN  InstLemma  `rv-pos-angle-shift`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index