Metamath Proof Explorer

Theorem dya2iocbrsiga

Description: Dyadic intervals are Borel sets of RR . (Contributed by Thierry Arnoux, 22-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 1 2 dya2iocival ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 𝐼 𝑁 ) = ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
4 mnfxr ⊢ -∞ ∈ ℝ*
5 4 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → -∞ ∈ ℝ* )
6 simpr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → 𝑋 ∈ ℤ )
7 6 zred ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → 𝑋 ∈ ℝ )
8 2rp ⊢ 2 ∈ ℝ+
9 8 a1i ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → 2 ∈ ℝ+ )
10 simpl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → 𝑁 ∈ ℤ )
11 9 10 rpexpcld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 2 ↑ 𝑁 ) ∈ ℝ+ )
12 7 11 rerpdivcld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
13 12 rexrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 / ( 2 ↑ 𝑁 ) ) ∈ ℝ* )
14 1red ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → 1 ∈ ℝ )
15 7 14 readdcld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 + 1 ) ∈ ℝ )
16 15 11 rerpdivcld ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
17 16 rexrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ* )
18 mnflt ⊢ ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) ∈ ℝ → -∞ < ( 𝑋 / ( 2 ↑ 𝑁 ) ) )
19 12 18 syl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → -∞ < ( 𝑋 / ( 2 ↑ 𝑁 ) ) )
20 difioo ⊢ ( ( ( -∞ ∈ ℝ* ∧ ( 𝑋 / ( 2 ↑ 𝑁 ) ) ∈ ℝ* ∧ ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ∈ ℝ* ) ∧ -∞ < ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) → ( ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∖ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ) = ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
21 5 13 17 19 20 syl31anc ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∖ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ) = ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) )
22 brsigarn ⊢ 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ )
23 elrnsiga ⊢ ( 𝔅ℝ ∈ ( sigAlgebra ‘ ℝ ) → 𝔅ℝ ∈ ∪ ran sigAlgebra )
24 22 23 ax-mp ⊢ 𝔅ℝ ∈ ∪ ran sigAlgebra
25 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
26 iooretop ⊢ ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ ( topGen ‘ ran (,) )
27 elsigagen ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ ( topGen ‘ ran (,) ) ) → ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
28 25 26 27 mp2an ⊢ ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) )
29 df-brsiga ⊢ 𝔅ℝ = ( sigaGen ‘ ( topGen ‘ ran (,) ) )
30 28 29 eleqtrri ⊢ ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ 𝔅ℝ
31 iooretop ⊢ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ∈ ( topGen ‘ ran (,) )
32 elsigagen ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ∈ ( topGen ‘ ran (,) ) ) → ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) ) )
33 25 31 32 mp2an ⊢ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ∈ ( sigaGen ‘ ( topGen ‘ ran (,) ) )
34 33 29 eleqtrri ⊢ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ∈ 𝔅ℝ
35 difelsiga ⊢ ( ( 𝔅ℝ ∈ ∪ ran sigAlgebra ∧ ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ 𝔅ℝ ∧ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ∈ 𝔅ℝ ) → ( ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∖ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ) ∈ 𝔅ℝ )
36 24 30 34 35 mp3an ⊢ ( ( -∞ (,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∖ ( -∞ (,) ( 𝑋 / ( 2 ↑ 𝑁 ) ) ) ) ∈ 𝔅ℝ
37 21 36 eqeltrrdi ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( ( 𝑋 / ( 2 ↑ 𝑁 ) ) [,) ( ( 𝑋 + 1 ) / ( 2 ↑ 𝑁 ) ) ) ∈ 𝔅ℝ )
38 3 37 eqeltrd ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ ℤ ) → ( 𝑋 𝐼 𝑁 ) ∈ 𝔅ℝ )