Metamath Proof Explorer


Theorem snmlflim

Description: If A is simply normal, then the function F of relative density of B in the digit string converges to 1 / R , i.e. the set of occurrences of B in the digit string has natural density 1 / R . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses snml.s 𝑆 = ( 𝑟 ∈ ( ℤ ‘ 2 ) ↦ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑟 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) } )
snml.f 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
Assertion snmlflim ( ( 𝐴 ∈ ( 𝑆𝑅 ) ∧ 𝐵 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝐹 ⇝ ( 1 / 𝑅 ) )

Proof

Step Hyp Ref Expression
1 snml.s 𝑆 = ( 𝑟 ∈ ( ℤ ‘ 2 ) ↦ { 𝑥 ∈ ℝ ∣ ∀ 𝑏 ∈ ( 0 ... ( 𝑟 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝑥 · ( 𝑟𝑘 ) ) mod 𝑟 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑟 ) } )
2 snml.f 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
3 1 snmlval ( 𝐴 ∈ ( 𝑆𝑅 ) ↔ ( 𝑅 ∈ ( ℤ ‘ 2 ) ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ) )
4 3 simp3bi ( 𝐴 ∈ ( 𝑆𝑅 ) → ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) )
5 eqeq2 ( 𝑏 = 𝐵 → ( ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 ↔ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝐵 ) )
6 5 rabbidv ( 𝑏 = 𝐵 → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } = { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝐵 } )
7 6 fveq2d ( 𝑏 = 𝐵 → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) = ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) )
8 7 oveq1d ( 𝑏 = 𝐵 → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) = ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
9 8 mpteq2dv ( 𝑏 = 𝐵 → ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) ) )
10 9 2 eqtr4di ( 𝑏 = 𝐵 → ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) = 𝐹 )
11 10 breq1d ( 𝑏 = 𝐵 → ( ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ↔ 𝐹 ⇝ ( 1 / 𝑅 ) ) )
12 11 rspccva ( ( ∀ 𝑏 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅𝑘 ) ) mod 𝑅 ) ) = 𝑏 } ) / 𝑛 ) ) ⇝ ( 1 / 𝑅 ) ∧ 𝐵 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝐹 ⇝ ( 1 / 𝑅 ) )
13 4 12 sylan ( ( 𝐴 ∈ ( 𝑆𝑅 ) ∧ 𝐵 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝐹 ⇝ ( 1 / 𝑅 ) )