---

Step * 2 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)| 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)
BY
{ (All (RepUR ``ip-congruent``)
   THEN (Assert ∀x,y,z:Point(rv).  (||x - y|| = ||x - z|| ⇐⇒ ||z - x|| = ||x - y||) BY
               Auto)
   THEN (Assert u + a ∈ {p:Point(rv)| (||a - b|| = ||a - p||) ∧ (||c - d|| = ||c - p||)}  BY
               (MemTypeCD
                THEN (((RWO "-1" 0 THENA Auto)
                       THEN (RWO "-5< -6<" 0 THENA Auto)
                       THEN D 0
                       THEN (BLemma `rv-norm_functionality` THENA Auto)
                       THEN RealVecEqual
                       THEN Auto)
                     ORELSE Auto
                     )
                ))
   THEN (Assert v + a ∈ {p:Point(rv)| (||a - b|| = ||a - p||) ∧ (||c - d|| = ||c - p||)}  BY
               (MemTypeCD
                THEN (((RWO "-2" 0 THENA Auto)
                       THEN (RWO "-5< -4<" 0 THENA Auto)
                       THEN D 0
                       THEN (BLemma `rv-norm_functionality` THENA Auto)
                       THEN RealVecEqual
                       THEN Auto)
                     ORELSE Auto
                     )
                ))
   THEN (InstConcl [⌜u + a⌝;⌜v + a⌝]⋅ THENA Auto)) }

1
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

---

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)|  ab=ap  \mwedge{}  (||c  -  p||  \mleq{}  ||c  -  d||)\} 
7.  [q]  :  \{q:Point(rv)|  cd=cq  \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
\mvdash{}  \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:
(All  (RepUR  ``ip-congruent``)
  THEN  (Assert  \mforall{}x,y,z:Point(rv).    (||x  -  y||  =  ||x  -  z||  \mLeftarrow{}{}\mRightarrow{}  ||z  -  x||  =  ||x  -  y||)  BY
                          Auto)
  THEN  (Assert  u  +  a  \mmember{}  \{p:Point(rv)|  (||a  -  b||  =  ||a  -  p||)  \mwedge{}  (||c  -  d||  =  ||c  -  p||)\}    BY
                          (MemTypeCD
                            THEN  (((RWO  "-1"  0  THENA  Auto)
                                          THEN  (RWO  "-5<  -6<"  0  THENA  Auto)
                                          THEN  D  0
                                          THEN  (BLemma  `rv-norm\_functionality`  THENA  Auto)
                                          THEN  RealVecEqual
                                          THEN  Auto)
                                      ORELSE  Auto
                                      )
                            ))
  THEN  (Assert  v  +  a  \mmember{}  \{p:Point(rv)|  (||a  -  b||  =  ||a  -  p||)  \mwedge{}  (||c  -  d||  =  ||c  -  p||)\}    BY
                          (MemTypeCD
                            THEN  (((RWO  "-2"  0  THENA  Auto)
                                          THEN  (RWO  "-5<  -4<"  0  THENA  Auto)
                                          THEN  D  0
                                          THEN  (BLemma  `rv-norm\_functionality`  THENA  Auto)
                                          THEN  RealVecEqual
                                          THEN  Auto)
                                      ORELSE  Auto
                                      )
                            ))
  THEN  (InstConcl  [\mkleeneopen{}u  +  a\mkleeneclose{};\mkleeneopen{}v  +  a\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index