---

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

.....assertion..... 
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. pp : Point(rv)
9. p - a = pp ∈ Point(rv)
10. qq : Point(rv)
11. q - a = qq ∈ Point(rv)
12. ||pp|| ≤ ||a - b||
13. ||a - b|| ≤ ||qq||
14. pp # qq
15. r0 < ||qq - pp||
16. r0 < ||qq - pp||^2
17. r0 ≤ (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
18. ||pp + quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||a - b||
19. ||pp + quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||a - b||
⊢ quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) ∈ [r0, r1]
BY
{ ((DupHyp (-4) THEN nRMul ⌜r(2)⌝ (-1)⋅)
   THEN RepUR ``quadratic1`` 0
   THEN (GenConclTerm ⌜rsqrt(((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4)
                       * ||qq - pp||^2
                       * (||pp||^2 - ||a - b||^2))⌝⋅
         THENA Auto
         )
   THEN MoveToConcl (-3)
   THEN GenConclTerm ⌜r(2) * ||qq - pp||^2⌝⋅
   THEN Auto
   THEN nRMul ⌜v1⌝ 0⋅
   THEN nRAdd ⌜r(2) * pp ⋅ qq - pp⌝ 0⋅
   THEN DVar `v'
   THEN Unhide
   THEN Auto
   THEN MoveToConcl (22)
   THEN GenConclTerm ⌜qq - pp⌝⋅
   THEN Auto) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. pp : Point(rv)
9. p - a = pp ∈ Point(rv)
10. qq : Point(rv)
11. q - a = qq ∈ Point(rv)
12. ||pp|| ≤ ||a - b||
13. ||a - b|| ≤ ||qq||
14. pp # qq
15. r0 < ||qq - pp||
16. r0 < ||qq - pp||^2
17. r0 ≤ (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
18. ||pp + quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||a - b||
19. ||pp + quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||a - b||
20. v : ℝ
21. r0 ≤ v
22. rsqrt(((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
= v
∈ {r:ℝ| 
   (r0 ≤ r)
   ∧ ((r * r) = (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2)))} 
23. v1 : ℝ
24. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
25. r0 < v1
26. v2 : Point(rv)
27. qq - pp = v2 ∈ Point(rv)
28. (v * v) = (((r(2) * pp ⋅ v2) * r(2) * pp ⋅ v2) - r(4) * ||v2||^2 * (||pp||^2 - ||a - b||^2))
⊢ (r(2) * pp ⋅ v2) ≤ v

2
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. pp : Point(rv)
9. p - a = pp ∈ Point(rv)
10. qq : Point(rv)
11. q - a = qq ∈ Point(rv)
12. ||pp|| ≤ ||a - b||
13. ||a - b|| ≤ ||qq||
14. pp # qq
15. r0 < ||qq - pp||
16. r0 < ||qq - pp||^2
17. r0 ≤ (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
18. ||pp + quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||a - b||
19. ||pp + quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2)*qq - pp|| = ||a - b||
20. v : ℝ
21. r0 ≤ v
22. rsqrt(((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
= v
∈ {r:ℝ| 
   (r0 ≤ r)
   ∧ ((r * r) = (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2)))} 
23. v1 : ℝ
24. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
25. r0 < v1
26. r0 ≤ (-(r(2) * pp ⋅ qq - pp) + v/v1)
27. v2 : Point(rv)
28. qq - pp = v2 ∈ Point(rv)
29. (v * v) = (((r(2) * pp ⋅ v2) * r(2) * pp ⋅ v2) - r(4) * ||v2||^2 * (||pp||^2 - ||a - b||^2))
⊢ v ≤ ((r(2) * pp ⋅ v2) + v1)

---

Latex:

---

Latex:
.....assertion..... 
1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  p  :  Point(rv)
5.  q  :  Point(rv)
6.  a  \#  b
7.  p  \#  q
8.  pp  :  Point(rv)
9.  p  -  a  =  pp
10.  qq  :  Point(rv)
11.  q  -  a  =  qq
12.  ||pp||  \mleq{}  ||a  -  b||
13.  ||a  -  b||  \mleq{}  ||qq||
14.  pp  \#  qq
15.  r0  <  ||qq  -  pp||
16.  r0  <  ||qq  -  pp||\^{}2
17.  r0  \mleq{}  (((r(2)  *  pp  \mcdot{}  qq  -  pp)  *  r(2)  *  pp  \mcdot{}  qq  -  pp)  -  r(4)
*  ||qq  -  pp||\^{}2
*  (||pp||\^{}2  -  ||a  -  b||\^{}2))
18.  ||pp  +  quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)*qq  -  pp||
=  ||a  -  b||
19.  ||pp  +  quadratic2(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)*qq  -  pp||
=  ||a  -  b||
\mvdash{}  quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  \mmember{}  [r0,  r1]


By

---

Latex:
((DupHyp  (-4)  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{})
  THEN  RepUR  ``quadratic1``  0
  THEN  (GenConclTerm  \mkleeneopen{}rsqrt(((r(2)  *  pp  \mcdot{}  qq  -  pp)  *  r(2)  *  pp  \mcdot{}  qq  -  pp)  -  r(4)
                                          *  ||qq  -  pp||\^{}2
                                          *  (||pp||\^{}2  -  ||a  -  b||\^{}2))\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  MoveToConcl  (-3)
  THEN  GenConclTerm  \mkleeneopen{}r(2)  *  ||qq  -  pp||\^{}2\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  nRMul  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{}
  THEN  nRAdd  \mkleeneopen{}r(2)  *  pp  \mcdot{}  qq  -  pp\mkleeneclose{}  0\mcdot{}
  THEN  DVar  `v'
  THEN  Unhide
  THEN  Auto
  THEN  MoveToConcl  (22)
  THEN  GenConclTerm  \mkleeneopen{}qq  -  pp\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index