Proof of Nuprl Lemma : rv-line-circle-0

Step * 1 1 1 2 1 1 2 1 2 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) < 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
BY
{ ((Assert req-vec(n;qq - pp;q - p) BY
          ((Assert q - a = qq ∈ ℝ^n BY
                  Hypothesis)
           THEN (Assert p - a = pp ∈ ℝ^n BY
                       Auto)
           THEN (RWO  "-1< -2<" 0 THENA Auto)
           THEN (RepUR ``req-vec real-vec-mul real-vec-sub real-vec-add`` 0 THEN Auto)
           THEN nRNorm 0
           THEN Auto))
   THEN (Assert ∀t:ℝ. ((t < r0) ⇒ ((-(t)/r1 - t) ∈ (r0, r1))) BY
               (RepeatFor 2 ((D 0 THENA Auto))
                THEN (Assert r0 < (r1 - t) BY

                            (nRAdd ⌜t⌝ 0⋅ THEN Auto THEN RWO "-1" 0 THEN Auto))

                THEN Reduce 0
                THEN Auto
                THEN nRMul ⌜r1 - t⌝ 0⋅
                THEN nRAdd ⌜t⌝ 0⋅
                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. ||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))

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) < d(a;q)) {}\mRightarrow{} (d(a;b) < ||qq||) 15. d(a;b) \mleq{} ||qq|| 16. pp \mneq{} qq 17. r0 < ||qq - pp|| 18. r0 < ||qq - pp||\^{}2 19. 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)) 20. 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) 21. 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) 22. quadratic1(||qq - pp||\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2) \mmember{} [r0, r1] 23. \mforall{}X:\mBbbR{}\^{}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\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp) 25. d(a;p) < d(a;b) 26. ||pp|| < d(a;b) \mvdash{} q-p-p + quadratic2(d(qq;pp)\^{}2;r(2) * pp\mcdot{}qq - pp;||pp||\^{}2 - d(a;b)\^{}2)*qq - pp By Latex: ((Assert req-vec(n;qq - pp;q - p) BY ((Assert q - a = qq BY Hypothesis) THEN (Assert p - a = pp BY Auto) THEN (RWO "-1< -2<" 0 THENA Auto) THEN (RepUR ``req-vec real-vec-mul real-vec-sub real-vec-add`` 0 THEN Auto) THEN nRNorm 0 THEN Auto)) THEN (Assert \mforall{}t:\mBbbR{}. ((t < r0) {}\mRightarrow{} ((-(t)/r1 - t) \mmember{} (r0, r1))) BY (RepeatFor 2 ((D 0 THENA Auto)) THEN (Assert r0 < (r1 - t) BY (nRAdd \mkleeneopen{}t\mkleeneclose{} 0\mcdot{} THEN Auto THEN RWO "-1" 0 THEN Auto)) THEN Reduce 0 THEN Auto THEN nRMul \mkleeneopen{}r1 - t\mkleeneclose{} 0\mcdot{} THEN nRAdd \mkleeneopen{}t\mkleeneclose{} 0\mcdot{} THEN Auto)) ) Home Index