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=r2x|b0r1nk1n|xrkmodr=bn1r
snml.f F=nk1n|ARkmodR=Bn
Assertion snmlflim ASRB0R1F1R

Proof

Step Hyp Ref Expression
1 snml.s S=r2x|b0r1nk1n|xrkmodr=bn1r
2 snml.f F=nk1n|ARkmodR=Bn
3 1 snmlval ASRR2Ab0R1nk1n|ARkmodR=bn1R
4 3 simp3bi ASRb0R1nk1n|ARkmodR=bn1R
5 eqeq2 b=BARkmodR=bARkmodR=B
6 5 rabbidv b=Bk1n|ARkmodR=b=k1n|ARkmodR=B
7 6 fveq2d b=Bk1n|ARkmodR=b=k1n|ARkmodR=B
8 7 oveq1d b=Bk1n|ARkmodR=bn=k1n|ARkmodR=Bn
9 8 mpteq2dv b=Bnk1n|ARkmodR=bn=nk1n|ARkmodR=Bn
10 9 2 eqtr4di b=Bnk1n|ARkmodR=bn=F
11 10 breq1d b=Bnk1n|ARkmodR=bn1RF1R
12 11 rspccva b0R1nk1n|ARkmodR=bn1RB0R1F1R
13 4 12 sylan ASRB0R1F1R