---

Step * 1 2 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. B[ravg(a;b)]
16. A a
17. B ravg(a;b)
18. a ≤ a
19. a ≤ ravg(a;b)
20. ravg(a;b) ≤ b
⊢ (ravg(a;b) - a) ≤ ((b - a) * (r1/r(2)))
BY
{ (RWO "rabs-of-nonneg" (-8) 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.  B[ravg(a;b)]
16.  A  a
17.  B  ravg(a;b)
18.  a  \mleq{}  a
19.  a  \mleq{}  ravg(a;b)
20.  ravg(a;b)  \mleq{}  b
\mvdash{}  (ravg(a;b)  -  a)  \mleq{}  ((b  -  a)  *  (r1/r(2)))


By

---

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

---

Home Index