Step | Hyp | Ref
| Expression |
1 | | dya2ioc.1 |
. . . 4
⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
2 | | ovex 7304 |
. . . 4
⊢ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈ V |
3 | 1, 2 | elrnmpo 7404 |
. . 3
⊢ (𝑑 ∈ ran 𝐼 ↔ ∃𝑥 ∈ ℤ ∃𝑛 ∈ ℤ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
4 | | simpr 485 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
5 | | mnfxr 11033 |
. . . . . . . . . 10
⊢ -∞
∈ ℝ* |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → -∞
∈ ℝ*) |
7 | | simpl 483 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈
ℤ) |
8 | 7 | zred 12425 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑥 ∈
ℝ) |
9 | | 2rp 12734 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ+ |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 2 ∈
ℝ+) |
11 | | simpr 485 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 𝑛 ∈
ℤ) |
12 | 10, 11 | rpexpcld 13960 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
(2↑𝑛) ∈
ℝ+) |
13 | 8, 12 | rerpdivcld 12802 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈ ℝ) |
14 | 13 | rexrd 11026 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 / (2↑𝑛)) ∈
ℝ*) |
15 | | 1red 10977 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → 1 ∈
ℝ) |
16 | 8, 15 | readdcld 11005 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑥 + 1) ∈
ℝ) |
17 | 16, 12 | rerpdivcld 12802 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈
ℝ) |
18 | 17 | rexrd 11026 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 + 1) / (2↑𝑛)) ∈
ℝ*) |
19 | | mnflt 12858 |
. . . . . . . . . 10
⊢ ((𝑥 / (2↑𝑛)) ∈ ℝ → -∞ < (𝑥 / (2↑𝑛))) |
20 | 13, 19 | syl 17 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → -∞
< (𝑥 / (2↑𝑛))) |
21 | | difioo 31099 |
. . . . . . . . 9
⊢
(((-∞ ∈ ℝ* ∧ (𝑥 / (2↑𝑛)) ∈ ℝ* ∧ ((𝑥 + 1) / (2↑𝑛)) ∈ ℝ*)
∧ -∞ < (𝑥 /
(2↑𝑛))) →
((-∞(,)((𝑥 + 1) /
(2↑𝑛))) ∖
(-∞(,)(𝑥 /
(2↑𝑛)))) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
22 | 6, 14, 18, 20, 21 | syl31anc 1372 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) →
((-∞(,)((𝑥 + 1) /
(2↑𝑛))) ∖
(-∞(,)(𝑥 /
(2↑𝑛)))) = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
23 | | brsigarn 32148 |
. . . . . . . . . 10
⊢
𝔅ℝ ∈
(sigAlgebra‘ℝ) |
24 | | elrnsiga 32090 |
. . . . . . . . . 10
⊢
(𝔅ℝ ∈ (sigAlgebra‘ℝ) →
𝔅ℝ ∈ ∪ ran
sigAlgebra) |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . 9
⊢
𝔅ℝ ∈ ∪ ran
sigAlgebra |
26 | | retop 23923 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) ∈ Top |
27 | | iooretop 23927 |
. . . . . . . . . . 11
⊢
(-∞(,)((𝑥 + 1)
/ (2↑𝑛))) ∈
(topGen‘ran (,)) |
28 | | elsigagen 32111 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Top ∧ (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ (topGen‘ran
(,))) → (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ (sigaGen‘(topGen‘ran
(,)))) |
29 | 26, 27, 28 | mp2an 689 |
. . . . . . . . . 10
⊢
(-∞(,)((𝑥 + 1)
/ (2↑𝑛))) ∈
(sigaGen‘(topGen‘ran (,))) |
30 | | df-brsiga 32146 |
. . . . . . . . . 10
⊢
𝔅ℝ = (sigaGen‘(topGen‘ran
(,))) |
31 | 29, 30 | eleqtrri 2840 |
. . . . . . . . 9
⊢
(-∞(,)((𝑥 + 1)
/ (2↑𝑛))) ∈
𝔅ℝ |
32 | | iooretop 23927 |
. . . . . . . . . . 11
⊢
(-∞(,)(𝑥 /
(2↑𝑛))) ∈
(topGen‘ran (,)) |
33 | | elsigagen 32111 |
. . . . . . . . . . 11
⊢
(((topGen‘ran (,)) ∈ Top ∧ (-∞(,)(𝑥 / (2↑𝑛))) ∈ (topGen‘ran (,))) →
(-∞(,)(𝑥 /
(2↑𝑛))) ∈
(sigaGen‘(topGen‘ran (,)))) |
34 | 26, 32, 33 | mp2an 689 |
. . . . . . . . . 10
⊢
(-∞(,)(𝑥 /
(2↑𝑛))) ∈
(sigaGen‘(topGen‘ran (,))) |
35 | 34, 30 | eleqtrri 2840 |
. . . . . . . . 9
⊢
(-∞(,)(𝑥 /
(2↑𝑛))) ∈
𝔅ℝ |
36 | | difelsiga 32097 |
. . . . . . . . 9
⊢
((𝔅ℝ ∈ ∪ ran
sigAlgebra ∧ (-∞(,)((𝑥 + 1) / (2↑𝑛))) ∈ 𝔅ℝ ∧
(-∞(,)(𝑥 /
(2↑𝑛))) ∈
𝔅ℝ) → ((-∞(,)((𝑥 + 1) / (2↑𝑛))) ∖ (-∞(,)(𝑥 / (2↑𝑛)))) ∈
𝔅ℝ) |
37 | 25, 31, 35, 36 | mp3an 1460 |
. . . . . . . 8
⊢
((-∞(,)((𝑥 +
1) / (2↑𝑛))) ∖
(-∞(,)(𝑥 /
(2↑𝑛)))) ∈
𝔅ℝ |
38 | 22, 37 | eqeltrrdi 2850 |
. . . . . . 7
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈
𝔅ℝ) |
39 | 38 | adantr 481 |
. . . . . 6
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) ∈
𝔅ℝ) |
40 | 4, 39 | eqeltrd 2841 |
. . . . 5
⊢ (((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) → 𝑑 ∈
𝔅ℝ) |
41 | 40 | ex 413 |
. . . 4
⊢ ((𝑥 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → 𝑑 ∈
𝔅ℝ)) |
42 | 41 | rexlimivv 3223 |
. . 3
⊢
(∃𝑥 ∈
ℤ ∃𝑛 ∈
ℤ 𝑑 = ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛))) → 𝑑 ∈
𝔅ℝ) |
43 | 3, 42 | sylbi 216 |
. 2
⊢ (𝑑 ∈ ran 𝐼 → 𝑑 ∈
𝔅ℝ) |
44 | 43 | ssriv 3930 |
1
⊢ ran 𝐼 ⊆
𝔅ℝ |