Step
*
2
1
1
2
of Lemma
ip-line-circle-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. 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)
BY
{ Assert ⌜r0 ≤ ((r(2) * pp ⋅ v2) + ||v2||^2)⌝⋅ }
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||
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))
⊢ r0 ≤ ((r(2) * pp ⋅ v2) + ||v2||^2)
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))
30. r0 ≤ ((r(2) * pp ⋅ v2) + ||v2||^2)
⊢ v ≤ ((r(2) * pp ⋅ v2) + v1)
Latex:
Latex:
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||
20. v : \mBbbR{}
21. r0 \mleq{} v
22. rsqrt(((r(2) * pp \mcdot{} qq - pp) * r(2) * pp \mcdot{} qq - pp) - r(4)
* ||qq - pp||\^{}2
* (||pp||\^{}2 - ||a - b||\^{}2))
= v
23. v1 : \mBbbR{}
24. (r(2) * ||qq - pp||\^{}2) = v1
25. r0 < v1
26. r0 \mleq{} (-(r(2) * pp \mcdot{} qq - pp) + v/v1)
27. v2 : Point(rv)
28. qq - pp = v2
29. (v * v) = (((r(2) * pp \mcdot{} v2) * r(2) * pp \mcdot{} v2) - r(4) * ||v2||\^{}2 * (||pp||\^{}2 - ||a - b||\^{}2))
\mvdash{} v \mleq{} ((r(2) * pp \mcdot{} v2) + v1)
By
Latex:
Assert \mkleeneopen{}r0 \mleq{} ((r(2) * pp \mcdot{} v2) + ||v2||\^{}2)\mkleeneclose{}\mcdot{}
Home
Index