Theorem snmlval 30126

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.)

Hypothesis

Ref	Expression
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

Ref	Expression
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 ) ) )

Distinct variable groups:   k, b, n, x, A   r, b, R, k, n, x

Allowed substitution hints:   A( r)   S( x, k, n, r, b)

Proof of Theorem snmlval

Step	Hyp	Ref	Expression
1		oveq1 6315	. . . . . . . . 9 |- ( r = R -> ( r - 1 ) = ( R - 1 ) )
2	1	oveq2d 6324	. . . . . . . 8 |- ( r = R -> ( 0 ... ( r - 1 ) ) = ( 0 ... ( R - 1 ) ) )
3		oveq1 6315	. . . . . . . . . . . . . . . . 17 |- ( r = R -> ( r ^ k ) = ( R ^ k ) )
4	3	oveq2d 6324	. . . . . . . . . . . . . . . 16 |- ( r = R -> ( x x. ( r ^ k ) ) = ( x x. ( R ^ k ) ) )
5		id 22	. . . . . . . . . . . . . . . 16 |- ( r = R -> r = R )
6	4, 5	oveq12d 6326	. . . . . . . . . . . . . . 15 |- ( r = R -> ( ( x x. ( r ^ k ) ) mod r ) = ( ( x x. ( R ^ k ) ) mod R ) )
7	6	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( r = R -> ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) )
8	7	eqeq1d 2473	. . . . . . . . . . . . 13 |- ( r = R -> ( ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b <-> ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b ) )
9	8	rabbidv 3022	. . . . . . . . . . . 12 |- ( 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 5883	. . . . . . . . . . 11 |- ( 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 6323	. . . . . . . . . 10 |- ( 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 4483	. . . . . . . . 9 |- ( 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 6316	. . . . . . . . 9 |- ( r = R -> ( 1 / r ) = ( 1 / R ) )
14	12, 13	breq12d 4408	. . . . . . . 8 |- ( 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	2, 14	raleqbidv 2987	. . . . . . 7 |- ( 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 3022	. . . . . 6 |- ( 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		snml.s	. . . . . 6 |- 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 ) } )
18		reex 9648	. . . . . . 7 |- RR e. _V
19	18	rabex 4550	. . . . . 6 |- { 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
20	16, 17, 19	fvmpt 5963	. . . . 5 |- ( 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 ) } )
21	20	eleq2d 2534	. . . 4 |- ( 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 ) } ) )
22		oveq1 6315	. . . . . . . . . . . . . 14 |- ( x = A -> ( x x. ( R ^ k ) ) = ( A x. ( R ^ k ) ) )
23	22	oveq1d 6323	. . . . . . . . . . . . 13 |- ( x = A -> ( ( x x. ( R ^ k ) ) mod R ) = ( ( A x. ( R ^ k ) ) mod R ) )
24	23	fveq2d 5883	. . . . . . . . . . . 12 |- ( x = A -> ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) )
25	24	eqeq1d 2473	. . . . . . . . . . 11 |- ( x = A -> ( ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b <-> ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b ) )
26	25	rabbidv 3022	. . . . . . . . . 10 |- ( x = A -> { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } = { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } )
27	26	fveq2d 5883	. . . . . . . . 9 |- ( x = A -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b } ) = ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b } ) )
28	27	oveq1d 6323	. . . . . . . 8 |- ( 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 ) )
29	28	mpteq2dv 4483	. . . . . . 7 |- ( 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 ) ) )
30	29	breq1d 4405	. . . . . 6 |- ( 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 ) ) )
31	30	ralbidv 2829	. . . . 5 |- ( 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 ) ) )
32	31	elrab 3184	. . . 4 |- ( 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 ) ) )
33	21, 32	syl6bb 269	. . 3 |- ( 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 ) ) ) )
34	33	pm5.32i 649	. 2 |- ( ( 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 ) ) ) )
35	17	dmmptss 5338	. . . 4 |- dom S C_ ( ZZ>= ` 2 )
36		elfvdm 5905	. . . 4 |- ( A e. ( S ` R ) -> R e. dom S )
37	35, 36	sseldi 3416	. . 3 |- ( A e. ( S ` R ) -> R e. ( ZZ>= ` 2 ) )
38	37	pm4.71ri 645	. 2 |- ( A e. ( S ` R ) <-> ( R e. ( ZZ>= ` 2 ) /\ A e. ( S ` R ) ) )
39		3anass 1011	. 2 |- ( ( 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 ) ) ) )
40	34, 38, 39	3bitr4i 285	1 |- ( 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 ) ) )

Syntax hints:   <-> wb 189   /\ wa 376   /\ w3a 1007   = wceq 1452   e. wcel 1904   A.wral 2756   {crab 2760   class class class wbr 4395   |-> cmpt 4454   dom cdm 4839   ` cfv 5589  (class class class)co 6308   RRcr 9556   0cc0 9557   1c1 9558   x. cmul 9562   - cmin 9880   / cdiv 10291   NNcn 10631   2c2 10681   ZZ>=cuz 11182   ...cfz 11810   |_cfl 12059   mod cmo 12129   ^cexp 12310   #chash 12553   ~~> cli 13625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-cnex 9613  ax-resscn 9614

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fv 5597  df-ov 6311

This theorem is referenced by:  snmlflim  30127