---

Step * 2 1 of Lemma ip-circle-circle-lemma3


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : {c:Point(rv)| a # c} 
5. d : Point(rv)
6. [p] : {p:Point(rv)| (||a - b|| = ||a - p||) ∧ (||c - p|| ≤ ||c - d||)} 
7. [q] : {q:Point(rv)| (||c - d|| = ||c - q||) ∧ (||a - q|| ≤ ||a - b||)} 
8. r0 < ||c - a||
9. u : Point(rv)
10. v : Point(rv)
11. ||u|| = ||a - b||
12. ||u - c - a|| = ||c - d||
13. ||v|| = ||a - b||
14. ||v - c - a|| = ||c - d||
15. ((||a - b||^2 - ||c - d||^2) + ||c - a||^2^2 < (r(4) * ||c - a||^2 * ||a - b||^2)) ⇒ u # v
16. ∀x,y,z:Point(rv).  (||x - y|| = ||x - z|| ⇐⇒ ||z - x|| = ||x - y||)
17. u + a ∈ {p:Point(rv)| (||a - b|| = ||a - p||) ∧ (||c - d|| = ||c - p||)} 
18. v + a ∈ {p:Point(rv)| (||a - b|| = ||a - p||) ∧ (||c - d|| = ||c - p||)} 
⊢ ((||a - q|| < ||a - b||) ∧ (||c - p|| < ||c - d||)) ⇒ u + a # v + a
BY
{ (RepeatFor 2 (Thin (-1))
   THEN (ParallelOp -2 THENM EAuto 1)
   THEN (Unhide THENA Auto)
   THEN DSetVars
   THEN (Unhide THENA Auto)
   THEN ExRepD
   THEN ∀h:hyp. (FLemma `ip-dist-between` [h] THENA Auto) ) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
5. a # c
6. d : Point(rv)
7. p : Point(rv)
8. ||a - b|| = ||a - p||
9. ||c - p|| ≤ ||c - d||
10. q : Point(rv)
11. ||c - d|| = ||c - q||
12. ||a - q|| ≤ ||a - b||
13. r0 < ||c - a||
14. u : Point(rv)
15. v : Point(rv)
16. ||u|| = ||a - b||
17. ||u - c - a|| = ||c - d||
18. ||v|| = ||a - b||
19. ||v - c - a|| = ||c - d||
20. ∀x,y,z:Point(rv).  (||x - y|| = ||x - z|| ⇐⇒ ||z - x|| = ||x - y||)
21. ||a - q|| < ||a - b||
22. ||c - p|| < ||c - d||
⊢ (||a - b||^2 - ||c - d||^2) + ||c - a||^2^2 < (r(4) * ||c - a||^2 * ||a - b||^2)

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  c  :  \{c:Point(rv)|  a  \#  c\} 
5.  d  :  Point(rv)
6.  [p]  :  \{p:Point(rv)|  (||a  -  b||  =  ||a  -  p||)  \mwedge{}  (||c  -  p||  \mleq{}  ||c  -  d||)\} 
7.  [q]  :  \{q:Point(rv)|  (||c  -  d||  =  ||c  -  q||)  \mwedge{}  (||a  -  q||  \mleq{}  ||a  -  b||)\} 
8.  r0  <  ||c  -  a||
9.  u  :  Point(rv)
10.  v  :  Point(rv)
11.  ||u||  =  ||a  -  b||
12.  ||u  -  c  -  a||  =  ||c  -  d||
13.  ||v||  =  ||a  -  b||
14.  ||v  -  c  -  a||  =  ||c  -  d||
15.  ((||a  -  b||\^{}2  -  ||c  -  d||\^{}2)  +  ||c  -  a||\^{}2\^{}2  <  (r(4)  *  ||c  -  a||\^{}2  *  ||a  -  b||\^{}2))  {}\mRightarrow{}  u  \#  v
16.  \mforall{}x,y,z:Point(rv).    (||x  -  y||  =  ||x  -  z||  \mLeftarrow{}{}\mRightarrow{}  ||z  -  x||  =  ||x  -  y||)
17.  u  +  a  \mmember{}  \{p:Point(rv)|  (||a  -  b||  =  ||a  -  p||)  \mwedge{}  (||c  -  d||  =  ||c  -  p||)\} 
18.  v  +  a  \mmember{}  \{p:Point(rv)|  (||a  -  b||  =  ||a  -  p||)  \mwedge{}  (||c  -  d||  =  ||c  -  p||)\} 
\mvdash{}  ((||a  -  q||  <  ||a  -  b||)  \mwedge{}  (||c  -  p||  <  ||c  -  d||))  {}\mRightarrow{}  u  +  a  \#  v  +  a


By

---

Latex:
(RepeatFor  2  (Thin  (-1))
  THEN  (ParallelOp  -2  THENM  EAuto  1)
  THEN  (Unhide  THENA  Auto)
  THEN  DSetVars
  THEN  (Unhide  THENA  Auto)
  THEN  ExRepD
  THEN  \mforall{}h:hyp.  (FLemma  `ip-dist-between`  [h]  THENA  Auto)  )

---

Home Index