---

Step * 1 1 1 1 of Lemma inhabited-covers-reals-implies


1. r0 ≤ (r1/r(2))
2. (r1/r(2)) < r1
3. A : ℝ ⟶ ℙ
4. B : ℝ ⟶ ℙ
5. ∀r:ℝ. (A[r] ∨ B[r])
6. a : ℝ
7. b : ℝ
8. A a
9. B b
10. a ≤ b
11. a ≤ ravg(a;b)
12. ravg(a;b) ≤ b
13. |ravg(a;b) - a| = ((r1/r(2)) * |b - a|)
14. |ravg(a;b) - b| = ((r1/r(2)) * |b - a|)
15. A[ravg(a;b)]
16. A ravg(a;b)
17. B b
18. a ≤ ravg(a;b)
19. ravg(a;b) ≤ b
20. b ≤ b
21. ((r1/r(2)) * |b - a|) = (b - ravg(a;b))
⊢ ((r1/r(2)) * |b - a|) ≤ ((b - a) * (r1/r(2)))
BY
{ (RWO "rabs-of-nonneg" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r0  \mleq{}  (r1/r(2))
2.  (r1/r(2))  <  r1
3.  A  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
4.  B  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r])
6.  a  :  \mBbbR{}
7.  b  :  \mBbbR{}
8.  A  a
9.  B  b
10.  a  \mleq{}  b
11.  a  \mleq{}  ravg(a;b)
12.  ravg(a;b)  \mleq{}  b
13.  |ravg(a;b)  -  a|  =  ((r1/r(2))  *  |b  -  a|)
14.  |ravg(a;b)  -  b|  =  ((r1/r(2))  *  |b  -  a|)
15.  A[ravg(a;b)]
16.  A  ravg(a;b)
17.  B  b
18.  a  \mleq{}  ravg(a;b)
19.  ravg(a;b)  \mleq{}  b
20.  b  \mleq{}  b
21.  ((r1/r(2))  *  |b  -  a|)  =  (b  -  ravg(a;b))
\mvdash{}  ((r1/r(2))  *  |b  -  a|)  \mleq{}  ((b  -  a)  *  (r1/r(2)))


By

---

Latex:
(RWO  "rabs-of-nonneg"  0  THEN  Auto)

---

Home Index