Metamath Proof Explorer


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 F = n k 1 n | A R k mod R = B n
Assertion snmlfval N F N = k 1 N | A R k mod R = B N

Proof

Step Hyp Ref Expression
1 snmlff.f F = n k 1 n | A R k mod R = B n
2 oveq2 n = N 1 n = 1 N
3 2 rabeqdv n = N k 1 n | A R k mod R = B = k 1 N | A R k mod R = B
4 3 fveq2d n = N k 1 n | A R k mod R = B = k 1 N | A R k mod R = B
5 id n = N n = N
6 4 5 oveq12d n = N k 1 n | A R k mod R = B n = k 1 N | A R k mod R = B N
7 ovex k 1 N | A R k mod R = B N V
8 6 1 7 fvmpt N F N = k 1 N | A R k mod R = B N