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 e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) )
Assertion	snmlfval	|- ( N e. NN -> ( F ` N ) = ( ( # ` { k e. ( 1 ... N ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / N ) )

Proof

Step	Hyp	Ref	Expression
1		snmlff.f	|- F = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) )
2		oveq2	|- ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
3	2	rabeqdv	|- ( n = N -> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } = { k e. ( 1 ... N ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } )
4	3	fveq2d	|- ( n = N -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) = ( # ` { k e. ( 1 ... N ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) )
5		id	|- ( n = N -> n = N )
6	4 5	oveq12d	|- ( n = N -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) = ( ( # ` { k e. ( 1 ... N ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / N ) )
7		ovex	|- ( ( # ` { k e. ( 1 ... N ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / N ) e. _V
8	6 1 7	fvmpt	|- ( N e. NN -> ( F ` N ) = ( ( # ` { k e. ( 1 ... N ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / N ) )