---

Step * 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
⊢ ∃a',b':ℝ. ((A a') ∧ (B b') ∧ (a ≤ a') ∧ (a' ≤ b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * (r1/r(2)))))
BY
{ ((InstLemma `ravg-weak-between` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN (InstLemma `ravg-dist` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN (Assert A[ravg(a;b)] ∨ B[ravg(a;b)] BY
               Auto)
   THEN (D -1 THENL [InstConcl [⌜ravg(a;b)⌝;⌜b⌝]⋅; InstConcl [⌜a⌝;⌜ravg(a;b)⌝]⋅])
   THEN Auto) }

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

2
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)))

---

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
\mvdash{}  \mexists{}a',b':\mBbbR{}
      ((A  a')  \mwedge{}  (B  b')  \mwedge{}  (a  \mleq{}  a')  \mwedge{}  (a'  \mleq{}  b')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  ((b'  -  a')  \mleq{}  ((b  -  a)  *  (r1/r(2)))))


By

---

Latex:
((InstLemma  `ravg-weak-between`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `ravg-dist`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  A[ravg(a;b)]  \mvee{}  B[ravg(a;b)]  BY
                          Auto)
  THEN  (D  -1  THENL  [InstConcl  [\mkleeneopen{}ravg(a;b)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{};  InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}ravg(a;b)\mkleeneclose{}]\mcdot{}])
  THEN  Auto)

---

Home Index