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