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 = ( 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 ) } )
Assertion 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 ) ) )

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 oveq1 
 |-  ( r = R -> ( r - 1 ) = ( R - 1 ) )
3 2 oveq2d 
 |-  ( r = R -> ( 0 ... ( r - 1 ) ) = ( 0 ... ( R - 1 ) ) )
4 oveq1 
 |-  ( r = R -> ( r ^ k ) = ( R ^ k ) )
5 4 oveq2d 
 |-  ( r = R -> ( x x. ( r ^ k ) ) = ( x x. ( R ^ k ) ) )
6 id 
 |-  ( r = R -> r = R )
7 5 6 oveq12d 
 |-  ( r = R -> ( ( x x. ( r ^ k ) ) mod r ) = ( ( x x. ( R ^ k ) ) mod R ) )
8 7 fveqeq2d 
 |-  ( r = R -> ( ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b <-> ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b ) )
9 8 rabbidv 
 |-  ( r = R -> { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } = { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } )
10 9 fveq2d 
 |-  ( r = R -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } ) = ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) )
11 10 oveq1d 
 |-  ( r = R -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } ) / n ) = ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) )
12 11 mpteq2dv 
 |-  ( r = R -> ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } ) / n ) ) = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) )
13 oveq2 
 |-  ( r = R -> ( 1 / r ) = ( 1 / R ) )
14 12 13 breq12d 
 |-  ( r = R -> ( ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } ) / n ) ) ~~> ( 1 / r ) <-> ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) ) )
15 3 14 raleqbidv 
 |-  ( r = R -> ( A. b e. ( 0 ... ( r - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b } ) / n ) ) ~~> ( 1 / r ) <-> A. b e. ( 0 ... ( R - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) ) )
16 15 rabbidv 
 |-  ( r = R -> { 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 ) } = { 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 ) } )
17 reex 
 |-  RR e. _V
18 17 rabex 
 |-  { 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 ) } e. _V
19 16 1 18 fvmpt 
 |-  ( R e. ( ZZ>= ` 2 ) -> ( S ` R ) = { 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 ) } )
20 19 eleq2d 
 |-  ( R e. ( ZZ>= ` 2 ) -> ( A e. ( S ` R ) <-> A e. { 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 ) } ) )
21 oveq1 
 |-  ( x = A -> ( x x. ( R ^ k ) ) = ( A x. ( R ^ k ) ) )
22 21 fvoveq1d 
 |-  ( x = A -> ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) )
23 22 eqeq1d 
 |-  ( x = A -> ( ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b <-> ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b ) )
24 23 rabbidv 
 |-  ( x = A -> { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } = { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } )
25 24 fveq2d 
 |-  ( x = A -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) = ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) )
26 25 oveq1d 
 |-  ( x = A -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) = ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) )
27 26 mpteq2dv 
 |-  ( x = A -> ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) )
28 27 breq1d 
 |-  ( x = A -> ( ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) <-> ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) ) )
29 28 ralbidv 
 |-  ( x = A -> ( A. b e. ( 0 ... ( R - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) <-> A. b e. ( 0 ... ( R - 1 ) ) ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) / n ) ) ~~> ( 1 / R ) ) )
30 29 elrab 
 |-  ( A e. { 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 ) } <-> ( 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 ) ) )
31 20 30 bitrdi 
 |-  ( R e. ( ZZ>= ` 2 ) -> ( A e. ( S ` R ) <-> ( 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 ) ) ) )
32 31 pm5.32i 
 |-  ( ( R e. ( ZZ>= ` 2 ) /\ 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 ) ) ) )
33 1 dmmptss 
 |-  dom S C_ ( ZZ>= ` 2 )
34 elfvdm 
 |-  ( A e. ( S ` R ) -> R e. dom S )
35 33 34 sseldi 
 |-  ( A e. ( S ` R ) -> R e. ( ZZ>= ` 2 ) )
36 35 pm4.71ri 
 |-  ( A e. ( S ` R ) <-> ( R e. ( ZZ>= ` 2 ) /\ A e. ( S ` R ) ) )
37 3anass 
 |-  ( ( 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 ) ) <-> ( 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 ) ) ) )
38 32 36 37 3bitr4i 
 |-  ( 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 ) ) )