Step
*
1
1
1
2
2
1
1
1
2
of Lemma
real-subset-connected-lemma
1. X : ℝ ⟶ ℙ
2. dense-in-interval((-∞, ∞);X)
3. a : {x:ℝ| X x} ⟶ 𝔹
4. b : {x:ℝ| X x} ⟶ 𝔹
5. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
6. a0 : {x:ℝ| X x}
7. b0 : {x:ℝ| X x}
8. ↑(a a0)
9. ↑(b b0)
10. a0 < b0
11. ∀u,v:{x:ℝ| X x} .
((u < v)
⇒ (∃p:{x:ℝ| X x}
(((u < p) ∧ (p < v)) ∧ ((p - u) ≤ ((r(2)/r(3)) * (v - u))) ∧ ((v - p) ≤ ((r(2)/r(3)) * (v - u))))))
12. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
∃pq':{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd(pq')) - fst(pq')) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
((pq' = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ (pq' = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )))))
13. h : pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} ⟶ {pq:{x:ℝ| X\000C x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq)))
∧ (↑(a (fst(pq))))
∧ (↑(b (snd(pq))))}
14. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd((h pq))) - fst((h pq))) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
(((h pq) = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ ((h pq) = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} \000C)))))
15. ∀n:ℕ
(primrec(n;<a0, b0>;λi.h) ∈ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} )
16. λn.primrec(n;<a0, b0>;λi.h) ∈ ℕ ⟶ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
⊢ ∀n:ℕ
((↑(a (fst(primrec(n;<a0, b0>;λi.h)))))
∧ (↑(b (snd(primrec(n;<a0, b0>;λi.h)))))
∧ let a,b = primrec(n;<a0, b0>;λi.h)
in ∃p:{x:ℝ| X x}
(((a < p) ∧ (p < b))
∧ (((primrec(n + 1;<a0, b0>;λi.h) = <a, p> ∈ (ℝ × ℝ)) ∧ ((p - a) ≤ ((r(2)/r(3)) * (b - a))))
∨ ((primrec(n + 1;<a0, b0>;λi.h) = <p, b> ∈ (ℝ × ℝ)) ∧ ((b - p) ≤ ((r(2)/r(3)) * (b - a)))))))
BY
{ Auto }
1
1. X : ℝ ⟶ ℙ
2. dense-in-interval((-∞, ∞);X)
3. a : {x:ℝ| X x} ⟶ 𝔹
4. b : {x:ℝ| X x} ⟶ 𝔹
5. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
6. a0 : {x:ℝ| X x}
7. b0 : {x:ℝ| X x}
8. ↑(a a0)
9. ↑(b b0)
10. a0 < b0
11. ∀u,v:{x:ℝ| X x} .
((u < v)
⇒ (∃p:{x:ℝ| X x}
(((u < p) ∧ (p < v)) ∧ ((p - u) ≤ ((r(2)/r(3)) * (v - u))) ∧ ((v - p) ≤ ((r(2)/r(3)) * (v - u))))))
12. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
∃pq':{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd(pq')) - fst(pq')) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
((pq' = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ (pq' = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )))))
13. h : pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} ⟶ {pq:{x:ℝ| X\000C x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq)))
∧ (↑(a (fst(pq))))
∧ (↑(b (snd(pq))))}
14. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd((h pq))) - fst((h pq))) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
(((h pq) = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ ((h pq) = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} \000C)))))
15. ∀n:ℕ
(primrec(n;<a0, b0>;λi.h) ∈ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} )
16. λn.primrec(n;<a0, b0>;λi.h) ∈ ℕ ⟶ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
17. n : ℕ
⊢ ↑(a (fst(primrec(n;<a0, b0>;λi.h))))
2
1. X : ℝ ⟶ ℙ
2. dense-in-interval((-∞, ∞);X)
3. a : {x:ℝ| X x} ⟶ 𝔹
4. b : {x:ℝ| X x} ⟶ 𝔹
5. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
6. a0 : {x:ℝ| X x}
7. b0 : {x:ℝ| X x}
8. ↑(a a0)
9. ↑(b b0)
10. a0 < b0
11. ∀u,v:{x:ℝ| X x} .
((u < v)
⇒ (∃p:{x:ℝ| X x}
(((u < p) ∧ (p < v)) ∧ ((p - u) ≤ ((r(2)/r(3)) * (v - u))) ∧ ((v - p) ≤ ((r(2)/r(3)) * (v - u))))))
12. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
∃pq':{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd(pq')) - fst(pq')) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
((pq' = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ (pq' = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )))))
13. h : pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} ⟶ {pq:{x:ℝ| X\000C x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq)))
∧ (↑(a (fst(pq))))
∧ (↑(b (snd(pq))))}
14. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd((h pq))) - fst((h pq))) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
(((h pq) = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ ((h pq) = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} \000C)))))
15. ∀n:ℕ
(primrec(n;<a0, b0>;λi.h) ∈ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} )
16. λn.primrec(n;<a0, b0>;λi.h) ∈ ℕ ⟶ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
17. n : ℕ
18. ↑(a (fst(primrec(n;<a0, b0>;λi.h))))
⊢ ↑(b (snd(primrec(n;<a0, b0>;λi.h))))
3
1. X : ℝ ⟶ ℙ
2. dense-in-interval((-∞, ∞);X)
3. a : {x:ℝ| X x} ⟶ 𝔹
4. b : {x:ℝ| X x} ⟶ 𝔹
5. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
6. a0 : {x:ℝ| X x}
7. b0 : {x:ℝ| X x}
8. ↑(a a0)
9. ↑(b b0)
10. a0 < b0
11. ∀u,v:{x:ℝ| X x} .
((u < v)
⇒ (∃p:{x:ℝ| X x}
(((u < p) ∧ (p < v)) ∧ ((p - u) ≤ ((r(2)/r(3)) * (v - u))) ∧ ((v - p) ≤ ((r(2)/r(3)) * (v - u))))))
12. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
∃pq':{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd(pq')) - fst(pq')) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
((pq' = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ (pq' = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )))))
13. h : pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} ⟶ {pq:{x:ℝ| X\000C x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq)))
∧ (↑(a (fst(pq))))
∧ (↑(b (snd(pq))))}
14. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd((h pq))) - fst((h pq))) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
(((h pq) = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ ((h pq) = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} \000C)))))
15. ∀n:ℕ
(primrec(n;<a0, b0>;λi.h) ∈ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} )
16. λn.primrec(n;<a0, b0>;λi.h) ∈ ℕ ⟶ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
17. n : ℕ
18. ↑(a (fst(primrec(n;<a0, b0>;λi.h))))
19. ↑(b (snd(primrec(n;<a0, b0>;λi.h))))
⊢ let a,b = primrec(n;<a0, b0>;λi.h)
in ∃p:{x:ℝ| X x}
(((a < p) ∧ (p < b))
∧ (((primrec(n + 1;<a0, b0>;λi.h) = <a, p> ∈ (ℝ × ℝ)) ∧ ((p - a) ≤ ((r(2)/r(3)) * (b - a))))
∨ ((primrec(n + 1;<a0, b0>;λi.h) = <p, b> ∈ (ℝ × ℝ)) ∧ ((b - p) ≤ ((r(2)/r(3)) * (b - a))))))
Latex:
Latex:
1. X : \mBbbR{} {}\mrightarrow{} \mBbbP{}
2. dense-in-interval((-\minfty{}, \minfty{});X)
3. a : \{x:\mBbbR{}| X x\} {}\mrightarrow{} \mBbbB{}
4. b : \{x:\mBbbR{}| X x\} {}\mrightarrow{} \mBbbB{}
5. \mforall{}x:\{x:\mBbbR{}| X x\} . ((\muparrow{}(a x)) \mvee{} (\muparrow{}(b x)))
6. a0 : \{x:\mBbbR{}| X x\}
7. b0 : \{x:\mBbbR{}| X x\}
8. \muparrow{}(a a0)
9. \muparrow{}(b b0)
10. a0 < b0
11. \mforall{}u,v:\{x:\mBbbR{}| X x\} .
((u < v)
{}\mRightarrow{} (\mexists{}p:\{x:\mBbbR{}| X x\}
(((u < p) \mwedge{} (p < v))
\mwedge{} ((p - u) \mleq{} ((r(2)/r(3)) * (v - u)))
\mwedge{} ((v - p) \mleq{} ((r(2)/r(3)) * (v - u))))))
12. \mforall{}pq:\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\000C\}
\mexists{}pq':\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq)\000C)))\}
((((snd(pq')) - fst(pq')) \mleq{} ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
\mwedge{} (\mexists{}xx:\{x:\mBbbR{}| X x\} . ((pq' = <fst(pq), xx>) \mvee{} (pq' = <xx, snd(pq)>))))
13. h : pq:\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq)\000C)))\}
{}\mrightarrow{} \{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\}
14. \mforall{}pq:\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\000C\}
((((snd((h pq))) - fst((h pq))) \mleq{} ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
\mwedge{} (\mexists{}xx:\{x:\mBbbR{}| X x\} . (((h pq) = <fst(pq), xx>) \mvee{} ((h pq) = <xx, snd(pq)>))))
15. \mforall{}n:\mBbbN{}
(primrec(n;<a0, b0>\mlambda{}i.h) \mmember{} \{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} |
((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\} )
16. \mlambda{}n.primrec(n;<a0, b0>\mlambda{}i.h) \mmember{} \mBbbN{} {}\mrightarrow{} \{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} |
((fst(pq)) < (snd(pq)))
\mwedge{} (\muparrow{}(a (fst(pq))))
\mwedge{} (\muparrow{}(b (snd(pq))))\}
\mvdash{} \mforall{}n:\mBbbN{}
((\muparrow{}(a (fst(primrec(n;<a0, b0>\mlambda{}i.h)))))
\mwedge{} (\muparrow{}(b (snd(primrec(n;<a0, b0>\mlambda{}i.h)))))
\mwedge{} let a,b = primrec(n;<a0, b0>\mlambda{}i.h)
in \mexists{}p:\{x:\mBbbR{}| X x\}
(((a < p) \mwedge{} (p < b))
\mwedge{} (((primrec(n + 1;<a0, b0>\mlambda{}i.h) = <a, p>) \mwedge{} ((p - a) \mleq{} ((r(2)/r(3)) * (b - a))))
\mvee{} ((primrec(n + 1;<a0, b0>\mlambda{}i.h) = <p, b>) \mwedge{} ((b - p) \mleq{} ((r(2)/r(3)) * (b - a)))))))
By
Latex:
Auto
Home
Index