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

Proof

Step	Hyp	Ref	Expression
1		hashnzfz2.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 2 ) )
2		hashnzfz2.k	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3		2nn	⊢ 2 ∈ ℕ
4		uznnssnn	⊢ ( 2 ∈ ℕ → ( ℤ≥ ‘ 2 ) ⊆ ℕ )
5	3 4	ax-mp	⊢ ( ℤ≥ ‘ 2 ) ⊆ ℕ
6	5 1	sselid	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7		2z	⊢ 2 ∈ ℤ
8	7	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
9		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
10		2m1e1	⊢ ( 2 − 1 ) = 1
11	10	fveq2i	⊢ ( ℤ≥ ‘ ( 2 − 1 ) ) = ( ℤ≥ ‘ 1 )
12	9 11	eqtr4i	⊢ ℕ = ( ℤ≥ ‘ ( 2 − 1 ) )
13	2 12	eleqtrdi	⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ ( 2 − 1 ) ) )
14	6 8 13	hashnzfz	⊢ ( 𝜑 → ( ♯ ‘ ( ( ∥ “ { 𝑁 } ) ∩ ( 2 ... 𝐾 ) ) ) = ( ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) − ( ⌊ ‘ ( ( 2 − 1 ) / 𝑁 ) ) ) )
15	10	oveq1i	⊢ ( ( 2 − 1 ) / 𝑁 ) = ( 1 / 𝑁 )
16	15	fveq2i	⊢ ( ⌊ ‘ ( ( 2 − 1 ) / 𝑁 ) ) = ( ⌊ ‘ ( 1 / 𝑁 ) )
17		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
18	6	nnrecred	⊢ ( 𝜑 → ( 1 / 𝑁 ) ∈ ℝ )
19	6	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
20	6	nngt0d	⊢ ( 𝜑 → 0 < 𝑁 )
21	19 20	recgt0d	⊢ ( 𝜑 → 0 < ( 1 / 𝑁 ) )
22	17 18 21	ltled	⊢ ( 𝜑 → 0 ≤ ( 1 / 𝑁 ) )
23		eluzle	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝑁 )
24	1 23	syl	⊢ ( 𝜑 → 2 ≤ 𝑁 )
25	6	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
26		zlem1lt	⊢ ( ( 2 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 2 ≤ 𝑁 ↔ ( 2 − 1 ) < 𝑁 ) )
27	7 25 26	sylancr	⊢ ( 𝜑 → ( 2 ≤ 𝑁 ↔ ( 2 − 1 ) < 𝑁 ) )
28	24 27	mpbid	⊢ ( 𝜑 → ( 2 − 1 ) < 𝑁 )
29	10 28	eqbrtrrid	⊢ ( 𝜑 → 1 < 𝑁 )
30	6	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
31	30	recgt1d	⊢ ( 𝜑 → ( 1 < 𝑁 ↔ ( 1 / 𝑁 ) < 1 ) )
32	29 31	mpbid	⊢ ( 𝜑 → ( 1 / 𝑁 ) < 1 )
33		0p1e1	⊢ ( 0 + 1 ) = 1
34	32 33	breqtrrdi	⊢ ( 𝜑 → ( 1 / 𝑁 ) < ( 0 + 1 ) )
35		0z	⊢ 0 ∈ ℤ
36		flbi	⊢ ( ( ( 1 / 𝑁 ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( 1 / 𝑁 ) ) = 0 ↔ ( 0 ≤ ( 1 / 𝑁 ) ∧ ( 1 / 𝑁 ) < ( 0 + 1 ) ) ) )
37	18 35 36	sylancl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 1 / 𝑁 ) ) = 0 ↔ ( 0 ≤ ( 1 / 𝑁 ) ∧ ( 1 / 𝑁 ) < ( 0 + 1 ) ) ) )
38	22 34 37	mpbir2and	⊢ ( 𝜑 → ( ⌊ ‘ ( 1 / 𝑁 ) ) = 0 )
39	16 38	eqtrid	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 2 − 1 ) / 𝑁 ) ) = 0 )
40	39	oveq2d	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) − ( ⌊ ‘ ( ( 2 − 1 ) / 𝑁 ) ) ) = ( ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) − 0 ) )
41	2	nnred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
42	41 6	nndivred	⊢ ( 𝜑 → ( 𝐾 / 𝑁 ) ∈ ℝ )
43	42	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ∈ ℤ )
44	43	zcnd	⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) ∈ ℂ )
45	44	subid1d	⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) − 0 ) = ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) )
46	14 40 45	3eqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( ( ∥ “ { 𝑁 } ) ∩ ( 2 ... 𝐾 ) ) ) = ( ⌊ ‘ ( 𝐾 / 𝑁 ) ) )