Metamath Proof Explorer

Theorem hashnzfz2

Description: Special case of hashnzfz : the count of multiples in nℤ,n greater than one, restricted to an interval starting at two. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Hypotheses hashnzfz2.n 
|- ( ph -> N e. ( ZZ>= ` 2 ) )
hashnzfz2.k 
|- ( ph -> K e. NN )
Assertion hashnzfz2 
|- ( ph -> ( # ` ( ( || " { N } ) i^i ( 2 ... K ) ) ) = ( |_ ` ( K / N ) ) )

Proof

Step Hyp Ref Expression
1 hashnzfz2.n 
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
2 hashnzfz2.k 
 |-  ( ph -> K e. NN )
3 2nn 
 |-  2 e. NN
4 uznnssnn 
 |-  ( 2 e. NN -> ( ZZ>= ` 2 ) C_ NN )
5 3 4 ax-mp 
 |-  ( ZZ>= ` 2 ) C_ NN
6 5 1 sseldi 
 |-  ( ph -> N e. NN )
7 2z 
 |-  2 e. ZZ
8 7 a1i 
 |-  ( ph -> 2 e. ZZ )
9 nnuz 
 |-  NN = ( ZZ>= ` 1 )
10 2m1e1 
 |-  ( 2 - 1 ) = 1
11 10 fveq2i 
 |-  ( ZZ>= ` ( 2 - 1 ) ) = ( ZZ>= ` 1 )
12 9 11 eqtr4i 
 |-  NN = ( ZZ>= ` ( 2 - 1 ) )
13 2 12 eleqtrdi 
 |-  ( ph -> K e. ( ZZ>= ` ( 2 - 1 ) ) )
14 6 8 13 hashnzfz 
 |-  ( ph -> ( # ` ( ( || " { N } ) i^i ( 2 ... K ) ) ) = ( ( |_ ` ( K / N ) ) - ( |_ ` ( ( 2 - 1 ) / N ) ) ) )
15 10 oveq1i 
 |-  ( ( 2 - 1 ) / N ) = ( 1 / N )
16 15 fveq2i 
 |-  ( |_ ` ( ( 2 - 1 ) / N ) ) = ( |_ ` ( 1 / N ) )
17 0red 
 |-  ( ph -> 0 e. RR )
18 6 nnrecred 
 |-  ( ph -> ( 1 / N ) e. RR )
19 6 nnred 
 |-  ( ph -> N e. RR )
20 6 nngt0d 
 |-  ( ph -> 0 < N )
21 19 20 recgt0d 
 |-  ( ph -> 0 < ( 1 / N ) )
22 17 18 21 ltled 
 |-  ( ph -> 0 <_ ( 1 / N ) )
23 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
24 1 23 syl 
 |-  ( ph -> 2 <_ N )
25 6 nnzd 
 |-  ( ph -> N e. ZZ )
26 zlem1lt 
 |-  ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 <_ N <-> ( 2 - 1 ) < N ) )
27 7 25 26 sylancr 
 |-  ( ph -> ( 2 <_ N <-> ( 2 - 1 ) < N ) )
28 24 27 mpbid 
 |-  ( ph -> ( 2 - 1 ) < N )
29 10 28 eqbrtrrid 
 |-  ( ph -> 1 < N )
30 6 nnrpd 
 |-  ( ph -> N e. RR+ )
31 30 recgt1d 
 |-  ( ph -> ( 1 < N <-> ( 1 / N ) < 1 ) )
32 29 31 mpbid 
 |-  ( ph -> ( 1 / N ) < 1 )
33 0p1e1 
 |-  ( 0 + 1 ) = 1
34 32 33 breqtrrdi 
 |-  ( ph -> ( 1 / N ) < ( 0 + 1 ) )
35 0z 
 |-  0 e. ZZ
36 flbi 
 |-  ( ( ( 1 / N ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( 1 / N ) ) = 0 <-> ( 0 <_ ( 1 / N ) /\ ( 1 / N ) < ( 0 + 1 ) ) ) )
37 18 35 36 sylancl 
 |-  ( ph -> ( ( |_ ` ( 1 / N ) ) = 0 <-> ( 0 <_ ( 1 / N ) /\ ( 1 / N ) < ( 0 + 1 ) ) ) )
38 22 34 37 mpbir2and 
 |-  ( ph -> ( |_ ` ( 1 / N ) ) = 0 )
39 16 38 syl5eq 
 |-  ( ph -> ( |_ ` ( ( 2 - 1 ) / N ) ) = 0 )
40 39 oveq2d 
 |-  ( ph -> ( ( |_ ` ( K / N ) ) - ( |_ ` ( ( 2 - 1 ) / N ) ) ) = ( ( |_ ` ( K / N ) ) - 0 ) )
41 2 nnred 
 |-  ( ph -> K e. RR )
42 41 6 nndivred 
 |-  ( ph -> ( K / N ) e. RR )
43 42 flcld 
 |-  ( ph -> ( |_ ` ( K / N ) ) e. ZZ )
44 43 zcnd 
 |-  ( ph -> ( |_ ` ( K / N ) ) e. CC )
45 44 subid1d 
 |-  ( ph -> ( ( |_ ` ( K / N ) ) - 0 ) = ( |_ ` ( K / N ) ) )
46 14 40 45 3eqtrd 
 |-  ( ph -> ( # ` ( ( || " { N } ) i^i ( 2 ... K ) ) ) = ( |_ ` ( K / N ) ) )