---

Step * 2 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} 
⊢ ||a - b|| ≤ ||q - a||
BY
{ (((Assert ||q - a|| = ||a - q|| 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. ||q - a|| = ||a - q||
⊢ SqStable(aq ≥ ab)

---

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{}  ||a  -  b||  \mleq{}  ||q  -  a||


By

---

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

---

Home Index