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 
|- S = ( r e. ( ZZ>= ` 2 ) |-> { x e. RR | A. b e. ( 0 ... ( r - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } ) / n ) ) ~~> ( 1 / r ) } )
snml.f 
|- F = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) )
Assertion snmlflim 
|- ( ( A e. ( S ` R ) /\ B e. ( 0 ... ( R - 1 ) ) ) -> F ~~> ( 1 / R ) )

Proof

Step Hyp Ref Expression
1 snml.s 
 |-  S = ( r e. ( ZZ>= ` 2 ) |-> { x e. RR | A. b e. ( 0 ... ( r - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } ) / n ) ) ~~> ( 1 / r ) } )
2 snml.f 
 |-  F = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) )
3 1 snmlval 
 |-  ( A e. ( S ` R ) <-> ( R e. ( ZZ>= ` 2 ) /\ A e. RR /\ A. b e. ( 0 ... ( R - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) ) )
4 3 simp3bi 
 |-  ( A e. ( S ` R ) -> A. b e. ( 0 ... ( R - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) )
5 eqeq2 
 |-  ( b = B -> ( ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b <-> ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B ) )
6 5 rabbidv 
 |-  ( b = B -> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } = { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } )
7 6 fveq2d 
 |-  ( b = B -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) = ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) )
8 7 oveq1d 
 |-  ( b = B -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) = ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) )
9 8 mpteq2dv 
 |-  ( b = B -> ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) ) )
10 9 2 eqtr4di 
 |-  ( b = B -> ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) = F )
11 10 breq1d 
 |-  ( b = B -> ( ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) <-> F ~~> ( 1 / R ) ) )
12 11 rspccva 
 |-  ( ( A. b e. ( 0 ... ( R - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) /\ B e. ( 0 ... ( R - 1 ) ) ) -> F ~~> ( 1 / R ) )
13 4 12 sylan 
 |-  ( ( A e. ( S ` R ) /\ B e. ( 0 ... ( R - 1 ) ) ) -> F ~~> ( 1 / R ) )