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 2 x | b 0 r 1 n k 1 n | x r k mod r = b n 1 r
snml.f F = n k 1 n | A R k mod R = B n
Assertion snmlflim A S R B 0 R 1 F 1 R

Proof

Step Hyp Ref Expression
1 snml.s S = r 2 x | b 0 r 1 n k 1 n | x r k mod r = b n 1 r
2 snml.f F = n k 1 n | A R k mod R = B n
3 1 snmlval A S R R 2 A b 0 R 1 n k 1 n | A R k mod R = b n 1 R
4 3 simp3bi A S R b 0 R 1 n k 1 n | A R k mod R = b n 1 R
5 eqeq2 b = B A R k mod R = b A R k mod R = B
6 5 rabbidv b = B k 1 n | A R k mod R = b = k 1 n | A R k mod R = B
7 6 fveq2d b = B k 1 n | A R k mod R = b = k 1 n | A R k mod R = B
8 7 oveq1d b = B k 1 n | A R k mod R = b n = k 1 n | A R k mod R = B n
9 8 mpteq2dv b = B n k 1 n | A R k mod R = b n = n k 1 n | A R k mod R = B n
10 9 2 eqtr4di b = B n k 1 n | A R k mod R = b n = F
11 10 breq1d b = B n k 1 n | A R k mod R = b n 1 R F 1 R
12 11 rspccva b 0 R 1 n k 1 n | A R k mod R = b n 1 R B 0 R 1 F 1 R
13 4 12 sylan A S R B 0 R 1 F 1 R