---

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

∀n:ℕ. ∀a,b,c:ℝ^n.  ((¬rv-pos-angle(n;a;b;c)) ⇒ (¬((¬rv-T(n;a;b;c)) ∧ (¬rv-T(n;b;c;a)) ∧ (¬rv-T(n;c;a;b)))))
BY
{ (InstLemma `not-rv-pos-angle-implies` [] THEN RepeatFor 5 ((ParallelLast' 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 ∧ b ≠ c ∧ c ≠ a ∧ (¬a-b-c) ∧ (¬b-c-a) ∧ (¬c-a-b))
⊢ ¬((¬rv-T(n;a;b;c)) ∧ (¬rv-T(n;b;c;a)) ∧ (¬rv-T(n;c;a;b)))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `not-rv-pos-angle-implies`  []  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto)))

---

Home Index