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	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	hashnzfz.j	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
	hashnzfz.k	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ ( 𝐽 − 1 ) ) )
Assertion	hashnzfz	⊢ ( 𝜑 → ( ♯ ‘ ( ( ∥ “ { 𝑁 } ) ∩ ( 𝐽 ... 𝐾 ) ) ) = ( ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) − ( ⌊ ‘ ( ( 𝐽 − 1 ) / 𝑁 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hashnzfz.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		hashnzfz.j	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
3		hashnzfz.k	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ ( 𝐽 − 1 ) ) )
4		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
5	1 2 3 4	hashdvds	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∣ 𝑁 ∥ ( 𝑥 − 0 ) } ) = ( ( ⌊ ‘ ( ( 𝐾 − 0 ) / 𝑁 ) ) − ( ⌊ ‘ ( ( ( 𝐽 − 1 ) − 0 ) / 𝑁 ) ) ) )
6		elfzelz	⊢ ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) → 𝑥 ∈ ℤ )
7	6	zcnd	⊢ ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) → 𝑥 ∈ ℂ )
8	7	subid1d	⊢ ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) → ( 𝑥 − 0 ) = 𝑥 )
9	8	breq2d	⊢ ( 𝑥 ∈ ( 𝐽 ... 𝐾 ) → ( 𝑁 ∥ ( 𝑥 − 0 ) ↔ 𝑁 ∥ 𝑥 ) )
10	9	rabbiia	⊢ { 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∣ 𝑁 ∥ ( 𝑥 − 0 ) } = { 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∣ 𝑁 ∥ 𝑥 }
11		dfrab3	⊢ { 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∣ 𝑁 ∥ 𝑥 } = ( ( 𝐽 ... 𝐾 ) ∩ { 𝑥 ∣ 𝑁 ∥ 𝑥 } )
12		reldvds	⊢ Rel ∥
13		relimasn	⊢ ( Rel ∥ → ( ∥ “ { 𝑁 } ) = { 𝑥 ∣ 𝑁 ∥ 𝑥 } )
14	12 13	ax-mp	⊢ ( ∥ “ { 𝑁 } ) = { 𝑥 ∣ 𝑁 ∥ 𝑥 }
15	14	ineq2i	⊢ ( ( 𝐽 ... 𝐾 ) ∩ ( ∥ “ { 𝑁 } ) ) = ( ( 𝐽 ... 𝐾 ) ∩ { 𝑥 ∣ 𝑁 ∥ 𝑥 } )
16		incom	⊢ ( ( 𝐽 ... 𝐾 ) ∩ ( ∥ “ { 𝑁 } ) ) = ( ( ∥ “ { 𝑁 } ) ∩ ( 𝐽 ... 𝐾 ) )
17	15 16	eqtr3i	⊢ ( ( 𝐽 ... 𝐾 ) ∩ { 𝑥 ∣ 𝑁 ∥ 𝑥 } ) = ( ( ∥ “ { 𝑁 } ) ∩ ( 𝐽 ... 𝐾 ) )
18	10 11 17	3eqtri	⊢ { 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∣ 𝑁 ∥ ( 𝑥 − 0 ) } = ( ( ∥ “ { 𝑁 } ) ∩ ( 𝐽 ... 𝐾 ) )
19	18	fveq2i	⊢ ( ♯ ‘ { 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∣ 𝑁 ∥ ( 𝑥 − 0 ) } ) = ( ♯ ‘ ( ( ∥ “ { 𝑁 } ) ∩ ( 𝐽 ... 𝐾 ) ) )
20	19	a1i	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ ( 𝐽 ... 𝐾 ) ∣ 𝑁 ∥ ( 𝑥 − 0 ) } ) = ( ♯ ‘ ( ( ∥ “ { 𝑁 } ) ∩ ( 𝐽 ... 𝐾 ) ) ) )
21		eluzelz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( 𝐽 − 1 ) ) → 𝐾 ∈ ℤ )
22	3 21	syl	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
23	22	zcnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
24	23	subid1d	⊢ ( 𝜑 → ( 𝐾 − 0 ) = 𝐾 )
25	24	fvoveq1d	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐾 − 0 ) / 𝑁 ) ) = ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) )
26		peano2zm	⊢ ( 𝐽 ∈ ℤ → ( 𝐽 − 1 ) ∈ ℤ )
27	2 26	syl	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℤ )
28	27	zcnd	⊢ ( 𝜑 → ( 𝐽 − 1 ) ∈ ℂ )
29	28	subid1d	⊢ ( 𝜑 → ( ( 𝐽 − 1 ) − 0 ) = ( 𝐽 − 1 ) )
30	29	fvoveq1d	⊢ ( 𝜑 → ( ⌊ ‘ ( ( ( 𝐽 − 1 ) − 0 ) / 𝑁 ) ) = ( ⌊ ‘ ( ( 𝐽 − 1 ) / 𝑁 ) ) )
31	25 30	oveq12d	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐾 − 0 ) / 𝑁 ) ) − ( ⌊ ‘ ( ( ( 𝐽 − 1 ) − 0 ) / 𝑁 ) ) ) = ( ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) − ( ⌊ ‘ ( ( 𝐽 − 1 ) / 𝑁 ) ) ) )
32	5 20 31	3eqtr3d	⊢ ( 𝜑 → ( ♯ ‘ ( ( ∥ “ { 𝑁 } ) ∩ ( 𝐽 ... 𝐾 ) ) ) = ( ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) − ( ⌊ ‘ ( ( 𝐽 − 1 ) / 𝑁 ) ) ) )