Step
*
1
1
1
2
1
1
2
1
3
1
1
2
2
2
1
1
1
1
1
of Lemma
rv-line-circle-0
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. p : ℝ^n
5. q : ℝ^n
6. p ≠ q
7. d(a;p) ≤ d(a;b)
8. d(a;b) ≤ d(a;q)
9. pp : ℝ^n
10. p - a = pp ∈ ℝ^n
11. qq : ℝ^n
12. q - a = qq ∈ ℝ^n
13. ||pp|| ≤ d(a;b)
14. d(a;b) ≤ ||qq||
15. pp ≠ qq
16. r0 < ||qq - pp||
17. r0 < ||qq - pp||^2
18. r0 ≤ (((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(a;b)^2))
19. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
20. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
21. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
22. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
23. real-vec-be(n;q;p;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp)
24. d(a;p) < d(a;b)
25. q-p-p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
26. d(a;b) < d(a;q)
27. d(a;b) < ||qq||
28. ||pp|| < d(a;b)
29. r0 < (r(2) * ||qq - pp||^2)
30. v : ℝ
31. r0 ≤ v
32. r0 < (-(r(2) * pp⋅qq - pp) + v/r(2) * ||qq - pp||^2)
33. v1 : ℝ
34. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
35. rsqrt(((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(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 - d(a;b)^2)))}
36. v2 : ℝ^n
37. qq - pp = v2 ∈ ℝ^n
38. v^2 = (r(2) * pp⋅v2^2 - r(4) * ||v2||^2 * (||pp||^2 - d(a;b)^2))
39. A : ℝ
40. (r(2) * pp⋅v2) = A ∈ ℝ
41. D : ℝ
42. ||v2||^2 = D ∈ ℝ
43. r0 < D
44. r0 ≤ (A + D)
45. v3 : ℝ
46. (||pp||^2 - d(a;b)^2) = v3 ∈ ℝ
47. v3 < r0
⊢ r0 < ((r(4) * A * D) + (r(4) * D * D) + (r(4) * D * v3))
BY
{ ((Assert d(a;b)^2 < ||qq||^2 BY (BLemma `rnexp-rless` THEN Auto)) THEN (nRAdd ⌜-(d(a;b)^2)⌝ (-1)⋅ THENA Auto)) }
1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. p : ℝ^n
5. q : ℝ^n
6. p ≠ q
7. d(a;p) ≤ d(a;b)
8. d(a;b) ≤ d(a;q)
9. pp : ℝ^n
10. p - a = pp ∈ ℝ^n
11. qq : ℝ^n
12. q - a = qq ∈ ℝ^n
13. ||pp|| ≤ d(a;b)
14. d(a;b) ≤ ||qq||
15. pp ≠ qq
16. r0 < ||qq - pp||
17. r0 < ||qq - pp||^2
18. r0 ≤ (((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(a;b)^2))
19. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
20. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
21. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
22. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
23. real-vec-be(n;q;p;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp)
24. d(a;p) < d(a;b)
25. q-p-p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
26. d(a;b) < d(a;q)
27. d(a;b) < ||qq||
28. ||pp|| < d(a;b)
29. r0 < (r(2) * ||qq - pp||^2)
30. v : ℝ
31. r0 ≤ v
32. r0 < (-(r(2) * pp⋅qq - pp) + v/r(2) * ||qq - pp||^2)
33. v1 : ℝ
34. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
35. rsqrt(((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(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 - d(a;b)^2)))}
36. v2 : ℝ^n
37. qq - pp = v2 ∈ ℝ^n
38. v^2 = (r(2) * pp⋅v2^2 - r(4) * ||v2||^2 * (||pp||^2 - d(a;b)^2))
39. A : ℝ
40. (r(2) * pp⋅v2) = A ∈ ℝ
41. D : ℝ
42. ||v2||^2 = D ∈ ℝ
43. r0 < D
44. r0 ≤ (A + D)
45. v3 : ℝ
46. (||pp||^2 - d(a;b)^2) = v3 ∈ ℝ
47. v3 < r0
48. r0 < (-(d(a;b)^2) + ||qq||^2)
⊢ r0 < ((r(4) * A * D) + (r(4) * D * D) + (r(4) * D * v3))
Latex:
Latex:
1. n : \mBbbN{}
2. a : \mBbbR{}\^{}n
3. b : \mBbbR{}\^{}n
4. p : \mBbbR{}\^{}n
5. q : \mBbbR{}\^{}n
6. p \mneq{} q
7. d(a;p) \mleq{} d(a;b)
8. d(a;b) \mleq{} d(a;q)
9. pp : \mBbbR{}\^{}n
10. p - a = pp
11. qq : \mBbbR{}\^{}n
12. q - a = qq
13. ||pp|| \mleq{} d(a;b)
14. d(a;b) \mleq{} ||qq||
15. pp \mneq{} qq
16. r0 < ||qq - pp||
17. r0 < ||qq - pp||\^{}2
18. r0 \mleq{} (((r(2) * pp\mcdot{}qq - pp) * r(2) * pp\mcdot{}qq - pp) - r(4) * ||qq - pp||\^{}2 * (||pp||\^{}2 - d(a;b)\^{}2))
19. d(a;p + quadratic1(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp) = d(a;b)
20. d(a;p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp) = d(a;b)
21. quadratic1(||qq - pp||\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2) \mmember{} [r0, r1]
22. \mforall{}X:\mBbbR{}\^{}n. req-vec(n;pp + X;p + X - a)
23. real-vec-be(n;q;p;p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp)
24. d(a;p) < d(a;b)
25. q-p-p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp
26. d(a;b) < d(a;q)
27. d(a;b) < ||qq||
28. ||pp|| < d(a;b)
29. r0 < (r(2) * ||qq - pp||\^{}2)
30. v : \mBbbR{}
31. r0 \mleq{} v
32. r0 < (-(r(2) * pp\mcdot{}qq - pp) + v/r(2) * ||qq - pp||\^{}2)
33. v1 : \mBbbR{}
34. (r(2) * ||qq - pp||\^{}2) = v1
35. rsqrt(((r(2) * pp\mcdot{}qq - pp) * r(2) * pp\mcdot{}qq - pp) - r(4) * ||qq - pp||\^{}2 * (||pp||\^{}2 - d(a;b)\^{}2))
= v
36. v2 : \mBbbR{}\^{}n
37. qq - pp = v2
38. v\^{}2 = (r(2) * pp\mcdot{}v2\^{}2 - r(4) * ||v2||\^{}2 * (||pp||\^{}2 - d(a;b)\^{}2))
39. A : \mBbbR{}
40. (r(2) * pp\mcdot{}v2) = A
41. D : \mBbbR{}
42. ||v2||\^{}2 = D
43. r0 < D
44. r0 \mleq{} (A + D)
45. v3 : \mBbbR{}
46. (||pp||\^{}2 - d(a;b)\^{}2) = v3
47. v3 < r0
\mvdash{} r0 < ((r(4) * A * D) + (r(4) * D * D) + (r(4) * D * v3))
By
Latex:
((Assert d(a;b)\^{}2 < ||qq||\^{}2 BY
(BLemma `rnexp-rless` THEN Auto))
THEN (nRAdd \mkleeneopen{}-(d(a;b)\^{}2)\mkleeneclose{} (-1)\mcdot{} THENA Auto)
)
Home
Index