Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → ([,]‘𝑧) = ([,]‘𝑤)) |
2 | 1 | sseq1d 3632 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴)) |
3 | 2 | elrab 3363 |
. . . . . . 7
⊢ (𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (𝑤 ∈ ran 𝐹 ∧ ([,]‘𝑤) ⊆ 𝐴)) |
4 | | simprr 796 |
. . . . . . . 8
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ (𝑤 ∈ ran 𝐹 ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ⊆ 𝐴) |
5 | | fvex 6201 |
. . . . . . . . 9
⊢
([,]‘𝑤) ∈
V |
6 | 5 | elpw 4164 |
. . . . . . . 8
⊢
(([,]‘𝑤)
∈ 𝒫 𝐴 ↔
([,]‘𝑤) ⊆ 𝐴) |
7 | 4, 6 | sylibr 224 |
. . . . . . 7
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ (𝑤 ∈ ran 𝐹 ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ∈ 𝒫 𝐴) |
8 | 3, 7 | sylan2b 492 |
. . . . . 6
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) → ([,]‘𝑤) ∈ 𝒫 𝐴) |
9 | 8 | ralrimiva 2966 |
. . . . 5
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ∀𝑤 ∈
{𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴) |
10 | | iccf 12272 |
. . . . . . 7
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
11 | | ffun 6048 |
. . . . . . 7
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢ Fun
[,] |
13 | | ssrab2 3687 |
. . . . . . . 8
⊢ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ ran 𝐹 |
14 | | dyadmbl.1 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) |
15 | 14 | dyadf 23359 |
. . . . . . . . . 10
⊢ 𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ ×
ℝ)) |
16 | | frn 6053 |
. . . . . . . . . 10
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → ran
𝐹 ⊆ ( ≤ ∩
(ℝ × ℝ))) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
⊢ ran 𝐹 ⊆ ( ≤ ∩ (ℝ
× ℝ)) |
18 | | inss2 3834 |
. . . . . . . . . 10
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
19 | | rexpssxrxp 10084 |
. . . . . . . . . 10
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
20 | 18, 19 | sstri 3612 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
21 | 17, 20 | sstri 3612 |
. . . . . . . 8
⊢ ran 𝐹 ⊆ (ℝ*
× ℝ*) |
22 | 13, 21 | sstri 3612 |
. . . . . . 7
⊢ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ (ℝ* ×
ℝ*) |
23 | 10 | fdmi 6052 |
. . . . . . 7
⊢ dom [,] =
(ℝ* × ℝ*) |
24 | 22, 23 | sseqtr4i 3638 |
. . . . . 6
⊢ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,] |
25 | | funimass4 6247 |
. . . . . 6
⊢ ((Fun [,]
∧ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (([,] “
{𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)) |
26 | 12, 24, 25 | mp2an 708 |
. . . . 5
⊢ (([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴) |
27 | 9, 26 | sylibr 224 |
. . . 4
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ([,] “ {𝑧
∈ ran 𝐹 ∣
([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴) |
28 | | sspwuni 4611 |
. . . 4
⊢ (([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴) |
29 | 27, 28 | sylib 208 |
. . 3
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴) |
30 | | eqid 2622 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
31 | 30 | rexmet 22594 |
. . . . . . 7
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
32 | | eqid 2622 |
. . . . . . . . 9
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
33 | 30, 32 | tgioo 22599 |
. . . . . . . 8
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
34 | 33 | mopni2 22298 |
. . . . . . 7
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ+ (𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴) |
35 | 31, 34 | mp3an1 1411 |
. . . . . 6
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ+
(𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴) |
36 | | elssuni 4467 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (topGen‘ran (,))
→ 𝐴 ⊆ ∪ (topGen‘ran (,))) |
37 | | uniretop 22566 |
. . . . . . . . . . . 12
⊢ ℝ =
∪ (topGen‘ran (,)) |
38 | 36, 37 | syl6sseqr 3652 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (topGen‘ran (,))
→ 𝐴 ⊆
ℝ) |
39 | 38 | sselda 3603 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ) |
40 | | rpre 11839 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
41 | 30 | bl2ioo 22595 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
42 | 39, 40, 41 | syl2an 494 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → (𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
43 | 42 | sseq1d 3632 |
. . . . . . . 8
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → ((𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 ↔ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) |
44 | | 2re 11090 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
45 | | 1lt2 11194 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
46 | | expnlbnd 12994 |
. . . . . . . . . . . 12
⊢ ((𝑟 ∈ ℝ+
∧ 2 ∈ ℝ ∧ 1 < 2) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟) |
47 | 44, 45, 46 | mp3an23 1416 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ℝ+
→ ∃𝑛 ∈
ℕ (1 / (2↑𝑛))
< 𝑟) |
48 | 47 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟) |
49 | 39 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ℝ) |
50 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℕ |
51 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
52 | 51 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑛 ∈ ℕ0) |
53 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
54 | 50, 52, 53 | sylancr 695 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℕ) |
55 | 54 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℝ) |
56 | 49, 55 | remulcld 10070 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) ∈ ℝ) |
57 | | fllelt 12598 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ →
((⌊‘(𝑤 ·
(2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1))) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1))) |
59 | 58 | simpld 475 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))) |
60 | | reflcl 12597 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ →
(⌊‘(𝑤 ·
(2↑𝑛))) ∈
ℝ) |
61 | 56, 60 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ) |
62 | 54 | nngt0d 11064 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 0 < (2↑𝑛)) |
63 | | ledivmul2 10902 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘(𝑤
· (2↑𝑛)))
∈ ℝ ∧ 𝑤
∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) →
(((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)))) |
64 | 61, 49, 55, 62, 63 | syl112anc 1330 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)))) |
65 | 59, 64 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤) |
66 | | peano2re 10209 |
. . . . . . . . . . . . . . . 16
⊢
((⌊‘(𝑤
· (2↑𝑛)))
∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ) |
67 | 61, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ) |
68 | 67, 54 | nndivred 11069 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈
ℝ) |
69 | 58 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)) |
70 | | ltmuldiv 10896 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ℝ ∧
((⌊‘(𝑤 ·
(2↑𝑛))) + 1) ∈
ℝ ∧ ((2↑𝑛)
∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
71 | 49, 67, 55, 62, 70 | syl112anc 1330 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
72 | 69, 71 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) |
73 | 49, 68, 72 | ltled 10185 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) |
74 | 61, 54 | nndivred 11069 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ) |
75 | | elicc2 12238 |
. . . . . . . . . . . . . 14
⊢
((((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛)) ∈ ℝ
∧ (((⌊‘(𝑤
· (2↑𝑛))) + 1)
/ (2↑𝑛)) ∈
ℝ) → (𝑤 ∈
(((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))) |
76 | 74, 68, 75 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))) |
77 | 49, 65, 73, 76 | mpbir3and 1245 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
78 | 56 | flcld 12599 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ) |
79 | 14 | dyadval 23360 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘(𝑤
· (2↑𝑛)))
∈ ℤ ∧ 𝑛
∈ ℕ0) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) = 〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉) |
80 | 78, 52, 79 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) = 〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) = ([,]‘〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉)) |
82 | | df-ov 6653 |
. . . . . . . . . . . . 13
⊢
(((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) = ([,]‘〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉) |
83 | 81, 82 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
84 | 77, 83 | eleqtrrd 2704 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛))) |
85 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹:(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) →
𝐹 Fn (ℤ ×
ℕ0)) |
86 | 15, 85 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝐹 Fn (ℤ ×
ℕ0) |
87 | | fnovrn 6809 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn (ℤ ×
ℕ0) ∧ (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ0) →
((⌊‘(𝑤 ·
(2↑𝑛)))𝐹𝑛) ∈ ran 𝐹) |
88 | 86, 87 | mp3an1 1411 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘(𝑤
· (2↑𝑛)))
∈ ℤ ∧ 𝑛
∈ ℕ0) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ ran 𝐹) |
89 | 78, 52, 88 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ ran 𝐹) |
90 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ+) |
91 | 90 | rpred 11872 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ) |
92 | 49, 91 | resubcld 10458 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈ ℝ) |
93 | 92 | rexrd 10089 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈
ℝ*) |
94 | 49, 91 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ) |
95 | 94 | rexrd 10089 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈
ℝ*) |
96 | 74, 91 | readdcld 10069 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟) ∈ ℝ) |
97 | 61 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℂ) |
98 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 1 ∈ ℂ) |
99 | 55 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℂ) |
100 | 54 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ≠ 0) |
101 | 97, 98, 99, 100 | divdird 10839 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛)))) |
102 | 54 | nnrecred 11066 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) ∈ ℝ) |
103 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) < 𝑟) |
104 | 102, 91, 74, 103 | ltadd2dd 10196 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)) |
105 | 101, 104 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)) |
106 | 49, 68, 96, 72, 105 | lttrd 10198 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)) |
107 | 49, 91, 74 | ltsubaddd 10623 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))) |
108 | 106, 107 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))) |
109 | 49, 102 | readdcld 10069 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) ∈ ℝ) |
110 | 74, 49, 102, 65 | leadd1dd 10641 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) ≤ (𝑤 + (1 / (2↑𝑛)))) |
111 | 101, 110 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ≤ (𝑤 + (1 / (2↑𝑛)))) |
112 | 102, 91, 49, 103 | ltadd2dd 10196 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) < (𝑤 + 𝑟)) |
113 | 68, 109, 94, 111, 112 | lelttrd 10195 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟)) |
114 | | iccssioo 12242 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑤 − 𝑟) ∈ ℝ* ∧ (𝑤 + 𝑟) ∈ ℝ*) ∧ ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
115 | 93, 95, 108, 113, 114 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
116 | 83, 115 | eqsstrd 3639 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
117 | | simplrr 801 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴) |
118 | 116, 117 | sstrd 3613 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ⊆ 𝐴) |
119 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) → ([,]‘𝑧) = ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛))) |
120 | 119 | sseq1d 3632 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ⊆ 𝐴)) |
121 | 120 | elrab 3363 |
. . . . . . . . . . . . 13
⊢
(((⌊‘(𝑤
· (2↑𝑛)))𝐹𝑛) ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ ran 𝐹 ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ⊆ 𝐴)) |
122 | 89, 118, 121 | sylanbrc 698 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛) ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) |
123 | | funfvima2 6493 |
. . . . . . . . . . . . 13
⊢ ((Fun [,]
∧ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) →
(((⌊‘(𝑤
· (2↑𝑛)))𝐹𝑛) ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))) |
124 | 12, 24, 123 | mp2an 708 |
. . . . . . . . . . . 12
⊢
(((⌊‘(𝑤
· (2↑𝑛)))𝐹𝑛) ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) |
125 | 122, 124 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) |
126 | | elunii 4441 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈
([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))𝐹𝑛)) ∈ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) |
127 | 84, 125, 126 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) |
128 | 48, 127 | rexlimddv 3035 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) |
129 | 128 | expr 643 |
. . . . . . . 8
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → (((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))) |
130 | 43, 129 | sylbid 230 |
. . . . . . 7
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → ((𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))) |
131 | 130 | rexlimdva 3031 |
. . . . . 6
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → (∃𝑟 ∈ ℝ+
(𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))) |
132 | 35, 131 | mpd 15 |
. . . . 5
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) |
133 | 132 | ex 450 |
. . . 4
⊢ (𝐴 ∈ (topGen‘ran (,))
→ (𝑤 ∈ 𝐴 → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}))) |
134 | 133 | ssrdv 3609 |
. . 3
⊢ (𝐴 ∈ (topGen‘ran (,))
→ 𝐴 ⊆ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴})) |
135 | 29, 134 | eqssd 3620 |
. 2
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴) |
136 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑐 = 𝑎 → ([,]‘𝑐) = ([,]‘𝑎)) |
137 | 136 | sseq1d 3632 |
. . . . . 6
⊢ (𝑐 = 𝑎 → (([,]‘𝑐) ⊆ ([,]‘𝑏) ↔ ([,]‘𝑎) ⊆ ([,]‘𝑏))) |
138 | | equequ1 1952 |
. . . . . 6
⊢ (𝑐 = 𝑎 → (𝑐 = 𝑏 ↔ 𝑎 = 𝑏)) |
139 | 137, 138 | imbi12d 334 |
. . . . 5
⊢ (𝑐 = 𝑎 → ((([,]‘𝑐) ⊆ ([,]‘𝑏) → 𝑐 = 𝑏) ↔ (([,]‘𝑎) ⊆ ([,]‘𝑏) → 𝑎 = 𝑏))) |
140 | 139 | ralbidv 2986 |
. . . 4
⊢ (𝑐 = 𝑎 → (∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑐) ⊆ ([,]‘𝑏) → 𝑐 = 𝑏) ↔ ∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑏) → 𝑎 = 𝑏))) |
141 | 140 | cbvrabv 3199 |
. . 3
⊢ {𝑐 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ∣ ∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑐) ⊆ ([,]‘𝑏) → 𝑐 = 𝑏)} = {𝑎 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ∣ ∀𝑏 ∈ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} (([,]‘𝑎) ⊆ ([,]‘𝑏) → 𝑎 = 𝑏)} |
142 | 13 | a1i 11 |
. . 3
⊢ (𝐴 ∈ (topGen‘ran (,))
→ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ ran 𝐹) |
143 | 14, 141, 142 | dyadmbl 23368 |
. 2
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ∪ ([,] “ {𝑧 ∈ ran 𝐹 ∣ ([,]‘𝑧) ⊆ 𝐴}) ∈ dom vol) |
144 | 135, 143 | eqeltrrd 2702 |
1
⊢ (𝐴 ∈ (topGen‘ran (,))
→ 𝐴 ∈ dom
vol) |