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


1. rv InnerProductSpace
2. Point(rv)
3. Point(rv)
4. Point(rv)
5. c
6. Point(rv)
7. Point(rv)
8. ||a b|| ||a p||
9. ||c p|| ≤ ||c d||
10. Point(rv)
11. ||c d|| ||c q||
12. ||a q|| ≤ ||a b||
13. r0 < ||c a||
14. Point(rv)
15. Point(rv)
16. ||u|| ||a b||
17. ||u a|| ||c d||
18. ||v|| ||a b||
19. ||v 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||
23. r0 < (||a b|| ||c a||^2 -(||c d||^2))
24. r0 < (-(||a b|| -(||c a||)^2) ||c d||^2)
⊢ (||a b||^2 ||c d||^2) ||c a||^2^2 < (r(4) ||c a||^2 ||a b||^2)
BY
(RepeatFor (MoveToConcl (-1))
   THEN (GenConcl ⌜||a b|| r1 ∈ ℝ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜||c d|| r2 ∈ ℝ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜||c a|| dd ∈ ℝ⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. r1 : ℝ
2. r2 : ℝ
3. dd : ℝ
4. r0 < (r1 dd^2 -(r2^2))
5. r0 < (-(r1 -(dd)^2) r2^2)
⊢ (r1^2 r2^2) dd^2^2 < (r(4) dd^2 r1^2)


Latex:


Latex:

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||  \mleq{}  ||c  -  d||
10.  q  :  Point(rv)
11.  ||c  -  d||  =  ||c  -  q||
12.  ||a  -  q||  \mleq{}  ||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.  \mforall{}x,y,z:Point(rv).    (||x  -  y||  =  ||x  -  z||  \mLeftarrow{}{}\mRightarrow{}  ||z  -  x||  =  ||x  -  y||)
21.  ||a  -  q||  <  ||a  -  b||
22.  ||c  -  p||  <  ||c  -  d||
23.  r0  <  (||a  -  b||  +  ||c  -  a||\^{}2  +  -(||c  -  d||\^{}2))
24.  r0  <  (-(||a  -  b||  +  -(||c  -  a||)\^{}2)  +  ||c  -  d||\^{}2)
\mvdash{}  (||a  -  b||\^{}2  -  ||c  -  d||\^{}2)  +  ||c  -  a||\^{}2\^{}2  <  (r(4)  *  ||c  -  a||\^{}2  *  ||a  -  b||\^{}2)


By


Latex:
(RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}||a  -  b||  =  r1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}||c  -  d||  =  r2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}||c  -  a||  =  dd\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)




Home Index