---

Step * of Lemma rv-pos-angle-not-be

∀[n:ℕ]. ∀[a,b,c:ℝ^n].  ¬a_b_c supposing rv-pos-angle(n;a;b;c)
BY
{ (Auto
   THEN (FLemma `rv-pos-angle-not-between` [-1] THENA Auto)
   THEN (FLemma `rv-pos-angle-implies-separated2` [-2] THENA Auto)
   THEN (FLemma `rv-pos-angle-permute` [-3] THENA Auto)
   THEN (FLemma `rv-pos-angle-permute` [-1] THENA Auto)
   THEN (FLemma `rv-pos-angle-implies-separated2` [-1] THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. rv-pos-angle(n;a;b;c)
6. ¬a-b-c
7. a ≠ b
8. rv-pos-angle(n;c;a;b)
9. rv-pos-angle(n;b;c;a)
10. b ≠ c
⊢ ¬a_b_c

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b,c:\mBbbR{}\^{}n].    \mneg{}a\_b\_c  supposing  rv-pos-angle(n;a;b;c)


By

---

Latex:
(Auto
  THEN  (FLemma  `rv-pos-angle-not-between`  [-1]  THENA  Auto)
  THEN  (FLemma  `rv-pos-angle-implies-separated2`  [-2]  THENA  Auto)
  THEN  (FLemma  `rv-pos-angle-permute`  [-3]  THENA  Auto)
  THEN  (FLemma  `rv-pos-angle-permute`  [-1]  THENA  Auto)
  THEN  (FLemma  `rv-pos-angle-implies-separated2`  [-1]  THENA  Auto))

---

Home Index