---

Step * 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
⊢ (b - ravg(a;b)) ≤ ((b - a) * (r1/r(2)))
BY
{ (Assert |ravg(a;b) - b| = (b - ravg(a;b)) BY
         (RWO "rabs-difference-symmetry" 0 THEN EAuto 1)) }

1
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. |ravg(a;b) - b| = (b - ravg(a;b))
⊢ (b - ravg(a;b)) ≤ ((b - a) * (r1/r(2)))

---

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
\mvdash{}  (b  -  ravg(a;b))  \mleq{}  ((b  -  a)  *  (r1/r(2)))


By

---

Latex:
(Assert  |ravg(a;b)  -  b|  =  (b  -  ravg(a;b))  BY
              (RWO  "rabs-difference-symmetry"  0  THEN  EAuto  1))

---

Home Index