---

Step * 1 of Lemma ip-line-circle

.....antecedent..... 
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : {b:Point(rv)| a # b} 
4. p : {p:Point(rv)| ab ≥ ap} 
5. q : {q:Point(rv)| p # q ∧ aq ≥ ab} 
⊢ ||p - a|| ≤ ||a - b||
BY
{ ((Assert ||p - a|| = ||a - p|| BY
          Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (BLemma `ip-ge-iff` THEN Auto)
   THEN DSetVars
   THEN Unhide
   THEN Auto) }

1
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)

---

Latex:

---

Latex:
.....antecedent..... 
1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  \{b:Point(rv)|  a  \#  b\} 
4.  p  :  \{p:Point(rv)|  ab  \mgeq{}  ap\} 
5.  q  :  \{q:Point(rv)|  p  \#  q  \mwedge{}  aq  \mgeq{}  ab\} 
\mvdash{}  ||p  -  a||  \mleq{}  ||a  -  b||


By

---

Latex:
((Assert  ||p  -  a||  =  ||a  -  p||  BY
                Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (BLemma  `ip-ge-iff`  THEN  Auto)
  THEN  DSetVars
  THEN  Unhide
  THEN  Auto)

---

Home Index