---

Step * 1 1 of Lemma reals-connected


1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x])
4. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x])
5. a : ℝ ⟶ 𝔹
6. b : ℝ ⟶ 𝔹
7. ∀x:ℝ. ((↑(a x)) ⇒ A[x])
8. ∀x:ℝ. ((↑(b x)) ⇒ B[x])
9. ∀x:ℝ. ((↑(a x)) ∨ (↑(b x)))
10. f : ℕ ⟶ ℝ
11. g : ℕ ⟶ ℝ
12. x : ℝ
13. ∀n:ℕ. (↑(a (f n)))
14. ∀n:ℕ. (↑(b (g n)))
15. lim n→∞.f n = x
16. lim n→∞.g n = x
⊢ ∃r:ℝ. (A[r] ∧ B[r])
BY
{ ((InstLemma `connectedness-main-lemma-ext` [⌜x⌝]⋅ THENA Auto)
   THEN (Assert (↑(a accelerate(3;x))) ∨ (↑(b accelerate(3;x))) BY
               Auto)
   THEN (D -1 THENL [InstHyp [⌜g⌝;⌜a⌝] (-2)⋅; InstHyp [⌜f⌝;⌜b⌝] (-2)⋅])
   THEN Auto
   THEN ExRepD
   THEN D 0 With ⌜z⌝ 
   THEN Auto) }

1
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x])
4. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x])
5. a : ℝ ⟶ 𝔹
6. b : ℝ ⟶ 𝔹
7. ∀x:ℝ. ((↑(a x)) ⇒ A[x])
8. ∀x:ℝ. ((↑(b x)) ⇒ B[x])
9. ∀x:ℝ. ((↑(a x)) ∨ (↑(b x)))
10. f : ℕ ⟶ ℝ
11. g : ℕ ⟶ ℝ
12. x : ℝ
13. ∀n:ℕ. (↑(a (f n)))
14. ∀n:ℕ. (↑(b (g n)))
15. lim n→∞.f n = x
16. lim n→∞.g n = x
17. ∀g:ℕ ⟶ ℝ. (lim n→∞.g n = x ⇒ (∀P:ℝ ⟶ 𝔹. ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:{ℕ| (z = (g n))})))
18. ↑(a accelerate(3;x))
19. z : {z:ℝ| a z = a accelerate(3;x)} 
20. n : ℕ
21. z = (g n)
22. A[z]
⊢ B[z]

2
1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (A[y] ⇒ A[x])
4. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  (B[y] ⇒ B[x])
5. a : ℝ ⟶ 𝔹
6. b : ℝ ⟶ 𝔹
7. ∀x:ℝ. ((↑(a x)) ⇒ A[x])
8. ∀x:ℝ. ((↑(b x)) ⇒ B[x])
9. ∀x:ℝ. ((↑(a x)) ∨ (↑(b x)))
10. f : ℕ ⟶ ℝ
11. g : ℕ ⟶ ℝ
12. x : ℝ
13. ∀n:ℕ. (↑(a (f n)))
14. ∀n:ℕ. (↑(b (g n)))
15. lim n→∞.f n = x
16. lim n→∞.g n = x
17. ∀g:ℕ ⟶ ℝ. (lim n→∞.g n = x ⇒ (∀P:ℝ ⟶ 𝔹. ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:{ℕ| (z = (g n))})))
18. ↑(b accelerate(3;x))
19. z : {z:ℝ| b z = b accelerate(3;x)} 
20. n : ℕ
21. z = (f n)
⊢ A[z]

---

Latex:

---

Latex:

1.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
4.  \mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
5.  a  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
6.  b  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
7.  \mforall{}x:\mBbbR{}.  ((\muparrow{}(a  x))  {}\mRightarrow{}  A[x])
8.  \mforall{}x:\mBbbR{}.  ((\muparrow{}(b  x))  {}\mRightarrow{}  B[x])
9.  \mforall{}x:\mBbbR{}.  ((\muparrow{}(a  x))  \mvee{}  (\muparrow{}(b  x)))
10.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
11.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
12.  x  :  \mBbbR{}
13.  \mforall{}n:\mBbbN{}.  (\muparrow{}(a  (f  n)))
14.  \mforall{}n:\mBbbN{}.  (\muparrow{}(b  (g  n)))
15.  lim  n\mrightarrow{}\minfty{}.f  n  =  x
16.  lim  n\mrightarrow{}\minfty{}.g  n  =  x
\mvdash{}  \mexists{}r:\mBbbR{}.  (A[r]  \mwedge{}  B[r])


By

---

Latex:
((InstLemma  `connectedness-main-lemma-ext`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (\muparrow{}(a  accelerate(3;x)))  \mvee{}  (\muparrow{}(b  accelerate(3;x)))  BY
                          Auto)
  THEN  (D  -1  THENL  [InstHyp  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (-2)\mcdot{};  InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-2)\mcdot{}])
  THEN  Auto
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}z\mkleeneclose{} 
  THEN  Auto)

---

Home Index