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 / 𝑅 ) )