Metamath Proof Explorer

Theorem snmlff

Description: The function F from snmlval is a mapping from positive integers to real numbers in the range [ 0 , 1 ] . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypothesis snmlff.f 
|- F = ( n e. NN |-> ( ( # ` { k e. ( 1 ... n ) | ( |_ ` ( ( A x. ( R ^ k ) ) mod R ) ) = B } ) / n ) )
Assertion snmlff 
|- F : NN --> ( 0 [,] 1 )

Proof

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 mulridd 
 |-  ( 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 )