---

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


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,b:ℝ. ((A a) ∧ (B b) ∧ ((a ≤ b) ∨ (b ≤ a)))
⊢ ∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)
BY
{ ((RepeatFor 5 (D -1) THENL [InstLemma `closures-meet` [⌜A⌝;⌜B⌝]⋅; InstLemma `closures-meet` [⌜B⌝;⌜A⌝]⋅]) THEN Auto) }

1
.....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. a ≤ b
⊢ ∃c:ℝ
   (((r0 ≤ c) ∧ (c < r1))
   ∧ (∀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
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. a ≤ b
12. ∃y:ℝ. (y ∈ closure(A) ∧ y ∈ closure(B))
⊢ ∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)

3
.....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)))))))

4
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
12. ∃y:ℝ. (y ∈ closure(B) ∧ y ∈ closure(A))
⊢ ∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)

---

Latex:

---

Latex:

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.  \mexists{}a,b:\mBbbR{}.  ((A  a)  \mwedge{}  (B  b)  \mwedge{}  ((a  \mleq{}  b)  \mvee{}  (b  \mleq{}  a)))
\mvdash{}  \mexists{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mexists{}x:\mBbbR{}.  ((\mforall{}n:\mBbbN{}.  A[f  n])  \mwedge{}  (\mforall{}n:\mBbbN{}.  B[g  n])  \mwedge{}  lim  n\mrightarrow{}\minfty{}.f  n  =  x  \mwedge{}  lim  n\mrightarrow{}\minfty{}.g  n  =  x)


By

---

Latex:
((RepeatFor  5  (D  -1)
    THENL  [InstLemma  `closures-meet`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{};  InstLemma  `closures-meet`  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}]
  )
  THEN  Auto
  )

---

Home Index