---

Step * 2 1 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. u : {u:ℝ^n| ab=au} 
10. ¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p))
11. v : {v:ℝ^n| ab=av} 
12. real-vec-be(n;q;p;v)
13. (d(a;p) < d(a;b)) ⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) ⇒ q-u-p))
14. (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))))
⊢ ∃v:ℝ^n [(ab=av
         ∧ (¬(q ≠ p ∧ p ≠ v ∧ (¬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 < 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))))))]
BY
{ ((RWO "rv-non-strict-between-iff<" (-3) THENA EAuto 1) THENM (D 0 With ⌜v⌝  THEN Auto)) }

1
.....rewrite subgoal..... 
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. u : {u:ℝ^n| ab=au} 
10. ¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p))
11. v : {v:ℝ^n| ab=av} 
12. real-vec-be(n;q;p;v)
13. (d(a;p) < d(a;b)) ⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) ⇒ q-u-p))
14. (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))))
⊢ q ≠ 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. u : {u:ℝ^n| ab=au} 
10. ¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p))
11. v : {v:ℝ^n| ab=av} 
12. ¬(q ≠ p ∧ p ≠ v ∧ (¬q-p-v))
13. (d(a;p) < d(a;b)) ⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) ⇒ q-u-p))
14. (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))))
⊢ ab=av

---

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.  u  :  \{u:\mBbbR{}\^{}n|  ab=au\} 
10.  \mneg{}(q  \mneq{}  u  \mwedge{}  u  \mneq{}  p  \mwedge{}  (\mneg{}q-u-p))
11.  v  :  \{v:\mBbbR{}\^{}n|  ab=av\} 
12.  real-vec-be(n;q;p;v)
13.  (d(a;p)  <  d(a;b))  {}\mRightarrow{}  (q-p-v  \mwedge{}  ((d(a;b)  <  d(a;q))  {}\mRightarrow{}  q-u-p))
14.  (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))))
\mvdash{}  \mexists{}v:\mBbbR{}\^{}n  [(ab=av
                  \mwedge{}  (\mneg{}(q  \mneq{}  p  \mwedge{}  p  \mneq{}  v  \mwedge{}  (\mneg{}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  <  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))))))]


By

---

Latex:
((RWO  "rv-non-strict-between-iff<"  (-3)  THENA  EAuto  1)  THENM  (D  0  With  \mkleeneopen{}v\mkleeneclose{}    THEN  Auto))

---

Home Index