Step
*
1
1
1
1
of Lemma
rv-line-circle-0
.....assertion.....
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. (d(a;p) < d(a;b)) ⇒ (||pp|| < d(a;b))
14. ||pp|| ≤ d(a;b)
15. (d(a;b) < d(a;q)) ⇒ (d(a;b) < ||qq||)
16. d(a;b) ≤ ||qq||
17. pp ≠ qq
18. r0 < ||qq - pp||
19. r0 < ||qq - pp||^2
20. r0 ≤ (((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(a;b)^2))
21. ||pp + quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
22. ||pp + quadratic2(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
⊢ quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
BY
{ ((DupHyp 19 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 - d(a;b)^2))⌝⋅
THEN Auto
THEN MoveToConcl 23
THEN GenConclTerm ⌜r(2) * ||qq - pp||^2⌝⋅
THEN Auto
THEN nRMul ⌜v1⌝ 0⋅
THEN nRAdd ⌜r(2) * pp⋅qq - pp⌝ 0⋅
THEN (RWW "-2<" 0 THENA Auto)
THEN DVar `v'
THEN Unhide
THEN Auto
THEN MoveToConcl (25)
THEN GenConclTerm ⌜qq - pp⌝⋅
THEN 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. (d(a;p) < d(a;b)) ⇒ (||pp|| < d(a;b))
14. ||pp|| ≤ d(a;b)
15. (d(a;b) < d(a;q)) ⇒ (d(a;b) < ||qq||)
16. d(a;b) ≤ ||qq||
17. pp ≠ qq
18. r0 < ||qq - pp||
19. r0 < ||qq - pp||^2
20. r0 ≤ (((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(a;b)^2))
21. ||pp + quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
22. ||pp + quadratic2(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
23. v : ℝ
24. r0 ≤ v
25. 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)))}
26. v1 : ℝ
27. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
28. r0 < v1
29. v2 : ℝ^n
30. qq - pp = v2 ∈ ℝ^n
31. (v * v) = (((r(2) * pp⋅v2) * r(2) * pp⋅v2) - r(4) * ||v2||^2 * (||pp||^2 - d(a;b)^2))
⊢ (r(2) * pp⋅v2) ≤ v
2
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. (d(a;p) < d(a;b)) ⇒ (||pp|| < d(a;b))
14. ||pp|| ≤ d(a;b)
15. (d(a;b) < d(a;q)) ⇒ (d(a;b) < ||qq||)
16. d(a;b) ≤ ||qq||
17. pp ≠ qq
18. r0 < ||qq - pp||
19. r0 < ||qq - pp||^2
20. r0 ≤ (((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(a;b)^2))
21. ||pp + quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
22. ||pp + quadratic2(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp|| = d(a;b)
23. v : ℝ
24. r0 ≤ v
25. 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)))}
26. r0 ≤ (-(r(2) * pp⋅qq - pp) + v/r(2) * ||qq - pp||^2)
27. v1 : ℝ
28. (r(2) * ||qq - pp||^2) = v1 ∈ ℝ
29. r0 < v1
30. v2 : ℝ^n
31. qq - pp = v2 ∈ ℝ^n
32. (v * v) = (((r(2) * pp⋅v2) * r(2) * pp⋅v2) - r(4) * ||v2||^2 * (||pp||^2 - d(a;b)^2))
⊢ v ≤ ((r(2) * pp⋅v2) + (r(2) * ||v2||^2))
Latex:
Latex:
.....assertion.....
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. (d(a;p) < d(a;b)) {}\mRightarrow{} (||pp|| < d(a;b))
14. ||pp|| \mleq{} d(a;b)
15. (d(a;b) < d(a;q)) {}\mRightarrow{} (d(a;b) < ||qq||)
16. d(a;b) \mleq{} ||qq||
17. pp \mneq{} qq
18. r0 < ||qq - pp||
19. r0 < ||qq - pp||\^{}2
20. 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))
21. ||pp + quadratic1(||qq - pp||\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp|| = d(a;b)
22. ||pp + quadratic2(||qq - pp||\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp|| = d(a;b)
\mvdash{} quadratic1(||qq - pp||\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2) \mmember{} [r0, r1]
By
Latex:
((DupHyp 19 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 - d(a;b)\^{}2))\mkleeneclose{}\mcdot{}
THEN Auto
THEN MoveToConcl 23
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 (RWW "-2<" 0 THENA Auto)
THEN DVar `v'
THEN Unhide
THEN Auto
THEN MoveToConcl (25)
THEN GenConclTerm \mkleeneopen{}qq - pp\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index