---

Step * 1 1 1 1 1 1 1 2 of Lemma real-subset-connected


1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. SqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((X y) ⇒ (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝ| X x}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x
6. [A] : {x:ℝ| X x}  ⟶ ℙ
7. [B] : {x:ℝ| X x}  ⟶ ℙ
8. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x])
9. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x])
10. a : {x:ℝ| X x}  ⟶ 𝔹
11. b : {x:ℝ| X x}  ⟶ 𝔹
12. ∀x:{x:ℝ| X x} . ((↑(a x)) ⇒ A[x])
13. ∀x:{x:ℝ| X x} . ((↑(b x)) ⇒ B[x])
14. x2 : {x:ℝ| X x} 
15. ↑(a x2)
16. x1 : {x:ℝ| X x} 
17. ↑(b x1)
18. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
19. f : ℕ ⟶ {x:ℝ| X x} 
20. g : ℕ ⟶ {x:ℝ| X x} 
21. ∀n:ℕ. (↑(a (f n)))
22. ∀n:ℕ. (↑(b (g n)))
23. aa : ℝ ⟶ 𝔹
24. ∀x:{x:ℝ| X x} . aa x = a x
25. bb : ℝ ⟶ 𝔹
26. ∀x:{x:ℝ| X x} . bb x = b x
27. x : ℝ
28. ∀k:ℕ+. ∃y:ℝ. ((y = x ∈ (ℕ+k ⟶ ℤ)) ∧ (X y))
29. lim n→∞.f n = x
30. lim n→∞.g n = x
31. ∃z:{z:ℝ| bb z = bb accelerate(3;x)} . (∃n:ℕ [(z = (f n))])
32. ∃z:{z:ℝ| aa z = aa accelerate(3;x)} . (∃n:ℕ [(z = (g n))])
33. aa accelerate(3;x) = tt ∨ bb accelerate(3;x) = tt
⊢ ∃r:{x:ℝ| X x} . (A[r] ∧ B[r])
BY
{ (((D -1 THENL [Thin (-3); Thin (-2)]) THEN ExRepD)
   THENL [((Assert aa z = tt BY (DVar `z' THEN Auto)) THEN D 0 With ⌜g n⌝  THEN Auto)
         ; ((Assert bb z = tt BY (DVar `z' THEN Auto)) THEN D 0 With ⌜f n⌝  THEN Auto)]
) }

1
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. SqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((X y) ⇒ (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝ| X x}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x
6. [A] : {x:ℝ| X x}  ⟶ ℙ
7. [B] : {x:ℝ| X x}  ⟶ ℙ
8. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x])
9. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x])
10. a : {x:ℝ| X x}  ⟶ 𝔹
11. b : {x:ℝ| X x}  ⟶ 𝔹
12. ∀x:{x:ℝ| X x} . ((↑(a x)) ⇒ A[x])
13. ∀x:{x:ℝ| X x} . ((↑(b x)) ⇒ B[x])
14. x2 : {x:ℝ| X x} 
15. ↑(a x2)
16. x1 : {x:ℝ| X x} 
17. ↑(b x1)
18. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
19. f : ℕ ⟶ {x:ℝ| X x} 
20. g : ℕ ⟶ {x:ℝ| X x} 
21. ∀n:ℕ. (↑(a (f n)))
22. ∀n:ℕ. (↑(b (g n)))
23. aa : ℝ ⟶ 𝔹
24. ∀x:{x:ℝ| X x} . aa x = a x
25. bb : ℝ ⟶ 𝔹
26. ∀x:{x:ℝ| X x} . bb x = b x
27. x : ℝ
28. ∀k:ℕ+. ∃y:ℝ. ((y = x ∈ (ℕ+k ⟶ ℤ)) ∧ (X y))
29. lim n→∞.f n = x
30. lim n→∞.g n = x
31. z : {z:ℝ| aa z = aa accelerate(3;x)} 
32. n : ℕ
33. z = (g n)
34. aa accelerate(3;x) = tt
35. aa z = tt
⊢ A[g n]

2
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. SqStable(X x)
3. ∀x:ℝ. ∀y:{y:ℝ| x = y} .  ((X y) ⇒ (X x))
4. dense-in-interval((-∞, ∞);X)
5. ∀Q:{x:ℝ| X x}  ⟶ 𝔹. ∃Q':ℝ ⟶ 𝔹. ∀x:{x:ℝ| X x} . Q' x = Q x
6. [A] : {x:ℝ| X x}  ⟶ ℙ
7. [B] : {x:ℝ| X x}  ⟶ ℙ
8. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (A[y] ⇒ A[x])
9. ∀x:{x:ℝ| X x} . ∀y:{y:{x:ℝ| X x} | x = y} .  (B[y] ⇒ B[x])
10. a : {x:ℝ| X x}  ⟶ 𝔹
11. b : {x:ℝ| X x}  ⟶ 𝔹
12. ∀x:{x:ℝ| X x} . ((↑(a x)) ⇒ A[x])
13. ∀x:{x:ℝ| X x} . ((↑(b x)) ⇒ B[x])
14. x2 : {x:ℝ| X x} 
15. ↑(a x2)
16. x1 : {x:ℝ| X x} 
17. ↑(b x1)
18. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
19. f : ℕ ⟶ {x:ℝ| X x} 
20. g : ℕ ⟶ {x:ℝ| X x} 
21. ∀n:ℕ. (↑(a (f n)))
22. ∀n:ℕ. (↑(b (g n)))
23. aa : ℝ ⟶ 𝔹
24. ∀x:{x:ℝ| X x} . aa x = a x
25. bb : ℝ ⟶ 𝔹
26. ∀x:{x:ℝ| X x} . bb x = b x
27. x : ℝ
28. ∀k:ℕ+. ∃y:ℝ. ((y = x ∈ (ℕ+k ⟶ ℤ)) ∧ (X y))
29. lim n→∞.f n = x
30. lim n→∞.g n = x
31. z : {z:ℝ| bb z = bb accelerate(3;x)} 
32. n : ℕ
33. z = (f n)
34. bb accelerate(3;x) = tt
35. bb z = tt
36. A[f n]
⊢ B[f n]

---

Latex:

---

Latex:

1.  X  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}x:\mBbbR{}.  SqStable(X  x)
3.  \mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  =  y\}  .    ((X  y)  {}\mRightarrow{}  (X  x))
4.  dense-in-interval((-\minfty{},  \minfty{});X)
5.  \mforall{}Q:\{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}.  \mexists{}Q':\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  Q'  x  =  Q  x
6.  [A]  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbP{}
7.  [B]  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbP{}
8.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  X  x\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
9.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  X  x\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
10.  a  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}
11.  b  :  \{x:\mBbbR{}|  X  x\}    {}\mrightarrow{}  \mBbbB{}
12.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  x))  {}\mRightarrow{}  A[x])
13.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(b  x))  {}\mRightarrow{}  B[x])
14.  x2  :  \{x:\mBbbR{}|  X  x\} 
15.  \muparrow{}(a  x2)
16.  x1  :  \{x:\mBbbR{}|  X  x\} 
17.  \muparrow{}(b  x1)
18.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  ((\muparrow{}(a  x))  \mvee{}  (\muparrow{}(b  x)))
19.  f  :  \mBbbN{}  {}\mrightarrow{}  \{x:\mBbbR{}|  X  x\} 
20.  g  :  \mBbbN{}  {}\mrightarrow{}  \{x:\mBbbR{}|  X  x\} 
21.  \mforall{}n:\mBbbN{}.  (\muparrow{}(a  (f  n)))
22.  \mforall{}n:\mBbbN{}.  (\muparrow{}(b  (g  n)))
23.  aa  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
24.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  aa  x  =  a  x
25.  bb  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
26.  \mforall{}x:\{x:\mBbbR{}|  X  x\}  .  bb  x  =  b  x
27.  x  :  \mBbbR{}
28.  \mforall{}k:\mBbbN{}\msupplus{}.  \mexists{}y:\mBbbR{}.  ((y  =  x)  \mwedge{}  (X  y))
29.  lim  n\mrightarrow{}\minfty{}.f  n  =  x
30.  lim  n\mrightarrow{}\minfty{}.g  n  =  x
31.  \mexists{}z:\{z:\mBbbR{}|  bb  z  =  bb  accelerate(3;x)\}  .  (\mexists{}n:\mBbbN{}  [(z  =  (f  n))])
32.  \mexists{}z:\{z:\mBbbR{}|  aa  z  =  aa  accelerate(3;x)\}  .  (\mexists{}n:\mBbbN{}  [(z  =  (g  n))])
33.  aa  accelerate(3;x)  =  tt  \mvee{}  bb  accelerate(3;x)  =  tt
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  X  x\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
(((D  -1  THENL  [Thin  (-3);  Thin  (-2)])  THEN  ExRepD)
  THENL  [((Assert  aa  z  =  tt  BY  (DVar  `z'  THEN  Auto))  THEN  D  0  With  \mkleeneopen{}g  n\mkleeneclose{}    THEN  Auto)
              ;  ((Assert  bb  z  =  tt  BY  (DVar  `z'  THEN  Auto))  THEN  D  0  With  \mkleeneopen{}f  n\mkleeneclose{}    THEN  Auto)]
)

---

Home Index