Step |
Hyp |
Ref |
Expression |
1 |
|
snmlff.f |
|- F = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) ) |
2 |
|
fzfid |
|- ( n e. NN -> ( 1 ... n ) e. Fin ) |
3 |
|
ssrab2 |
|- { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } C_ ( 1 ... n ) |
4 |
|
ssfi |
|- ( ( ( 1 ... n ) e. Fin /\ { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } C_ ( 1 ... n ) ) -> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } e. Fin ) |
5 |
2 3 4
|
sylancl |
|- ( n e. NN -> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } e. Fin ) |
6 |
|
hashcl |
|- ( { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } e. Fin -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) e. NN0 ) |
7 |
5 6
|
syl |
|- ( n e. NN -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) e. NN0 ) |
8 |
7
|
nn0red |
|- ( n e. NN -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) e. RR ) |
9 |
|
nndivre |
|- ( ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) e. RR /\ n e. NN ) -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) e. RR ) |
10 |
8 9
|
mpancom |
|- ( n e. NN -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) e. RR ) |
11 |
7
|
nn0ge0d |
|- ( n e. NN -> 0 <_ ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) ) |
12 |
|
nnre |
|- ( n e. NN -> n e. RR ) |
13 |
|
nngt0 |
|- ( n e. NN -> 0 < n ) |
14 |
|
divge0 |
|- ( ( ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) e. RR /\ 0 <_ ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) ) /\ ( n e. RR /\ 0 < n ) ) -> 0 <_ ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) ) |
15 |
8 11 12 13 14
|
syl22anc |
|- ( n e. NN -> 0 <_ ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) ) |
16 |
|
ssdomg |
|- ( ( 1 ... n ) e. Fin -> ( { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } C_ ( 1 ... n ) -> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ~<_ ( 1 ... n ) ) ) |
17 |
2 3 16
|
mpisyl |
|- ( n e. NN -> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ~<_ ( 1 ... n ) ) |
18 |
|
hashdom |
|- ( ( { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } e. Fin /\ ( 1 ... n ) e. Fin ) -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) <_ ( # ` ( 1 ... n ) ) <-> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ~<_ ( 1 ... n ) ) ) |
19 |
5 2 18
|
syl2anc |
|- ( n e. NN -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) <_ ( # ` ( 1 ... n ) ) <-> { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ~<_ ( 1 ... n ) ) ) |
20 |
17 19
|
mpbird |
|- ( n e. NN -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) <_ ( # ` ( 1 ... n ) ) ) |
21 |
|
nnnn0 |
|- ( n e. NN -> n e. NN0 ) |
22 |
|
hashfz1 |
|- ( n e. NN0 -> ( # ` ( 1 ... n ) ) = n ) |
23 |
21 22
|
syl |
|- ( n e. NN -> ( # ` ( 1 ... n ) ) = n ) |
24 |
20 23
|
breqtrd |
|- ( n e. NN -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) <_ n ) |
25 |
|
nncn |
|- ( n e. NN -> n e. CC ) |
26 |
25
|
mulid1d |
|- ( n e. NN -> ( n x. 1 ) = n ) |
27 |
24 26
|
breqtrrd |
|- ( n e. NN -> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) <_ ( n x. 1 ) ) |
28 |
|
1red |
|- ( n e. NN -> 1 e. RR ) |
29 |
|
ledivmul |
|- ( ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) e. RR /\ 1 e. RR /\ ( n e. RR /\ 0 < n ) ) -> ( ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) <_ 1 <-> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) <_ ( n x. 1 ) ) ) |
30 |
8 28 12 13 29
|
syl112anc |
|- ( n e. NN -> ( ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) <_ 1 <-> ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) <_ ( n x. 1 ) ) ) |
31 |
27 30
|
mpbird |
|- ( n e. NN -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) <_ 1 ) |
32 |
|
elicc01 |
|- ( ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) e. ( 0 [,] 1 ) <-> ( ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) e. RR /\ 0 <_ ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) /\ ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) <_ 1 ) ) |
33 |
10 15 31 32
|
syl3anbrc |
|- ( n e. NN -> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) e. ( 0 [,] 1 ) ) |
34 |
1 33
|
fmpti |
|- F : NN --> ( 0 [,] 1 ) |