---

Step * 2 of Lemma rv-ge-dist


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. p : ℝ^n
6. cp ≥ ab
⊢ d(a;b) ≤ d(c;p)
BY
{ ((BLemma `not-rless` THENA Auto) THEN (D 0 THENA Auto) THEN D -2 THEN (D 0 THENA Auto) THEN ExRepD) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. p : ℝ^n
6. d(c;p) < d(a;b)
7. u : ℝ^n
8. v : ℝ^n
9. w : ℝ^n
10. ¬(u ≠ v ∧ v ≠ w ∧ (¬u-v-w))
11. ab=uv
12. cp=uw
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  p  :  \mBbbR{}\^{}n
6.  cp  \mgeq{}  ab
\mvdash{}  d(a;b)  \mleq{}  d(c;p)


By

---

Latex:
((BLemma  `not-rless`  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  D  -2  THEN  (D  0  THENA  Auto)  THEN  ExRepD)

---

Home Index