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

.....assertion..... 
1. rv InnerProductSpace
2. Point(rv)
3. Point(rv)
4. Point(rv)
5. Point(rv)
6. b
7. q
8. pp Point(rv)
9. pp ∈ Point(rv)
10. qq Point(rv)
11. 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. : ℝ
19. quadratic1(||qq pp||^2;r(2) pp ⋅ qq pp;||pp||^2 ||a b||^2) t ∈ ℝ
20. : ℝ
21. quadratic2(||qq pp||^2;r(2) pp ⋅ qq pp;||pp||^2 ||a b||^2) s ∈ ℝ
22. ∀X:Point(rv). pp X ≡ a
23. ||p t*q a|| ||a b||
24. ||p s*q a|| ||a b||
25. t ∈ [r0, r1]
26. s ≤ r0
27. qq pp ≡ p
28. ||a p|| < ||a b||
29. s*q p
30. ||a b|| < ||a q||
31. s < r0
32. : ℝ
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<THENA Auto) THEN (RWW "rv-norm-squared rv-ip-sub-squared rv-ip-sub2" THENA Auto)) }

1
1. rv InnerProductSpace
2. Point(rv)
3. Point(rv)
4. Point(rv)
5. Point(rv)
6. b
7. q
8. pp Point(rv)
9. pp ∈ Point(rv)
10. qq Point(rv)
11. 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. : ℝ
19. quadratic1(||qq pp||^2;r(2) pp ⋅ qq pp;||pp||^2 ||a b||^2) t ∈ ℝ
20. : ℝ
21. quadratic2(||qq pp||^2;r(2) pp ⋅ qq pp;||pp||^2 ||a b||^2) s ∈ ℝ
22. ∀X:Point(rv). pp X ≡ a
23. ||p t*q a|| ||a b||
24. ||p s*q a|| ||a b||
25. t ∈ [r0, r1]
26. s ≤ r0
27. qq pp ≡ p
28. ||a p|| < ||a b||
29. s*q p
30. ||a b|| < ||a q||
31. s < r0
32. : ℝ
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