Metamath Proof Explorer

Theorem dya2iocival

Description: The function I returns closed-below open-above dyadic rational intervals covering the real line. This is the same construction as in dyadmbl . (Contributed by Thierry Arnoux, 24-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
Assertion dya2iocival ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 𝐼 𝑁 ) = ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 oveq1 ⊢ ( 𝑢 = 𝑋 → ( 𝑢 / ( 2 ↑ 𝑚 ) ) = ( 𝑋 / ( 2 ↑ 𝑚 ) ) )
4 oveq1 ⊢ ( 𝑢 = 𝑋 → ( 𝑢 + 1 ) = ( 𝑋 + 1 ) )
5 4 oveq1d ⊢ ( 𝑢 = 𝑋 → ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑚 ) ) = ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑚 ) ) )
6 3 5 oveq12d ⊢ ( 𝑢 = 𝑋 → ( ( 𝑢 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑋 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑚 ) ) ) )
7 oveq2 ⊢ ( 𝑚 = 𝑁 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑁 ) )
8 7 oveq2d ⊢ ( 𝑚 = 𝑁 → ( 𝑋 / ( 2 ↑ 𝑚 ) ) = ( 𝑋 / ( 2 ↑ 𝑁 ) ) )
9 7 oveq2d ⊢ ( 𝑚 = 𝑁 → ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑚 ) ) = ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) )
10 8 9 oveq12d ⊢ ( 𝑚 = 𝑁 → ( ( 𝑋 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
11 oveq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 / ( 2 ↑ 𝑚 ) ) = ( 𝑥 / ( 2 ↑ 𝑚 ) ) )
12 oveq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 + 1 ) = ( 𝑥 + 1 ) )
13 12 oveq1d ⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑚 ) ) = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) )
14 11 13 oveq12d ⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑥 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) ) )
15 oveq2 ⊢ ( 𝑚 = 𝑛 → ( 2 ↑ 𝑚 ) = ( 2 ↑ 𝑛 ) )
16 15 oveq2d ⊢ ( 𝑚 = 𝑛 → ( 𝑥 / ( 2 ↑ 𝑚 ) ) = ( 𝑥 / ( 2 ↑ 𝑛 ) ) )
17 15 oveq2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) = ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) )
18 16 17 oveq12d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑥 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑚 ) ) ) = ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
19 14 18 cbvmpov ⊢ ( 𝑢 ∈ ℤ , 𝑚 ∈ ℤ ↦ ( ( 𝑢 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑚 ) ) ) ) = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
20 2 19 eqtr4i ⊢ 𝐼 = ( 𝑢 ∈ ℤ , 𝑚 ∈ ℤ ↦ ( ( 𝑢 / ( 2 ↑ 𝑚 ) ) [,) ( ( 𝑢 + 1 ) / ( 2 ↑ 𝑚 ) ) ) )
21 ovex ⊢ ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ V
22 6 10 20 21 ovmpo ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑋 𝐼 𝑁 ) = ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
23 22 ancoms ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 𝐼 𝑁 ) = ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) )