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 | |
|
Assertion | snmlval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snml.s | |
|
2 | oveq1 | |
|
3 | 2 | oveq2d | |
4 | oveq1 | |
|
5 | 4 | oveq2d | |
6 | id | |
|
7 | 5 6 | oveq12d | |
8 | 7 | fveqeq2d | |
9 | 8 | rabbidv | |
10 | 9 | fveq2d | |
11 | 10 | oveq1d | |
12 | 11 | mpteq2dv | |
13 | oveq2 | |
|
14 | 12 13 | breq12d | |
15 | 3 14 | raleqbidv | |
16 | 15 | rabbidv | |
17 | reex | |
|
18 | 17 | rabex | |
19 | 16 1 18 | fvmpt | |
20 | 19 | eleq2d | |
21 | oveq1 | |
|
22 | 21 | fvoveq1d | |
23 | 22 | eqeq1d | |
24 | 23 | rabbidv | |
25 | 24 | fveq2d | |
26 | 25 | oveq1d | |
27 | 26 | mpteq2dv | |
28 | 27 | breq1d | |
29 | 28 | ralbidv | |
30 | 29 | elrab | |
31 | 20 30 | bitrdi | |
32 | 31 | pm5.32i | |
33 | 1 | dmmptss | |
34 | elfvdm | |
|
35 | 33 34 | sselid | |
36 | 35 | pm4.71ri | |
37 | 3anass | |
|
38 | 32 36 37 | 3bitr4i | |