---

Step * of Lemma ip-circle-circle-lemma3

No Annotations
∀rv:InnerProductSpace. ∀a,b:Point(rv). ∀c:{c:Point(rv)| a # c} . ∀d:Point(rv).
  ∀[p:{p:Point(rv)| ab=ap ∧ (||c - p|| ≤ ||c - d||)} ]. ∀[q:{q:Point(rv)| cd=cq ∧ (||a - q|| ≤ ||a - b||)} ].
    ∃u,v:{p:Point(rv)| ab=ap ∧ cd=cp} . (((||a - q|| < ||a - b||) ∧ (||c - p|| < ||c - d||)) ⇒ u # v)
BY
{ ((Auto THEN (Assert r0 < ||c - a|| BY EAuto 2))
   THEN ((InstLemma `ip-circle-circle-lemma2` [⌜rv⌝;⌜||a - b||⌝;⌜||c - d||⌝;⌜c - a⌝]⋅ THENM ExRepD) THENA Auto)
   ) }

1
.....antecedent..... 
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)| ab=ap ∧ (||c - p|| ≤ ||c - d||)} 
7. [q] : {q:Point(rv)| cd=cq ∧ (||a - q|| ≤ ||a - b||)} 
8. r0 < ||c - a||
⊢ (||a - b||^2 - ||c - d||^2) + ||c - a||^2^2 ≤ (r(4) * ||c - a||^2 * ||a - b||^2)

2
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)| ab=ap ∧ (||c - p|| ≤ ||c - d||)} 
7. [q] : {q:Point(rv)| cd=cq ∧ (||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
⊢ ∃u,v:{p:Point(rv)| ab=ap ∧ cd=cp} . (((||a - q|| < ||a - b||) ∧ (||c - p|| < ||c - d||)) ⇒ u # v)

---

Latex:

---

Latex:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a,b:Point(rv).  \mforall{}c:\{c:Point(rv)|  a  \#  c\}  .  \mforall{}d:Point(rv).
    \mforall{}[p:\{p:Point(rv)|  ab=ap  \mwedge{}  (||c  -  p||  \mleq{}  ||c  -  d||)\}  ].  \mforall{}[q:\{q:Point(rv)| 
                                                                                                                        cd=cq  \mwedge{}  (||a  -  q||  \mleq{}  ||a  -  b||)\}  ].
        \mexists{}u,v:\{p:Point(rv)|  ab=ap  \mwedge{}  cd=cp\} 
          (((||a  -  q||  <  ||a  -  b||)  \mwedge{}  (||c  -  p||  <  ||c  -  d||))  {}\mRightarrow{}  u  \#  v)


By

---

Latex:
((Auto  THEN  (Assert  r0  <  ||c  -  a||  BY  EAuto  2))
  THEN  ((InstLemma  `ip-circle-circle-lemma2`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}||a  -  b||\mkleeneclose{};\mkleeneopen{}||c  -  d||\mkleeneclose{};\mkleeneopen{}c  -  a\mkleeneclose{}]\mcdot{}  THENM  ExRepD)
              THENA  Auto
              )
  )

---

Home Index