Theorem snmlval 28965

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 6203	. . . . . . . . 9 |- ( r = R -> ( r - 1 ) = ( R - 1 ) )
2	1	oveq2d 6212	. . . . . . . 8 |- ( r = R -> ( 0 ... ( r - 1 ) ) = ( 0 ... ( R - 1 ) ) )
3		oveq1 6203	. . . . . . . . . . . . . . . . 17 |- ( r = R -> ( r ^ k ) = ( R ^ k ) )
4	3	oveq2d 6212	. . . . . . . . . . . . . . . 16 |- ( r = R -> ( x x. ( r ^ k ) ) = ( x x. ( R ^ k ) ) )
5		id 22	. . . . . . . . . . . . . . . 16 |- ( r = R -> r = R )
6	4, 5	oveq12d 6214	. . . . . . . . . . . . . . 15 |- ( r = R -> ( ( x x. ( r ^ k ) ) mod r ) = ( ( x x. ( R ^ k ) ) mod R ) )
7	6	fveq2d 5778	. . . . . . . . . . . . . 14 |- ( r = R -> ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) )
8	7	eqeq1d 2384	. . . . . . . . . . . . 13 |- ( r = R -> ( ( |_ ` ( ( x x. ( r ^ k ) ) mod r ) ) = b <-> ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b ) )
9	8	rabbidv 3026	. . . . . . . . . . . 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 5778	. . . . . . . . . . 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 6211	. . . . . . . . . 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 4454	. . . . . . . . 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 6204	. . . . . . . . 9 |- ( r = R -> ( 1 / r ) = ( 1 / R ) )
14	12, 13	breq12d 4380	. . . . . . . 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 2993	. . . . . . 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 3026	. . . . . 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 9494	. . . . . . 7 |- RR e. _V
19	18	rabex 4516	. . . . . 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 5857	. . . . 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 2452	. . . 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 6203	. . . . . . . . . . . . . 14 |- ( x = A -> ( x x. ( R ^ k ) ) = ( A x. ( R ^ k ) ) )
23	22	oveq1d 6211	. . . . . . . . . . . . 13 |- ( x = A -> ( ( x x. ( R ^ k ) ) mod R ) = ( ( A x. ( R ^ k ) ) mod R ) )
24	23	fveq2d 5778	. . . . . . . . . . . 12 |- ( x = A -> ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) )
25	24	eqeq1d 2384	. . . . . . . . . . 11 |- ( x = A -> ( ( |_ ` ( ( x x. ( R ^ k ) ) mod R ) ) = b <-> ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = b ) )
26	25	rabbidv 3026	. . . . . . . . . 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 5778	. . . . . . . . 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 6211	. . . . . . . 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 4454	. . . . . . 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 4377	. . . . . 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 2821	. . . . 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 3182	. . . 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 261	. . 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 635	. 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 5411	. . . 4 |- dom S C_ ( ZZ>= ` 2 )
36		elfvdm 5800	. . . 4 |- ( A e. ( S ` R ) -> R e. dom S )
37	35, 36	sseldi 3415	. . 3 |- ( A e. ( S ` R ) -> R e. ( ZZ>= ` 2 ) )
38	37	pm4.71ri 631	. 2 |- ( A e. ( S ` R ) <-> ( R e. ( ZZ>= ` 2 ) /\ A e. ( S ` R ) ) )
39		3anass 975	. 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 277	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 184   /\ wa 367   /\ w3a 971   = wceq 1399   e. wcel 1826   A.wral 2732   {crab 2736   class class class wbr 4367   |-> cmpt 4425   dom cdm 4913   ` cfv 5496  (class class class)co 6196   RRcr 9402   0cc0 9403   1c1 9404   x. cmul 9408   - cmin 9718   / cdiv 10123   NNcn 10452   2c2 10502   ZZ>=cuz 11001   ...cfz 11593   |_cfl 11826   mod cmo 11896   ^cexp 12069   #chash 12307   ~~> cli 13309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-cnex 9459  ax-resscn 9460

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fv 5504  df-ov 6199

This theorem is referenced by:  snmlflim  28966