Step
*
1
1
1
1
1
1
1
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))])
⊢ ∃r:{x:ℝ| X x} . (A[r] ∧ B[r])
BY
{ Assert ⌜aa accelerate(3;x) = tt ∨ bb accelerate(3;x) = tt⌝⋅ }
1
.....assertion.....
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))])
⊢ aa accelerate(3;x) = tt ∨ bb accelerate(3;x) = tt
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)} . (∃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])
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))])
\mvdash{} \mexists{}r:\{x:\mBbbR{}| X x\} . (A[r] \mwedge{} B[r])
By
Latex:
Assert \mkleeneopen{}aa accelerate(3;x) = tt \mvee{} bb accelerate(3;x) = tt\mkleeneclose{}\mcdot{}
Home
Index