Step
*
1
1
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. (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. quadratic1(||qq - pp||^2;r(2) * pp⋅qq - pp;||pp||^2 - d(a;b)^2) ∈ [r0, r1]
⊢ ∃u:{u:ℝ^n| ab=au} 
   (real-vec-be(n;q;u;p)
   ∧ (∃v:{v:ℝ^n| ab=av} 
       (real-vec-be(n;q;p;v)
       ∧ ((d(a;p) < d(a;b)) 
⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) 
⇒ q-u-p)))
       ∧ ((d(a;p) = d(a;b))
         
⇒ ((u ≠ v 
⇒ ((req-vec(n;u;p) ∧ (r0 < pp⋅q - p)) ∨ (req-vec(n;v;p) ∧ (pp⋅q - p < r0))))
            ∧ (req-vec(n;u;v) 
⇒ ((pp⋅q - p = r0) ∧ req-vec(n;u;p))))))))
BY
{ (Assert ∀X:ℝ^n. req-vec(n;pp + X;p + X - a) BY
         (Auto
          THEN (Assert p - a = pp ∈ ℝ^n BY
                      Hypothesis)
          THEN (RWO "-1<" 0 THENA Auto)
          THEN RepUR ``req-vec real-vec-add real-vec-sub`` 0
          THEN Auto
          THEN nRNorm 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. (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. 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)
⊢ ∃u:{u:ℝ^n| ab=au} 
   (real-vec-be(n;q;u;p)
   ∧ (∃v:{v:ℝ^n| ab=av} 
       (real-vec-be(n;q;p;v)
       ∧ ((d(a;p) < d(a;b)) 
⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) 
⇒ q-u-p)))
       ∧ ((d(a;p) = d(a;b))
         
⇒ ((u ≠ v 
⇒ ((req-vec(n;u;p) ∧ (r0 < pp⋅q - p)) ∨ (req-vec(n;v;p) ∧ (pp⋅q - p < r0))))
            ∧ (req-vec(n;u;v) 
⇒ ((pp⋅q - p = r0) ∧ req-vec(n;u;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.  ||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)
23.  quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp\mcdot{}qq  -  pp;||pp||\^{}2  -  d(a;b)\^{}2)  \mmember{}  [r0,  r1]
\mvdash{}  \mexists{}u:\{u:\mBbbR{}\^{}n|  ab=au\} 
      (real-vec-be(n;q;u;p)
      \mwedge{}  (\mexists{}v:\{v:\mBbbR{}\^{}n|  ab=av\} 
              (real-vec-be(n;q;p;v)
              \mwedge{}  ((d(a;p)  <  d(a;b))  {}\mRightarrow{}  (q-p-v  \mwedge{}  ((d(a;b)  <  d(a;q))  {}\mRightarrow{}  q-u-p)))
              \mwedge{}  ((d(a;p)  =  d(a;b))
                  {}\mRightarrow{}  ((u  \mneq{}  v  {}\mRightarrow{}  ((req-vec(n;u;p)  \mwedge{}  (r0  <  pp\mcdot{}q  -  p))  \mvee{}  (req-vec(n;v;p)  \mwedge{}  (pp\mcdot{}q  -  p  <  r0))))
                        \mwedge{}  (req-vec(n;u;v)  {}\mRightarrow{}  ((pp\mcdot{}q  -  p  =  r0)  \mwedge{}  req-vec(n;u;p))))))))
By
Latex:
(Assert  \mforall{}X:\mBbbR{}\^{}n.  req-vec(n;pp  +  X;p  +  X  -  a)  BY
              (Auto
                THEN  (Assert  p  -  a  =  pp  BY
                                        Hypothesis)
                THEN  (RWO  "-1<"  0  THENA  Auto)
                THEN  RepUR  ``req-vec  real-vec-add  real-vec-sub``  0
                THEN  Auto
                THEN  nRNorm  0
                THEN  Auto))
Home
Index