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