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