Metamath Proof Explorer

Theorem hashnzfz

Description: Special case of hashdvds : the count of multiples in nℤ restricted to an interval. (Contributed by Steve Rodriguez, 20-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 hashnzfz.n
` |-  ( ph -> N e. NN )`
2 hashnzfz.j
` |-  ( ph -> J e. ZZ )`
3 hashnzfz.k
` |-  ( ph -> K e. ( ZZ>= ` ( J - 1 ) ) )`
4 0zd
` |-  ( ph -> 0 e. ZZ )`
5 1 2 3 4 hashdvds
` |-  ( ph -> ( # ` { x e. ( J ... K ) | N || ( x - 0 ) } ) = ( ( |_ ` ( ( K - 0 ) / N ) ) - ( |_ ` ( ( ( J - 1 ) - 0 ) / N ) ) ) )`
6 elfzelz
` |-  ( x e. ( J ... K ) -> x e. ZZ )`
7 6 zcnd
` |-  ( x e. ( J ... K ) -> x e. CC )`
8 7 subid1d
` |-  ( x e. ( J ... K ) -> ( x - 0 ) = x )`
9 8 breq2d
` |-  ( x e. ( J ... K ) -> ( N || ( x - 0 ) <-> N || x ) )`
10 9 rabbiia
` |-  { x e. ( J ... K ) | N || ( x - 0 ) } = { x e. ( J ... K ) | N || x }`
11 dfrab3
` |-  { x e. ( J ... K ) | N || x } = ( ( J ... K ) i^i { x | N || x } )`
12 reldvds
` |-  Rel ||`
13 relimasn
` |-  ( Rel || -> ( || " { N } ) = { x | N || x } )`
14 12 13 ax-mp
` |-  ( || " { N } ) = { x | N || x }`
15 14 ineq2i
` |-  ( ( J ... K ) i^i ( || " { N } ) ) = ( ( J ... K ) i^i { x | N || x } )`
16 incom
` |-  ( ( J ... K ) i^i ( || " { N } ) ) = ( ( || " { N } ) i^i ( J ... K ) )`
17 15 16 eqtr3i
` |-  ( ( J ... K ) i^i { x | N || x } ) = ( ( || " { N } ) i^i ( J ... K ) )`
18 10 11 17 3eqtri
` |-  { x e. ( J ... K ) | N || ( x - 0 ) } = ( ( || " { N } ) i^i ( J ... K ) )`
19 18 fveq2i
` |-  ( # ` { x e. ( J ... K ) | N || ( x - 0 ) } ) = ( # ` ( ( || " { N } ) i^i ( J ... K ) ) )`
20 19 a1i
` |-  ( ph -> ( # ` { x e. ( J ... K ) | N || ( x - 0 ) } ) = ( # ` ( ( || " { N } ) i^i ( J ... K ) ) ) )`
21 eluzelz
` |-  ( K e. ( ZZ>= ` ( J - 1 ) ) -> K e. ZZ )`
22 3 21 syl
` |-  ( ph -> K e. ZZ )`
23 22 zcnd
` |-  ( ph -> K e. CC )`
24 23 subid1d
` |-  ( ph -> ( K - 0 ) = K )`
25 24 fvoveq1d
` |-  ( ph -> ( |_ ` ( ( K - 0 ) / N ) ) = ( |_ ` ( K / N ) ) )`
26 peano2zm
` |-  ( J e. ZZ -> ( J - 1 ) e. ZZ )`
27 2 26 syl
` |-  ( ph -> ( J - 1 ) e. ZZ )`
28 27 zcnd
` |-  ( ph -> ( J - 1 ) e. CC )`
29 28 subid1d
` |-  ( ph -> ( ( J - 1 ) - 0 ) = ( J - 1 ) )`
30 29 fvoveq1d
` |-  ( ph -> ( |_ ` ( ( ( J - 1 ) - 0 ) / N ) ) = ( |_ ` ( ( J - 1 ) / N ) ) )`
31 25 30 oveq12d
` |-  ( ph -> ( ( |_ ` ( ( K - 0 ) / N ) ) - ( |_ ` ( ( ( J - 1 ) - 0 ) / N ) ) ) = ( ( |_ ` ( K / N ) ) - ( |_ ` ( ( J - 1 ) / N ) ) ) )`
32 5 20 31 3eqtr3d
` |-  ( ph -> ( # ` ( ( || " { N } ) i^i ( J ... K ) ) ) = ( ( |_ ` ( K / N ) ) - ( |_ ` ( ( J - 1 ) / N ) ) ) )`