This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opnmbllem

Description: Lemma for opnmbl . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
Assertion opnmbllem ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 fveq2 ⊢ ( 𝑧 = 𝑤 → ( [,] ‘ 𝑧 ) = ( [,] ‘ 𝑤 ) )
3 2 sseq1d ⊢ ( 𝑧 = 𝑤 → ( ( [,] ‘ 𝑧 ) ⊆ 𝐴 ↔ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) )
4 3 elrab ⊢ ( 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ↔ ( 𝑤 ∈ ran 𝐹 ∧ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) )
5 simprr ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ ( 𝑤 ∈ ran 𝐹 ∧ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) ) → ( [,] ‘ 𝑤 ) ⊆ 𝐴 )
6 fvex ⊢ ( [,] ‘ 𝑤 ) ∈ V
7 6 elpw ⊢ ( ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 ↔ ( [,] ‘ 𝑤 ) ⊆ 𝐴 )
8 5 7 sylibr ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ ( 𝑤 ∈ ran 𝐹 ∧ ( [,] ‘ 𝑤 ) ⊆ 𝐴 ) ) → ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
9 4 8 sylan2b ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) → ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
10 9 ralrimiva ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∀ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
11 iccf ⊢ [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
12 ffun ⊢ ( [,] : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ* → Fun [,] )
13 11 12 ax-mp ⊢ Fun [,]
14 ssrab2 ⊢ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ ran 𝐹
15 1 dyadf ⊢ 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )
16 frn ⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) ) )
17 15 16 ax-mp ⊢ ran 𝐹 ⊆ ( ≤ ∩ ( ℝ × ℝ ) )
18 inss2 ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ × ℝ )
19 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
20 18 19 sstri ⊢ ( ≤ ∩ ( ℝ × ℝ ) ) ⊆ ( ℝ* × ℝ* )
21 17 20 sstri ⊢ ran 𝐹 ⊆ ( ℝ* × ℝ* )
22 14 21 sstri ⊢ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ ( ℝ* × ℝ* )
23 11 fdmi ⊢ dom [,] = ( ℝ* × ℝ* )
24 22 23 sseqtrri ⊢ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ dom [,]
25 funimass4 ⊢ ( ( Fun [,] ∧ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ dom [,] ) → ( ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 ↔ ∀ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 ) )
26 13 24 25 mp2an ⊢ ( ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 ↔ ∀ 𝑤 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( [,] ‘ 𝑤 ) ∈ 𝒫 𝐴 )
27 10 26 sylibr ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 )
28 sspwuni ⊢ ( ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝒫 𝐴 ↔ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝐴 )
29 27 28 sylib ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ⊆ 𝐴 )
30 eqid ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
31 30 rexmet ⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
32 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
33 30 32 tgioo ⊢ ( topGen ‘ ran (,) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
34 33 mopni2 ⊢ ( ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) ∧ 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 )
35 31 34 mp3an1 ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) → ∃ 𝑟 ∈ ℝ+ ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 )
36 elssuni ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ⊆ ∪ ( topGen ‘ ran (,) ) )
37 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
38 36 37 sseqtrrdi ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ⊆ ℝ )
39 38 sselda ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ℝ )
40 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
41 30 bl2ioo ⊢ ( ( 𝑤 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
42 39 40 41 syl2an ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) = ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
43 42 sseq1d ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 ↔ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) )
44 2re ⊢ 2 ∈ ℝ
45 1lt2 ⊢ 1 < 2
46 expnlbnd ⊢ ( ( 𝑟 ∈ ℝ+ ∧ 2 ∈ ℝ ∧ 1 < 2 ) → ∃ 𝑛 ∈ ℕ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
47 44 45 46 mp3an23 ⊢ ( 𝑟 ∈ ℝ+ → ∃ 𝑛 ∈ ℕ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
48 47 ad2antrl ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) → ∃ 𝑛 ∈ ℕ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
49 39 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ∈ ℝ )
50 2nn ⊢ 2 ∈ ℕ
51 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
52 51 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑛 ∈ ℕ0 )
53 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
54 50 52 53 sylancr ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ∈ ℕ )
55 54 nnred ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ∈ ℝ )
56 49 55 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∈ ℝ )
57 fllelt ⊢ ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∧ ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ) )
58 56 57 syl ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∧ ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ) )
59 58 simpld ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) )
60 reflcl ⊢ ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
61 56 60 syl ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
62 54 nngt0d ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 0 < ( 2 ↑ 𝑛 ) )
63 ledivmul2 ⊢ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ ∧ 𝑤 ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 ↔ ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) )
64 61 49 55 62 63 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 ↔ ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) )
65 59 64 mpbird ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 )
66 peano2re ⊢ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ∈ ℝ )
67 61 66 syl ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ∈ ℝ )
68 67 54 nndivred ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
69 58 simprd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) )
70 ltmuldiv ⊢ ( ( 𝑤 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ∈ ℝ ∧ ( ( 2 ↑ 𝑛 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝑛 ) ) ) → ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ↔ 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
71 49 67 55 62 70 syl112anc ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( 𝑤 · ( 2 ↑ 𝑛 ) ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) ↔ 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
72 69 71 mpbid ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) )
73 49 68 72 ltled ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ≤ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) )
74 61 54 nndivred ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
75 elicc2 ⊢ ( ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ∧ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ∈ ℝ ) → ( 𝑤 ∈ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 ∧ 𝑤 ≤ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) )
76 74 68 75 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 ∈ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ↔ ( 𝑤 ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ≤ 𝑤 ∧ 𝑤 ≤ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ) )
77 49 65 73 76 mpbir3and ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ∈ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
78 56 flcld ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℤ )
79 1 dyadval ⊢ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) = ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ )
80 78 52 79 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) = ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ )
81 80 fveq2d ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) = ( [,] ‘ ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ ) )
82 df-ov ⊢ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) = ( [,] ‘ ⟨ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) , ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ⟩ )
83 81 82 eqtr4di ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) = ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
84 77 83 eleqtrrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ∈ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) )
85 fveq2 ⊢ ( 𝑧 = ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) → ( [,] ‘ 𝑧 ) = ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) )
86 85 sseq1d ⊢ ( 𝑧 = ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) → ( ( [,] ‘ 𝑧 ) ⊆ 𝐴 ↔ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ⊆ 𝐴 ) )
87 ffn ⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ( ℤ × ℕ0 ) )
88 15 87 ax-mp ⊢ 𝐹 Fn ( ℤ × ℕ0 )
89 fnovrn ⊢ ( ( 𝐹 Fn ( ℤ × ℕ0 ) ∧ ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ ran 𝐹 )
90 88 78 52 89 mp3an2i ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ ran 𝐹 )
91 simplrl ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑟 ∈ ℝ+ )
92 91 rpred ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑟 ∈ ℝ )
93 49 92 resubcld ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 − 𝑟 ) ∈ ℝ )
94 93 rexrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 − 𝑟 ) ∈ ℝ* )
95 49 92 readdcld ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + 𝑟 ) ∈ ℝ )
96 95 rexrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + 𝑟 ) ∈ ℝ* )
97 74 92 readdcld ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) ∈ ℝ )
98 61 recnd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) ∈ ℂ )
99 1cnd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 1 ∈ ℂ )
100 55 recnd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ∈ ℂ )
101 54 nnne0d ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 2 ↑ 𝑛 ) ≠ 0 )
102 98 99 100 101 divdird ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) = ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + ( 1 / ( 2 ↑ 𝑛 ) ) ) )
103 54 nnrecred ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 1 / ( 2 ↑ 𝑛 ) ) ∈ ℝ )
104 simprr ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 )
105 103 92 74 104 ltadd2dd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + ( 1 / ( 2 ↑ 𝑛 ) ) ) < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) )
106 102 105 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) )
107 49 68 97 72 106 lttrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) )
108 49 92 74 ltsubaddd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( 𝑤 − 𝑟 ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ↔ 𝑤 < ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + 𝑟 ) ) )
109 107 108 mpbird ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 − 𝑟 ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) )
110 49 103 readdcld ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) ∈ ℝ )
111 74 49 103 65 leadd1dd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) + ( 1 / ( 2 ↑ 𝑛 ) ) ) ≤ ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) )
112 102 111 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ≤ ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) )
113 103 92 49 104 ltadd2dd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( 𝑤 + ( 1 / ( 2 ↑ 𝑛 ) ) ) < ( 𝑤 + 𝑟 ) )
114 68 110 95 112 113 lelttrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) < ( 𝑤 + 𝑟 ) )
115 iccssioo ⊢ ( ( ( ( 𝑤 − 𝑟 ) ∈ ℝ* ∧ ( 𝑤 + 𝑟 ) ∈ ℝ* ) ∧ ( ( 𝑤 − 𝑟 ) < ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) ∧ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) < ( 𝑤 + 𝑟 ) ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ⊆ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
116 94 96 109 114 115 syl22anc ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) / ( 2 ↑ 𝑛 ) ) [,] ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) + 1 ) / ( 2 ↑ 𝑛 ) ) ) ⊆ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
117 83 116 eqsstrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ⊆ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) )
118 simplrr ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 )
119 117 118 sstrd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ⊆ 𝐴 )
120 86 90 119 elrabd ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } )
121 funfvima2 ⊢ ( ( Fun [,] ∧ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ dom [,] ) → ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
122 13 24 121 mp2an ⊢ ( ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
123 120 122 syl ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
124 elunii ⊢ ( ( 𝑤 ∈ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∧ ( [,] ‘ ( ( ⌊ ‘ ( 𝑤 · ( 2 ↑ 𝑛 ) ) ) 𝐹 𝑛 ) ) ∈ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) → 𝑤 ∈ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
125 84 123 124 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 1 / ( 2 ↑ 𝑛 ) ) < 𝑟 ) ) → 𝑤 ∈ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
126 48 125 rexlimddv ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 ) ) → 𝑤 ∈ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
127 126 expr ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( ( 𝑤 − 𝑟 ) (,) ( 𝑤 + 𝑟 ) ) ⊆ 𝐴 → 𝑤 ∈ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
128 43 127 sylbid ⊢ ( ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 → 𝑤 ∈ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
129 128 rexlimdva ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝑤 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑟 ) ⊆ 𝐴 → 𝑤 ∈ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ) )
130 35 129 mpd ⊢ ( ( 𝐴 ∈ ( topGen ‘ ran (,) ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) )
131 29 130 eqelssd ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) = 𝐴 )
132 fveq2 ⊢ ( 𝑐 = 𝑎 → ( [,] ‘ 𝑐 ) = ( [,] ‘ 𝑎 ) )
133 132 sseq1d ⊢ ( 𝑐 = 𝑎 → ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) ↔ ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) ) )
134 equequ1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 = 𝑏 ↔ 𝑎 = 𝑏 ) )
135 133 134 imbi12d ⊢ ( 𝑐 = 𝑎 → ( ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑐 = 𝑏 ) ↔ ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
136 135 ralbidv ⊢ ( 𝑐 = 𝑎 → ( ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑐 = 𝑏 ) ↔ ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
137 136 cbvrabv ⊢ { 𝑐 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ∣ ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑐 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑐 = 𝑏 ) } = { 𝑎 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ∣ ∀ 𝑏 ∈ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ( ( [,] ‘ 𝑎 ) ⊆ ( [,] ‘ 𝑏 ) → 𝑎 = 𝑏 ) }
138 14 a1i ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ⊆ ran 𝐹 )
139 1 137 138 dyadmbl ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → ∪ ( [,] “ { 𝑧 ∈ ran 𝐹 ∣ ( [,] ‘ 𝑧 ) ⊆ 𝐴 } ) ∈ dom vol )
140 131 139 eqeltrrd ⊢ ( 𝐴 ∈ ( topGen ‘ ran (,) ) → 𝐴 ∈ dom vol )