---

Step * of Lemma not-ip-triangle

No Annotations
∀rv:InnerProductSpace. ∀a,b,c:Point(rv).  (a # b ⇒ c # b ⇒ (¬Δ(a;b;c)) ⇒ (∃t:ℝ. ((r0 < |t|) ∧ c ≡ b + t*a - b)))
BY
{ (Auto THEN Unfold `ip-triangle` -1 THEN (FLemma `not-rless` [-1] THENA Auto) THEN Thin (-2)) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. a # b
6. c # b
7. (||a - b|| * ||c - b||) ≤ |a - b ⋅ c - b|
⊢ ∃t:ℝ. ((r0 < |t|) ∧ c ≡ b + t*a - b)

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point(rv).
    (a  \#  b  {}\mRightarrow{}  c  \#  b  {}\mRightarrow{}  (\mneg{}\mDelta{}(a;b;c))  {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  ((r0  <  |t|)  \mwedge{}  c  \mequiv{}  b  +  t*a  -  b)))


By

---

Latex:
(Auto  THEN  Unfold  `ip-triangle`  -1  THEN  (FLemma  `not-rless`  [-1]  THENA  Auto)  THEN  Thin  (-2))

---

Home Index