Step
*
2
1
2
2
1
1
6
1
1
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. t : ℝ
19. quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = t ∈ ℝ
20. s : ℝ
21. quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = s ∈ ℝ
22. ∀X:Point(rv). pp + X ≡ p + X - a
23. ||p + t*q - p - a|| = ||a - b||
24. ||p + s*q - p - a|| = ||a - b||
25. t ∈ [r0, r1]
26. s ≤ r0
27. qq - pp ≡ q - p
28. ||a - p|| < ||a - b||
29. p # p + s*q - p
30. ||a - b|| < ||a - q||
31. s < r0
32. v : ℝ
33. r0 ≤ v
34. 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)))} 
35. v1 : ℝ
36. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
37. r0 < v1
38. v2 : Point(rv)
39. qq - pp = v2 ∈ Point(rv)
40. (v * v) = (((r(2) * pp ⋅ v2) * r(2) * pp ⋅ v2) - r(4) * ||v2||^2 * (||pp||^2 - ||a - b||^2))
⊢ r0 ≤ ((r(2) * pp ⋅ v2) + ||v2||^2)
BY
{ ((RWO "-2<" 0 THENA Auto) THEN (RWW "rv-norm-squared rv-ip-sub-squared rv-ip-sub2" 0 THENA 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. t : ℝ
19. quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = t ∈ ℝ
20. s : ℝ
21. quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = s ∈ ℝ
22. ∀X:Point(rv). pp + X ≡ p + X - a
23. ||p + t*q - p - a|| = ||a - b||
24. ||p + s*q - p - a|| = ||a - b||
25. t ∈ [r0, r1]
26. s ≤ r0
27. qq - pp ≡ q - p
28. ||a - p|| < ||a - b||
29. p # p + s*q - p
30. ||a - b|| < ||a - q||
31. s < r0
32. v : ℝ
33. r0 ≤ v
34. 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)))} 
35. v1 : ℝ
36. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
37. r0 < v1
38. v2 : Point(rv)
39. qq - pp = v2 ∈ Point(rv)
40. (v * v) = (((r(2) * pp ⋅ v2) * r(2) * pp ⋅ v2) - r(4) * ||v2||^2 * (||pp||^2 - ||a - b||^2))
⊢ r0 ≤ ((r(2) * (pp ⋅ qq - pp^2)) + (qq^2 - r(2) * qq ⋅ pp) + pp^2)
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.  t  :  \mBbbR{}
19.  quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  =  t
20.  s  :  \mBbbR{}
21.  quadratic2(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  =  s
22.  \mforall{}X:Point(rv).  pp  +  X  \mequiv{}  p  +  X  -  a
23.  ||p  +  t*q  -  p  -  a||  =  ||a  -  b||
24.  ||p  +  s*q  -  p  -  a||  =  ||a  -  b||
25.  t  \mmember{}  [r0,  r1]
26.  s  \mleq{}  r0
27.  qq  -  pp  \mequiv{}  q  -  p
28.  ||a  -  p||  <  ||a  -  b||
29.  p  \#  p  +  s*q  -  p
30.  ||a  -  b||  <  ||a  -  q||
31.  s  <  r0
32.  v  :  \mBbbR{}
33.  r0  \mleq{}  v
34.  rsqrt(((r(2)  *  pp  \mcdot{}  qq  -  pp)  *  r(2)  *  pp  \mcdot{}  qq  -  pp)  -  r(4)
*  ||qq  -  pp||\^{}2
*  (||pp||\^{}2  -  ||a  -  b||\^{}2))
=  v
35.  v1  :  \mBbbR{}
36.  (r(2)  *  ||qq  -  pp||\^{}2)  =  v1
37.  r0  <  v1
38.  v2  :  Point(rv)
39.  qq  -  pp  =  v2
40.  (v  *  v)  =  (((r(2)  *  pp  \mcdot{}  v2)  *  r(2)  *  pp  \mcdot{}  v2)  -  r(4)  *  ||v2||\^{}2  *  (||pp||\^{}2  -  ||a  -  b||\^{}2))
\mvdash{}  r0  \mleq{}  ((r(2)  *  pp  \mcdot{}  v2)  +  ||v2||\^{}2)
By
Latex:
((RWO  "-2<"  0  THENA  Auto)  THEN  (RWW  "rv-norm-squared  rv-ip-sub-squared  rv-ip-sub2"  0  THENA  Auto))
Home
Index