Step
*
1
1
1
2
1
1
2
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. (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. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
22. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
23. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
24. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
⊢ 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)
∧ ((d(a;p) < d(a;b))
⇒ (q-p-p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
∧ ((d(a;b) < d(a;q)) ⇒ q-p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp-p)))
∧ ((d(a;p) = d(a;b))
⇒ ((p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp ≠ p + quadratic2(d(qq;pp)^2;r(2)
* pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
⇒ ((req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (r0 < pp⋅q - p))
∨ (req-vec(n;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (pp⋅q - p < r0))))
∧ (req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2
- d(a;b)^2)*qq - pp;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp)
⇒ ((pp⋅q - p = r0) ∧ req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p)))))
BY
{ 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. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
22. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
23. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
24. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
⊢ 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)
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. ||pp|| ≤ d(a;b)
14. (d(a;b) < d(a;q)) ⇒ (d(a;b) < ||qq||)
15. d(a;b) ≤ ||qq||
16. pp ≠ qq
17. r0 < ||qq - pp||
18. r0 < ||qq - pp||^2
19. r0 ≤ (((r(2) * pp⋅qq - pp) * r(2) * pp⋅qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - d(a;b)^2))
20. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
21. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
22. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
23. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
24. 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)
25. d(a;p) < d(a;b)
26. ||pp|| < d(a;b)
⊢ q-p-p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
3
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)
⊢ q-p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp-p
4
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. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
22. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
23. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
24. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
25. 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)
26. (d(a;p) < d(a;b))
⇒ (q-p-p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
∧ ((d(a;b) < d(a;q)) ⇒ q-p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp-p))
27. d(a;p) = d(a;b)
28. p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp ≠ p + quadratic2(d(qq;pp)^2;r(2)
* pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
⊢ (req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (r0 < pp⋅q - p))
∨ (req-vec(n;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (pp⋅q - p < r0))
5
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. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
22. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
23. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
24. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
25. 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)
26. (d(a;p) < d(a;b))
⇒ (q-p-p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
∧ ((d(a;b) < d(a;q)) ⇒ q-p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp-p))
27. d(a;p) = d(a;b)
28. p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp ≠ p + quadratic2(d(qq;pp)^2;r(2)
* pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
⇒ ((req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (r0 < pp⋅q - p))
∨ (req-vec(n;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (pp⋅q - p < r0)))
29. req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p + quadratic2(d(qq;pp)^2;r(2)
* pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp)
⊢ pp⋅q - p = r0
6
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. d(a;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
22. d(a;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp) = d(a;b)
23. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
24. ∀X:ℝ^n. req-vec(n;pp + X;p + X - a)
25. 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)
26. (d(a;p) < d(a;b))
⇒ (q-p-p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
∧ ((d(a;b) < d(a;q)) ⇒ q-p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp-p))
27. d(a;p) = d(a;b)
28. p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp ≠ p + quadratic2(d(qq;pp)^2;r(2)
* pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp
⇒ ((req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (r0 < pp⋅q - p))
∨ (req-vec(n;p + quadratic2(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p) ∧ (pp⋅q - p < r0)))
29. req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p + quadratic2(d(qq;pp)^2;r(2)
* pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp)
30. pp⋅q - p = r0
⊢ req-vec(n;p + quadratic1(d(qq;pp)^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2)*qq - pp;p)
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. (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. 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)
22. 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)
23. quadratic1(||qq - pp||\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2) \mmember{} [r0, r1]
24. \mforall{}X:\mBbbR{}\^{}n. req-vec(n;pp + X;p + X - a)
\mvdash{} 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)
\mwedge{} ((d(a;p) < d(a;b))
{}\mRightarrow{} (q-p-p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp
\mwedge{} ((d(a;b) < d(a;q))
{}\mRightarrow{} q-p + quadratic1(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp-p)))
\mwedge{} ((d(a;p) = d(a;b))
{}\mRightarrow{} ((p + quadratic1(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2
- d(a;b)\^{}2)*qq - pp \mneq{} p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp
{}\mRightarrow{} ((req-vec(n;p + quadratic1(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp;p)
\mwedge{} (r0 < pp\mcdot{}q - p))
\mvee{} (req-vec(n;p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp;p)
\mwedge{} (pp\mcdot{}q - p < r0))))
\mwedge{} (req-vec(n;p + quadratic1(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2
- d(a;b)\^{}2)*qq - pp;p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp)
{}\mRightarrow{} ((pp\mcdot{}q - p = r0)
\mwedge{} req-vec(n;p + quadratic1(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2
- d(a;b)\^{}2)*qq - pp;p)))))
By
Latex:
Auto
Home
Index