Metamath Proof Explorer

Theorem snmlval

Description: The property " A is simply normal in base R ". A number is simply normal if each digit 0 <_ b < R occurs in the base- R digit string of A with frequency 1 / R (which is consistent with the expectation in an infinite random string of numbers selected from 0 ... R - 1 ). (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypothesis snml.s ⊢ 𝑆 = ( 𝑟 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑟 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) } )
Assertion snmlval ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ↔ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 snml.s ⊢ 𝑆 = ( 𝑟 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑟 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) } )
2 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 − 1 ) = ( 𝑅 − 1 ) )
3 2 oveq2d ⊢ ( 𝑟 = 𝑅 → ( 0 ... ( 𝑟 − 1 ) ) = ( 0 ... ( 𝑅 − 1 ) ) )
4 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑ 𝑘 ) = ( 𝑅 ↑ 𝑘 ) )
5 4 oveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) = ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) )
6 id ⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
7 5 6 oveq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) = ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) )
8 7 fveqeq2d ⊢ ( 𝑟 = 𝑅 → ( ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 ↔ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 ) )
9 8 rabbidv ⊢ ( 𝑟 = 𝑅 → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } = { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } )
10 9 fveq2d ⊢ ( 𝑟 = 𝑅 → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) = ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) )
11 10 oveq1d ⊢ ( 𝑟 = 𝑅 → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) = ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) )
12 11 mpteq2dv ⊢ ( 𝑟 = 𝑅 → ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) )
13 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 1 / 𝑟 ) = ( 1 / 𝑅 ) )
14 12 13 breq12d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )
15 3 14 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑏 ∈ ( 0 ... ( 𝑟 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) ↔ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )
16 15 rabbidv ⊢ ( 𝑟 = 𝑅 → { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑟 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟 ↑ 𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) } = { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) } )
17 reex ⊢ ℝ ∈ V
18 17 rabex ⊢ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) } ∈ V
19 16 1 18 fvmpt ⊢ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑆 ‘ 𝑅 ) = { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) } )
20 19 eleq2d ⊢ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ↔ 𝐴 ∈ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) } ) )
21 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) = ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) )
22 21 fvoveq1d ⊢ ( 𝑥 = 𝐴 → ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) )
23 22 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 ↔ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 ) )
24 23 rabbidv ⊢ ( 𝑥 = 𝐴 → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } = { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } )
25 24 fveq2d ⊢ ( 𝑥 = 𝐴 → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) = ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) )
26 25 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) = ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) )
27 26 mpteq2dv ⊢ ( 𝑥 = 𝐴 → ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) )
28 27 breq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ↔ ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )
29 28 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ↔ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )
30 29 elrab ⊢ ( 𝐴 ∈ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) } ↔ ( 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )
31 20 30 bitrdi ⊢ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ↔ ( 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) ) )
32 31 pm5.32i ⊢ ( ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) ) )
33 1 dmmptss ⊢ dom 𝑆 ⊆ ( ℤ≥ ‘ 2 )
34 elfvdm ⊢ ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) → 𝑅 ∈ dom 𝑆 )
35 33 34 sseldi ⊢ ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) → 𝑅 ∈ ( ℤ≥ ‘ 2 ) )
36 35 pm4.71ri ⊢ ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ↔ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ) )
37 3anass ⊢ ( ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) ↔ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ ( 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) ) )
38 32 36 37 3bitr4i ⊢ ( 𝐴 ∈ ( 𝑆 ‘ 𝑅 ) ↔ ( 𝑅 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )