---

Step * of Lemma rv-line-circle-2

∀n:ℕ. ∀a,b:ℝ^n. ∀p:{p:ℝ^n| ab ≥ ap} . ∀q:{q:ℝ^n| aq ≥ ab} .
  (a ≠ b ⇒ p ≠ q ⇒ (∃u:{u:ℝ^n| ab=au ∧ q_u_p} . (∃v:{ℝ^n| (ab=av ∧ q_p_v)})))
BY
{ (Unfolds ``rv-ge rv-be`` 0
   THEN InstLemma `rv-line-circle-1` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN InstHyp [⌜p⌝;⌜q⌝] 4⋅
   THEN Auto
   THEN DSetVars
   THEN (Unhide THENA Auto)
   THEN (BLemma `not-rless` THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. ∀p,q:ℝ^n.
     (a ≠ b
     ⇒ p ≠ q
     ⇒ (d(a;p) ≤ d(a;b))
     ⇒ (d(a;b) ≤ d(a;q))
     ⇒ (∃u:{u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
          ∃v:{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)))))
5. p : ℝ^n
6. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ap=uv ∧ ab=uw))
7. q : ℝ^n
8. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ aq=uw))
9. a ≠ b
10. p ≠ q
⊢ ¬(d(a;b) < d(a;p))

2
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. ∀p,q:ℝ^n.
     (a ≠ b
     ⇒ p ≠ q
     ⇒ (d(a;p) ≤ d(a;b))
     ⇒ (d(a;b) ≤ d(a;q))
     ⇒ (∃u:{u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))} 
          ∃v:{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)))))
5. p : ℝ^n
6. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ap=uv ∧ ab=uw))
7. q : ℝ^n
8. ¬¬(∃u,v,w:ℝ^n. ((¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))) ∧ ab=uv ∧ aq=uw))
9. a ≠ b
10. p ≠ q
⊢ ¬(d(a;q) < d(a;b))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbR{}\^{}n.  \mforall{}p:\{p:\mBbbR{}\^{}n|  ab  \mgeq{}  ap\}  .  \mforall{}q:\{q:\mBbbR{}\^{}n|  aq  \mgeq{}  ab\}  .
    (a  \mneq{}  b  {}\mRightarrow{}  p  \mneq{}  q  {}\mRightarrow{}  (\mexists{}u:\{u:\mBbbR{}\^{}n|  ab=au  \mwedge{}  q\_u\_p\}  .  (\mexists{}v:\{\mBbbR{}\^{}n|  (ab=av  \mwedge{}  q\_p\_v)\})))


By

---

Latex:
(Unfolds  ``rv-ge  rv-be``  0
  THEN  InstLemma  `rv-line-circle-1`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]  4\mcdot{}
  THEN  Auto
  THEN  DSetVars
  THEN  (Unhide  THENA  Auto)
  THEN  (BLemma  `not-rless`  THENA  Auto))

---

Home Index