Metamath Proof Explorer


Theorem snmlval

Description: The property " A is simply normal in base R ". A number is simply normal if each digit 0 <_ b < R occurs in the base- R digit string of A with frequency 1 / R (which is consistent with the expectation in an infinite random string of numbers selected from 0 ... R - 1 ). (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypothesis snml.s S=r2x|b0r1nk1n|xrkmodr=bn1r
Assertion snmlval ASRR2Ab0R1nk1n|ARkmodR=bn1R

Proof

Step Hyp Ref Expression
1 snml.s S=r2x|b0r1nk1n|xrkmodr=bn1r
2 oveq1 r=Rr1=R1
3 2 oveq2d r=R0r1=0R1
4 oveq1 r=Rrk=Rk
5 4 oveq2d r=Rxrk=xRk
6 id r=Rr=R
7 5 6 oveq12d r=Rxrkmodr=xRkmodR
8 7 fveqeq2d r=Rxrkmodr=bxRkmodR=b
9 8 rabbidv r=Rk1n|xrkmodr=b=k1n|xRkmodR=b
10 9 fveq2d r=Rk1n|xrkmodr=b=k1n|xRkmodR=b
11 10 oveq1d r=Rk1n|xrkmodr=bn=k1n|xRkmodR=bn
12 11 mpteq2dv r=Rnk1n|xrkmodr=bn=nk1n|xRkmodR=bn
13 oveq2 r=R1r=1R
14 12 13 breq12d r=Rnk1n|xrkmodr=bn1rnk1n|xRkmodR=bn1R
15 3 14 raleqbidv r=Rb0r1nk1n|xrkmodr=bn1rb0R1nk1n|xRkmodR=bn1R
16 15 rabbidv r=Rx|b0r1nk1n|xrkmodr=bn1r=x|b0R1nk1n|xRkmodR=bn1R
17 reex V
18 17 rabex x|b0R1nk1n|xRkmodR=bn1RV
19 16 1 18 fvmpt R2SR=x|b0R1nk1n|xRkmodR=bn1R
20 19 eleq2d R2ASRAx|b0R1nk1n|xRkmodR=bn1R
21 oveq1 x=AxRk=ARk
22 21 fvoveq1d x=AxRkmodR=ARkmodR
23 22 eqeq1d x=AxRkmodR=bARkmodR=b
24 23 rabbidv x=Ak1n|xRkmodR=b=k1n|ARkmodR=b
25 24 fveq2d x=Ak1n|xRkmodR=b=k1n|ARkmodR=b
26 25 oveq1d x=Ak1n|xRkmodR=bn=k1n|ARkmodR=bn
27 26 mpteq2dv x=Ank1n|xRkmodR=bn=nk1n|ARkmodR=bn
28 27 breq1d x=Ank1n|xRkmodR=bn1Rnk1n|ARkmodR=bn1R
29 28 ralbidv x=Ab0R1nk1n|xRkmodR=bn1Rb0R1nk1n|ARkmodR=bn1R
30 29 elrab Ax|b0R1nk1n|xRkmodR=bn1RAb0R1nk1n|ARkmodR=bn1R
31 20 30 bitrdi R2ASRAb0R1nk1n|ARkmodR=bn1R
32 31 pm5.32i R2ASRR2Ab0R1nk1n|ARkmodR=bn1R
33 1 dmmptss domS2
34 elfvdm ASRRdomS
35 33 34 sselid ASRR2
36 35 pm4.71ri ASRR2ASR
37 3anass R2Ab0R1nk1n|ARkmodR=bn1RR2Ab0R1nk1n|ARkmodR=bn1R
38 32 36 37 3bitr4i ASRR2Ab0R1nk1n|ARkmodR=bn1R