---

Step * 1 1 1 1 1 2 of Lemma rv-line-circle


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. p : ℝ^n
5. q : ℝ^n
6. p ≠ q
7. x : {x:ℝ^n| ap=ax ∧ (¬(a ≠ x ∧ x ≠ b ∧ (¬a-x-b)))} 
8. y : {y:ℝ^n| aq=ay ∧ (¬(a ≠ b ∧ b ≠ y ∧ (¬a-b-y)))} 
9. d(a;p) ≤ d(a;b)
10. d(a;b) ≤ d(a;q)
11. u : {u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
12. v : ℝ^n
13. ab=av
14. ¬(q ≠ p ∧ p ≠ v ∧ (¬q-p-v))
15. (d(a;p) = d(a;b))
⇒ ((u ≠ v ⇒ ((req-vec(n;u;p) ∧ (r0 < p - a⋅q - p)) ∨ (req-vec(n;v;p) ∧ (p - a⋅q - p < r0))))
   ∧ (req-vec(n;u;v) ⇒ ((p - a⋅q - p = r0) ∧ req-vec(n;u;p))))
16. a-x-b
17. q-p-v
18. (d(a;b) < d(a;q)) ⇒ q-u-p
19. q-p-v
20. a-b-y
⊢ d(a;b) < d(a;q)
BY
{ (D 8
   THEN (Unhide THENA Auto)
   THEN (RWO "rv-T-iff<" 9 THENA Auto)
   THEN D 9
   THEN UnfoldTopAb 9
   THEN (RW (AddrC [2] (HypC 9)) 0 THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. p : ℝ^n
5. q : ℝ^n
6. p ≠ q
7. x : {x:ℝ^n| ap=ax ∧ (¬(a ≠ x ∧ x ≠ b ∧ (¬a-x-b)))} 
8. y : ℝ^n
9. d(a;q) = d(a;y)
10. rv-T(n;a;b;y)
11. d(a;p) ≤ d(a;b)
12. d(a;b) ≤ d(a;q)
13. u : {u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
14. v : ℝ^n
15. ab=av
16. ¬(q ≠ p ∧ p ≠ v ∧ (¬q-p-v))
17. (d(a;p) = d(a;b))
⇒ ((u ≠ v ⇒ ((req-vec(n;u;p) ∧ (r0 < p - a⋅q - p)) ∨ (req-vec(n;v;p) ∧ (p - a⋅q - p < r0))))
   ∧ (req-vec(n;u;v) ⇒ ((p - a⋅q - p = r0) ∧ req-vec(n;u;p))))
18. a-x-b
19. q-p-v
20. (d(a;b) < d(a;q)) ⇒ q-u-p
21. q-p-v
22. a-b-y
⊢ d(a;b) < d(a;y)

---

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.  x  :  \{x:\mBbbR{}\^{}n|  ap=ax  \mwedge{}  (\mneg{}(a  \mneq{}  x  \mwedge{}  x  \mneq{}  b  \mwedge{}  (\mneg{}a-x-b)))\} 
8.  y  :  \{y:\mBbbR{}\^{}n|  aq=ay  \mwedge{}  (\mneg{}(a  \mneq{}  b  \mwedge{}  b  \mneq{}  y  \mwedge{}  (\mneg{}a-b-y)))\} 
9.  d(a;p)  \mleq{}  d(a;b)
10.  d(a;b)  \mleq{}  d(a;q)
11.  u  :  \{u:\mBbbR{}\^{}n|  ab=au  \mwedge{}  (\mneg{}(q  \mneq{}  u  \mwedge{}  u  \mneq{}  p  \mwedge{}  (\mneg{}q-u-p)))\} 
12.  v  :  \mBbbR{}\^{}n
13.  ab=av
14.  \mneg{}(q  \mneq{}  p  \mwedge{}  p  \mneq{}  v  \mwedge{}  (\mneg{}q-p-v))
15.  (d(a;p)  =  d(a;b))
{}\mRightarrow{}  ((u  \mneq{}  v  {}\mRightarrow{}  ((req-vec(n;u;p)  \mwedge{}  (r0  <  p  -  a\mcdot{}q  -  p))  \mvee{}  (req-vec(n;v;p)  \mwedge{}  (p  -  a\mcdot{}q  -  p  <  r0))))
      \mwedge{}  (req-vec(n;u;v)  {}\mRightarrow{}  ((p  -  a\mcdot{}q  -  p  =  r0)  \mwedge{}  req-vec(n;u;p))))
16.  a-x-b
17.  q-p-v
18.  (d(a;b)  <  d(a;q))  {}\mRightarrow{}  q-u-p
19.  q-p-v
20.  a-b-y
\mvdash{}  d(a;b)  <  d(a;q)


By

---

Latex:
(D  8
  THEN  (Unhide  THENA  Auto)
  THEN  (RWO  "rv-T-iff<"  9  THENA  Auto)
  THEN  D  9
  THEN  UnfoldTopAb  9
  THEN  (RW  (AddrC  [2]  (HypC  9))  0  THENA  Auto))

---

Home Index