| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → ([,]‘𝑧) = ([,]‘𝑤)) |
| 2 | 1 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘𝑤) ⊆ 𝐴)) |
| 3 | 2 | elrab 3692 |
. . . . . 6
⊢ (𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∧ ([,]‘𝑤) ⊆ 𝐴)) |
| 4 | | simprr 773 |
. . . . . . 7
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ⊆ 𝐴) |
| 5 | | fvex 6919 |
. . . . . . . 8
⊢
([,]‘𝑤) ∈
V |
| 6 | 5 | elpw 4604 |
. . . . . . 7
⊢
(([,]‘𝑤)
∈ 𝒫 𝐴 ↔
([,]‘𝑤) ⊆ 𝐴) |
| 7 | 4, 6 | sylibr 234 |
. . . . . 6
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ (𝑤 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∧ ([,]‘𝑤) ⊆ 𝐴)) → ([,]‘𝑤) ∈ 𝒫 𝐴) |
| 8 | 3, 7 | sylan2b 594 |
. . . . 5
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}) → ([,]‘𝑤) ∈ 𝒫 𝐴) |
| 9 | 8 | ralrimiva 3146 |
. . . 4
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ∀𝑤 ∈
{𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴) |
| 10 | | iccf 13488 |
. . . . . 6
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
| 11 | | ffun 6739 |
. . . . . 6
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → Fun [,]) |
| 12 | 10, 11 | ax-mp 5 |
. . . . 5
⊢ Fun
[,] |
| 13 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) |
| 14 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑟 → (𝑥 / (2↑𝑦)) = (𝑟 / (2↑𝑦))) |
| 15 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑟 → (𝑥 + 1) = (𝑟 + 1)) |
| 16 | 15 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑟 → ((𝑥 + 1) / (2↑𝑦)) = ((𝑟 + 1) / (2↑𝑦))) |
| 17 | 14, 16 | opeq12d 4881 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑟 → 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉 = 〈(𝑟 / (2↑𝑦)), ((𝑟 + 1) / (2↑𝑦))〉) |
| 18 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑠 → (2↑𝑦) = (2↑𝑠)) |
| 19 | 18 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑠 → (𝑟 / (2↑𝑦)) = (𝑟 / (2↑𝑠))) |
| 20 | 18 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑠 → ((𝑟 + 1) / (2↑𝑦)) = ((𝑟 + 1) / (2↑𝑠))) |
| 21 | 19, 20 | opeq12d 4881 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑠 → 〈(𝑟 / (2↑𝑦)), ((𝑟 + 1) / (2↑𝑦))〉 = 〈(𝑟 / (2↑𝑠)), ((𝑟 + 1) / (2↑𝑠))〉) |
| 22 | 17, 21 | cbvmpov 7528 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) = (𝑟 ∈ ℤ, 𝑠 ∈ ℕ0 ↦
〈(𝑟 / (2↑𝑠)), ((𝑟 + 1) / (2↑𝑠))〉) |
| 23 | 22 | dyadf 25626 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉):(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ ×
ℝ)) |
| 24 | | frn 6743 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉):(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) → ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⊆ ( ≤ ∩
(ℝ × ℝ))) |
| 25 | 23, 24 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⊆ ( ≤ ∩
(ℝ × ℝ)) |
| 26 | | inss2 4238 |
. . . . . . . . 9
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ ×
ℝ) |
| 27 | | rexpssxrxp 11306 |
. . . . . . . . 9
⊢ (ℝ
× ℝ) ⊆ (ℝ* ×
ℝ*) |
| 28 | 26, 27 | sstri 3993 |
. . . . . . . 8
⊢ ( ≤
∩ (ℝ × ℝ)) ⊆ (ℝ* ×
ℝ*) |
| 29 | 25, 28 | sstri 3993 |
. . . . . . 7
⊢ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ⊆
(ℝ* × ℝ*) |
| 30 | 13, 29 | sstri 3993 |
. . . . . 6
⊢ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ (ℝ* ×
ℝ*) |
| 31 | 10 | fdmi 6747 |
. . . . . 6
⊢ dom [,] =
(ℝ* × ℝ*) |
| 32 | 30, 31 | sseqtrri 4033 |
. . . . 5
⊢ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,] |
| 33 | | funimass4 6973 |
. . . . 5
⊢ ((Fun [,]
∧ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) → (([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴)) |
| 34 | 12, 32, 33 | mp2an 692 |
. . . 4
⊢ (([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∀𝑤 ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} ([,]‘𝑤) ∈ 𝒫 𝐴) |
| 35 | 9, 34 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ([,] “ {𝑧
∈ ran (𝑥 ∈
ℤ, 𝑦 ∈
ℕ0 ↦ 〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴) |
| 36 | | sspwuni 5100 |
. . 3
⊢ (([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝒫 𝐴 ↔ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴) |
| 37 | 35, 36 | sylib 218 |
. 2
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}) ⊆ 𝐴) |
| 38 | | eqid 2737 |
. . . . 5
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 39 | 38 | rexmet 24812 |
. . . 4
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) |
| 40 | | eqid 2737 |
. . . . . 6
⊢
(MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
| 41 | 38, 40 | tgioo 24817 |
. . . . 5
⊢
(topGen‘ran (,)) = (MetOpen‘((abs ∘ − ) ↾
(ℝ × ℝ))) |
| 42 | 41 | mopni2 24506 |
. . . 4
⊢ ((((abs
∘ − ) ↾ (ℝ × ℝ)) ∈
(∞Met‘ℝ) ∧ 𝐴 ∈ (topGen‘ran (,)) ∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ+ (𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴) |
| 43 | 39, 42 | mp3an1 1450 |
. . 3
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → ∃𝑟 ∈ ℝ+
(𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴) |
| 44 | | elssuni 4937 |
. . . . . . . . 9
⊢ (𝐴 ∈ (topGen‘ran (,))
→ 𝐴 ⊆ ∪ (topGen‘ran (,))) |
| 45 | | uniretop 24783 |
. . . . . . . . 9
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 46 | 44, 45 | sseqtrrdi 4025 |
. . . . . . . 8
⊢ (𝐴 ∈ (topGen‘ran (,))
→ 𝐴 ⊆
ℝ) |
| 47 | 46 | sselda 3983 |
. . . . . . 7
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ℝ) |
| 48 | | rpre 13043 |
. . . . . . 7
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
| 49 | 38 | bl2ioo 24813 |
. . . . . . 7
⊢ ((𝑤 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
| 50 | 47, 48, 49 | syl2an 596 |
. . . . . 6
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → (𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) = ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
| 51 | 50 | sseq1d 4015 |
. . . . 5
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → ((𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 ↔ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) |
| 52 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 53 | | 1lt2 12437 |
. . . . . . . . 9
⊢ 1 <
2 |
| 54 | | expnlbnd 14272 |
. . . . . . . . 9
⊢ ((𝑟 ∈ ℝ+
∧ 2 ∈ ℝ ∧ 1 < 2) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟) |
| 55 | 52, 53, 54 | mp3an23 1455 |
. . . . . . . 8
⊢ (𝑟 ∈ ℝ+
→ ∃𝑛 ∈
ℕ (1 / (2↑𝑛))
< 𝑟) |
| 56 | 55 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → ∃𝑛 ∈ ℕ (1 / (2↑𝑛)) < 𝑟) |
| 57 | 47 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ℝ) |
| 58 | | 2nn 12339 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ |
| 59 | | nnnn0 12533 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 60 | 59 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑛 ∈ ℕ0) |
| 61 | | nnexpcl 14115 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
| 62 | 58, 60, 61 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℕ) |
| 63 | 62 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℝ) |
| 64 | 57, 63 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) ∈ ℝ) |
| 65 | | fllelt 13837 |
. . . . . . . . . . . . 13
⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ →
((⌊‘(𝑤 ·
(2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1))) |
| 66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)) ∧ (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1))) |
| 67 | 66 | simpld 494 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛))) |
| 68 | | reflcl 13836 |
. . . . . . . . . . . . 13
⊢ ((𝑤 · (2↑𝑛)) ∈ ℝ →
(⌊‘(𝑤 ·
(2↑𝑛))) ∈
ℝ) |
| 69 | 64, 68 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℝ) |
| 70 | 62 | nngt0d 12315 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 0 < (2↑𝑛)) |
| 71 | | ledivmul2 12147 |
. . . . . . . . . . . 12
⊢
(((⌊‘(𝑤
· (2↑𝑛)))
∈ ℝ ∧ 𝑤
∈ ℝ ∧ ((2↑𝑛) ∈ ℝ ∧ 0 < (2↑𝑛))) →
(((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)))) |
| 72 | 69, 57, 63, 70, 71 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ↔ (⌊‘(𝑤 · (2↑𝑛))) ≤ (𝑤 · (2↑𝑛)))) |
| 73 | 67, 72 | mpbird 257 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤) |
| 74 | | peano2re 11434 |
. . . . . . . . . . . . 13
⊢
((⌊‘(𝑤
· (2↑𝑛)))
∈ ℝ → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ) |
| 75 | 69, 74 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) + 1) ∈ ℝ) |
| 76 | 75, 62 | nndivred 12320 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ∈
ℝ) |
| 77 | 66 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1)) |
| 78 | | ltmuldiv 12141 |
. . . . . . . . . . . . 13
⊢ ((𝑤 ∈ ℝ ∧
((⌊‘(𝑤 ·
(2↑𝑛))) + 1) ∈
ℝ ∧ ((2↑𝑛)
∈ ℝ ∧ 0 < (2↑𝑛))) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
| 79 | 57, 75, 63, 70, 78 | syl112anc 1376 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 · (2↑𝑛)) < ((⌊‘(𝑤 · (2↑𝑛))) + 1) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
| 80 | 77, 79 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) |
| 81 | 57, 76, 80 | ltled 11409 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) |
| 82 | 69, 62 | nndivred 12320 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∈ ℝ) |
| 83 | | elicc2 13452 |
. . . . . . . . . . 11
⊢
((((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛)) ∈ ℝ
∧ (((⌊‘(𝑤
· (2↑𝑛))) + 1)
/ (2↑𝑛)) ∈
ℝ) → (𝑤 ∈
(((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))) |
| 84 | 82, 76, 83 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ↔ (𝑤 ∈ ℝ ∧ ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ≤ 𝑤 ∧ 𝑤 ≤ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))))) |
| 85 | 57, 73, 81, 84 | mpbir3and 1343 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
| 86 | 64 | flcld 13838 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ) |
| 87 | 22 | dyadval 25627 |
. . . . . . . . . . . 12
⊢
(((⌊‘(𝑤
· (2↑𝑛)))
∈ ℤ ∧ 𝑛
∈ ℕ0) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) = 〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉) |
| 88 | 86, 60, 87 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) = 〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉) |
| 89 | 88 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) = ([,]‘〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉)) |
| 90 | | df-ov 7434 |
. . . . . . . . . 10
⊢
(((⌊‘(𝑤
· (2↑𝑛))) /
(2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) = ([,]‘〈((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)), (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))〉) |
| 91 | 89, 90 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)))) |
| 92 | 85, 91 | eleqtrrd 2844 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛))) |
| 93 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉):(ℤ ×
ℕ0)⟶( ≤ ∩ (ℝ × ℝ)) →
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) Fn (ℤ ×
ℕ0)) |
| 94 | 23, 93 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) Fn (ℤ ×
ℕ0) |
| 95 | | fnovrn 7608 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) Fn (ℤ ×
ℕ0) ∧ (⌊‘(𝑤 · (2↑𝑛))) ∈ ℤ ∧ 𝑛 ∈ ℕ0) →
((⌊‘(𝑤 ·
(2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)) |
| 96 | 94, 95 | mp3an1 1450 |
. . . . . . . . . . 11
⊢
(((⌊‘(𝑤
· (2↑𝑛)))
∈ ℤ ∧ 𝑛
∈ ℕ0) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)) |
| 97 | 86, 60, 96 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)) |
| 98 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ+) |
| 99 | 98 | rpred 13077 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑟 ∈ ℝ) |
| 100 | 57, 99 | resubcld 11691 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈ ℝ) |
| 101 | 100 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) ∈
ℝ*) |
| 102 | 57, 99 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈ ℝ) |
| 103 | 102 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + 𝑟) ∈
ℝ*) |
| 104 | 82, 99 | readdcld 11290 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟) ∈ ℝ) |
| 105 | 69 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (⌊‘(𝑤 · (2↑𝑛))) ∈ ℂ) |
| 106 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 1 ∈ ℂ) |
| 107 | 63 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ∈ ℂ) |
| 108 | 62 | nnne0d 12316 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (2↑𝑛) ≠ 0) |
| 109 | 105, 106,
107, 108 | divdird 12081 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) = (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛)))) |
| 110 | 62 | nnrecred 12317 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) ∈ ℝ) |
| 111 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (1 / (2↑𝑛)) < 𝑟) |
| 112 | 110, 99, 82, 111 | ltadd2dd 11420 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)) |
| 113 | 109, 112 | eqbrtrd 5165 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)) |
| 114 | 57, 76, 104, 80, 113 | lttrd 11422 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟)) |
| 115 | 57, 99, 82 | ltsubaddd 11859 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ↔ 𝑤 < (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + 𝑟))) |
| 116 | 114, 115 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))) |
| 117 | 57, 110 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) ∈ ℝ) |
| 118 | 82, 57, 110, 73 | leadd1dd 11877 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) + (1 / (2↑𝑛))) ≤ (𝑤 + (1 / (2↑𝑛)))) |
| 119 | 109, 118 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) ≤ (𝑤 + (1 / (2↑𝑛)))) |
| 120 | 110, 99, 57, 111 | ltadd2dd 11420 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (𝑤 + (1 / (2↑𝑛))) < (𝑤 + 𝑟)) |
| 121 | 76, 117, 102, 119, 120 | lelttrd 11419 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟)) |
| 122 | | iccssioo 13456 |
. . . . . . . . . . . . 13
⊢ ((((𝑤 − 𝑟) ∈ ℝ* ∧ (𝑤 + 𝑟) ∈ ℝ*) ∧ ((𝑤 − 𝑟) < ((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛)) ∧ (((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛)) < (𝑤 + 𝑟))) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
| 123 | 101, 103,
116, 121, 122 | syl22anc 839 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → (((⌊‘(𝑤 · (2↑𝑛))) / (2↑𝑛))[,](((⌊‘(𝑤 · (2↑𝑛))) + 1) / (2↑𝑛))) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
| 124 | 91, 123 | eqsstrd 4018 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ⊆ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟))) |
| 125 | | simplrr 778 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴) |
| 126 | 124, 125 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ⊆ 𝐴) |
| 127 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) → ([,]‘𝑧) = ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛))) |
| 128 | 127 | sseq1d 4015 |
. . . . . . . . . . 11
⊢ (𝑧 = ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) → (([,]‘𝑧) ⊆ 𝐴 ↔ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ⊆ 𝐴)) |
| 129 | 128 | elrab 3692 |
. . . . . . . . . 10
⊢
(((⌊‘(𝑤
· (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} ↔ (((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∧
([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ⊆ 𝐴)) |
| 130 | 97, 126, 129 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}) |
| 131 | | funfvima2 7251 |
. . . . . . . . . 10
⊢ ((Fun [,]
∧ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴} ⊆ dom [,]) →
(((⌊‘(𝑤
· (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}))) |
| 132 | 12, 32, 131 | mp2an 692 |
. . . . . . . . 9
⊢
(((⌊‘(𝑤
· (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛) ∈ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴} → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴})) |
| 133 | 130, 132 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴})) |
| 134 | | elunii 4912 |
. . . . . . . 8
⊢ ((𝑤 ∈
([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ∧ ([,]‘((⌊‘(𝑤 · (2↑𝑛)))(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉)𝑛)) ∈ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴})) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴})) |
| 135 | 92, 133, 134 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) ∧ (𝑛 ∈ ℕ ∧ (1 / (2↑𝑛)) < 𝑟)) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴})) |
| 136 | 56, 135 | rexlimddv 3161 |
. . . . . 6
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ (𝑟 ∈ ℝ+ ∧ ((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴)) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴})) |
| 137 | 136 | expr 456 |
. . . . 5
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → (((𝑤 − 𝑟)(,)(𝑤 + 𝑟)) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴}))) |
| 138 | 51, 137 | sylbid 240 |
. . . 4
⊢ (((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) ∧ 𝑟 ∈ ℝ+) → ((𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴}))) |
| 139 | 138 | rexlimdva 3155 |
. . 3
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → (∃𝑟 ∈ ℝ+
(𝑤(ball‘((abs ∘
− ) ↾ (ℝ × ℝ)))𝑟) ⊆ 𝐴 → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴}))) |
| 140 | 43, 139 | mpd 15 |
. 2
⊢ ((𝐴 ∈ (topGen‘ran (,))
∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ∪ ([,]
“ {𝑧 ∈ ran
(𝑥 ∈ ℤ, 𝑦 ∈ ℕ0
↦ 〈(𝑥 /
(2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣
([,]‘𝑧) ⊆ 𝐴})) |
| 141 | 37, 140 | eqelssd 4005 |
1
⊢ (𝐴 ∈ (topGen‘ran (,))
→ ∪ ([,] “ {𝑧 ∈ ran (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) ∣ ([,]‘𝑧) ⊆ 𝐴}) = 𝐴) |