---

Step * 2 2 3 of Lemma inhabited-covers-reals-implies

.....antecedent..... 
1. ∃c:ℝ
    (((r0 ≤ c) ∧ (c < r1))
    ∧ (∀[A,B:ℝ ⟶ ℙ].
         ((∀r:ℝ. (A[r] ∨ B[r]))
         ⇒ (∀a,b:ℝ.
               (((A a) ∧ (B b) ∧ (a ≤ b))
               ⇒ (∃a',b':ℝ. ((A a') ∧ (B b') ∧ (a ≤ a') ∧ (a' ≤ b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))))))
2. [A] : ℝ ⟶ ℙ
3. [B] : ℝ ⟶ ℙ
4. ∃a:ℝ. A[a]
5. ∃b:ℝ. B[b]
6. ∀r:ℝ. (A[r] ∨ B[r])
7. a : ℝ
8. b : ℝ
9. A a
10. B b
11. b ≤ a
⊢ ∃c:ℝ
   (((r0 ≤ c) ∧ (c < r1))
   ∧ (∀a,b:ℝ.
        (((B a) ∧ (A b) ∧ (a ≤ b))
        ⇒ (∃a',b':ℝ. ((B a') ∧ (A b') ∧ (a ≤ a') ∧ (a' ≤ b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))))
BY
{ (ParallelOp 1 THEN ParallelOp 2 THEN InstHyp [⌜B⌝;⌜A⌝] 3⋅ THEN Auto) }

1
1. c : ℝ
2. r0 ≤ c
3. c < r1
4. ∀[A,B:ℝ ⟶ ℙ].
     ((∀r:ℝ. (A[r] ∨ B[r]))
     ⇒ (∀a,b:ℝ.
           (((A a) ∧ (B b) ∧ (a ≤ b))
           ⇒ (∃a',b':ℝ. ((A a') ∧ (B b') ∧ (a ≤ a') ∧ (a' ≤ b') ∧ (b' ≤ b) ∧ ((b' - a') ≤ ((b - a) * c)))))))
5. [A] : ℝ ⟶ ℙ
6. [B] : ℝ ⟶ ℙ
7. ∃a:ℝ. A[a]
8. ∃b:ℝ. B[b]
9. ∀r:ℝ. (A[r] ∨ B[r])
10. a : ℝ
11. b : ℝ
12. A a
13. B b
14. b ≤ a
15. r : ℝ
⊢ B[r] ∨ A[r]

---

Latex:

---

Latex:
.....antecedent..... 
1.  \mexists{}c:\mBbbR{}
        (((r0  \mleq{}  c)  \mwedge{}  (c  <  r1))
        \mwedge{}  (\mforall{}[A,B:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].
                  ((\mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r]))
                  {}\mRightarrow{}  (\mforall{}a,b:\mBbbR{}.
                              (((A  a)  \mwedge{}  (B  b)  \mwedge{}  (a  \mleq{}  b))
                              {}\mRightarrow{}  (\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)  *  c)))))))))
2.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
4.  \mexists{}a:\mBbbR{}.  A[a]
5.  \mexists{}b:\mBbbR{}.  B[b]
6.  \mforall{}r:\mBbbR{}.  (A[r]  \mvee{}  B[r])
7.  a  :  \mBbbR{}
8.  b  :  \mBbbR{}
9.  A  a
10.  B  b
11.  b  \mleq{}  a
\mvdash{}  \mexists{}c:\mBbbR{}
      (((r0  \mleq{}  c)  \mwedge{}  (c  <  r1))
      \mwedge{}  (\mforall{}a,b:\mBbbR{}.
                (((B  a)  \mwedge{}  (A  b)  \mwedge{}  (a  \mleq{}  b))
                {}\mRightarrow{}  (\mexists{}a',b':\mBbbR{}
                          ((B  a')  \mwedge{}  (A  b')  \mwedge{}  (a  \mleq{}  a')  \mwedge{}  (a'  \mleq{}  b')  \mwedge{}  (b'  \mleq{}  b)  \mwedge{}  ((b'  -  a')  \mleq{}  ((b  -  a)  *  c)))))))


By

---

Latex:
(ParallelOp  1  THEN  ParallelOp  2  THEN  InstHyp  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]  3\mcdot{}  THEN  Auto)

---

Home Index