Metamath Proof Explorer

Theorem opnmbllem0

Description: Lemma for ismblfin ; could also be used to shorten proof of opnmbllem . (Contributed by Brendan Leahy, 13-Jul-2018)

Ref Expression
Assertion opnmbllem0 ( 𝐴 ∈ ( topGen β€˜ ran (,) ) β†’ βˆͺ ( [,] β€œ { 𝑧 ∈ ran ( π‘₯ ∈ β„€ , 𝑦 ∈ β„•0 ↦ ⟨ ( π‘₯ / ( 2 ↑ 𝑦 ) ) , ( ( π‘₯ + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ ) ∣ ( [,] β€˜ 𝑧 ) βŠ† 𝐴 } ) = 𝐴 )

Proof

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