---

Step * 1 1 of Lemma ip-line-circle


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. [%4] : a # b
5. p : Point(rv)
6. [%3] : ab ≥ ap
7. q : Point(rv)
8. [%2] : p # q ∧ aq ≥ ab
9. ||p - a|| = ||a - p||
⊢ SqStable(ab ≥ ap)
BY
{ (Unfold `ip-ge` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  [\%4]  :  a  \#  b
5.  p  :  Point(rv)
6.  [\%3]  :  ab  \mgeq{}  ap
7.  q  :  Point(rv)
8.  [\%2]  :  p  \#  q  \mwedge{}  aq  \mgeq{}  ab
9.  ||p  -  a||  =  ||a  -  p||
\mvdash{}  SqStable(ab  \mgeq{}  ap)


By

---

Latex:
(Unfold  `ip-ge`  0  THEN  Auto)

---

Home Index