Theorem snmlfval

Description: The function F from snmlval maps N to the relative density of B in the first N digits of the digit string of A in base R . (Contributed by Mario Carneiro, 6-Apr-2015)

	Ref	Expression
Hypothesis	snmlff.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
Assertion	snmlfval	⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑁 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		snmlff.f	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) )
2		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
3	2	rabeqdv	⊢ ( 𝑛 = 𝑁 → { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } = { 𝑘 ∈ ( 1 ... 𝑁 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } )
4	3	fveq2d	⊢ ( 𝑛 = 𝑁 → ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) = ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑁 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) )
5		id	⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
6	4 5	oveq12d	⊢ ( 𝑛 = 𝑁 → ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑛 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑛 ) = ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑁 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑁 ) )
7		ovex	⊢ ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑁 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑁 ) ∈ V
8	6 1 7	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( 𝐹 ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑘 ∈ ( 1 ... 𝑁 ) ∣ ( ⌊ ‘ ( ( 𝐴 · ( 𝑅 ↑ 𝑘 ) ) mod 𝑅 ) ) = 𝐵 } ) / 𝑁 ) )