hashdvds

Description: The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014) (Proof shortened by Mario Carneiro, 7-Jun-2016)

	Ref	Expression
Hypotheses	hashdvds.1	$⊢ φ \to N \in ℕ$
	hashdvds.2	$⊢ φ \to A \in ℤ$
	hashdvds.3	$⊢ φ \to B \in ℤ_{\geq (A - 1)}$
	hashdvds.4	$⊢ φ \to C \in ℤ$
Assertion	hashdvds	$⊢ φ \to \|\{x \in (A \dots B) \| N ∥ (x - C)\}\| = ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋$

Proof

Step	Hyp	Ref	Expression
1		hashdvds.1	$⊢ φ \to N \in ℕ$
2		hashdvds.2	$⊢ φ \to A \in ℤ$
3		hashdvds.3	$⊢ φ \to B \in ℤ_{\geq (A - 1)}$
4		hashdvds.4	$⊢ φ \to C \in ℤ$
5		1zzd	$⊢ φ \to 1 \in ℤ$
6		eluzelz	$⊢ B \in ℤ_{\geq (A - 1)} \to B \in ℤ$
7	3 6	syl	$⊢ φ \to B \in ℤ$
8	7 4	zsubcld	$⊢ φ \to B - C \in ℤ$
9	8	zred	$⊢ φ \to B - C \in ℝ$
10	9 1	nndivred	$⊢ φ \to \frac{B - C}{N} \in ℝ$
11	10	flcld	$⊢ φ \to ⌊\frac{B - C}{N}⌋ \in ℤ$
12		peano2zm	$⊢ A \in ℤ \to A - 1 \in ℤ$
13	2 12	syl	$⊢ φ \to A - 1 \in ℤ$
14	13 4	zsubcld	$⊢ φ \to A - 1 - C \in ℤ$
15	14	zred	$⊢ φ \to A - 1 - C \in ℝ$
16	15 1	nndivred	$⊢ φ \to \frac{A - 1 - C}{N} \in ℝ$
17	16	flcld	$⊢ φ \to ⌊\frac{A - 1 - C}{N}⌋ \in ℤ$
18	11 17	zsubcld	$⊢ φ \to ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ \in ℤ$
19		fzen	$⊢ (1 \in ℤ \land ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ \in ℤ \land ⌊\frac{A - 1 - C}{N}⌋ \in ℤ) \to (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx (1 + ⌊\frac{A - 1 - C}{N}⌋ \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ + ⌊\frac{A - 1 - C}{N}⌋)$
20	5 18 17 19	syl3anc	$⊢ φ \to (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx (1 + ⌊\frac{A - 1 - C}{N}⌋ \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ + ⌊\frac{A - 1 - C}{N}⌋)$
21		ax-1cn	$⊢ 1 \in ℂ$
22	17	zcnd	$⊢ φ \to ⌊\frac{A - 1 - C}{N}⌋ \in ℂ$
23		addcom	$⊢ (1 \in ℂ \land ⌊\frac{A - 1 - C}{N}⌋ \in ℂ) \to 1 + ⌊\frac{A - 1 - C}{N}⌋ = ⌊\frac{A - 1 - C}{N}⌋ + 1$
24	21 22 23	sylancr	$⊢ φ \to 1 + ⌊\frac{A - 1 - C}{N}⌋ = ⌊\frac{A - 1 - C}{N}⌋ + 1$
25	11	zcnd	$⊢ φ \to ⌊\frac{B - C}{N}⌋ \in ℂ$
26	25 22	npcand	$⊢ φ \to ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ + ⌊\frac{A - 1 - C}{N}⌋ = ⌊\frac{B - C}{N}⌋$
27	24 26	oveq12d	$⊢ φ \to (1 + ⌊\frac{A - 1 - C}{N}⌋ \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ + ⌊\frac{A - 1 - C}{N}⌋) = (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)$
28	20 27	breqtrd	$⊢ φ \to (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)$
29		ovexd	$⊢ φ \to (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \in V$
30		fzfi	$⊢ (A \dots B) \in Fin$
31		rabexg	$⊢ (A \dots B) \in Fin \to \{x \in (A \dots B) \| N ∥ (x - C)\} \in V$
32	30 31	mp1i	$⊢ φ \to \{x \in (A \dots B) \| N ∥ (x - C)\} \in V$
33		oveq1	$⊢ x = z \cdot N + C \to x - C = z \cdot N + C - C$
34	33	breq2d	$⊢ x = z \cdot N + C \to (N ∥ (x - C) \leftrightarrow N ∥ (z \cdot N + C - C))$
35	2	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to A \in ℤ$
36	7	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to B \in ℤ$
37		elfzelz	$⊢ z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \to z \in ℤ$
38	37	adantl	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \in ℤ$
39	1	nnzd	$⊢ φ \to N \in ℤ$
40	39	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to N \in ℤ$
41	38 40	zmulcld	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N \in ℤ$
42	4	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to C \in ℤ$
43	41 42	zaddcld	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N + C \in ℤ$
44		elfzle1	$⊢ z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \to ⌊\frac{A - 1 - C}{N}⌋ + 1 \leq z$
45	44	adantl	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to ⌊\frac{A - 1 - C}{N}⌋ + 1 \leq z$
46		zltp1le	$⊢ (⌊\frac{A - 1 - C}{N}⌋ \in ℤ \land z \in ℤ) \to (⌊\frac{A - 1 - C}{N}⌋ < z \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ + 1 \leq z)$
47	17 37 46	syl2an	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (⌊\frac{A - 1 - C}{N}⌋ < z \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ + 1 \leq z)$
48	45 47	mpbird	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to ⌊\frac{A - 1 - C}{N}⌋ < z$
49		fllt	$⊢ (\frac{A - 1 - C}{N} \in ℝ \land z \in ℤ) \to (\frac{A - 1 - C}{N} < z \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ < z)$
50	16 37 49	syl2an	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (\frac{A - 1 - C}{N} < z \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ < z)$
51	48 50	mpbird	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to \frac{A - 1 - C}{N} < z$
52	15	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to A - 1 - C \in ℝ$
53	38	zred	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \in ℝ$
54	1	nnred	$⊢ φ \to N \in ℝ$
55	1	nngt0d	$⊢ φ \to 0 < N$
56	54 55	jca	$⊢ φ \to (N \in ℝ \land 0 < N)$
57	56	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (N \in ℝ \land 0 < N)$
58		ltdivmul2	$⊢ (A - 1 - C \in ℝ \land z \in ℝ \land (N \in ℝ \land 0 < N)) \to (\frac{A - 1 - C}{N} < z \leftrightarrow A - 1 - C < z \cdot N)$
59	52 53 57 58	syl3anc	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (\frac{A - 1 - C}{N} < z \leftrightarrow A - 1 - C < z \cdot N)$
60	51 59	mpbid	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to A - 1 - C < z \cdot N$
61	13	zred	$⊢ φ \to A - 1 \in ℝ$
62	61	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to A - 1 \in ℝ$
63	4	zred	$⊢ φ \to C \in ℝ$
64	63	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to C \in ℝ$
65	41	zred	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N \in ℝ$
66	62 64 65	ltsubaddd	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (A - 1 - C < z \cdot N \leftrightarrow A - 1 < z \cdot N + C)$
67	60 66	mpbid	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to A - 1 < z \cdot N + C$
68		zlem1lt	$⊢ (A \in ℤ \land z \cdot N + C \in ℤ) \to (A \leq z \cdot N + C \leftrightarrow A - 1 < z \cdot N + C)$
69	2 43 68	syl2an2r	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (A \leq z \cdot N + C \leftrightarrow A - 1 < z \cdot N + C)$
70	67 69	mpbird	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to A \leq z \cdot N + C$
71		elfzle2	$⊢ z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \to z \leq ⌊\frac{B - C}{N}⌋$
72	71	adantl	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \leq ⌊\frac{B - C}{N}⌋$
73		flge	$⊢ (\frac{B - C}{N} \in ℝ \land z \in ℤ) \to (z \leq \frac{B - C}{N} \leftrightarrow z \leq ⌊\frac{B - C}{N}⌋)$
74	10 37 73	syl2an	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (z \leq \frac{B - C}{N} \leftrightarrow z \leq ⌊\frac{B - C}{N}⌋)$
75	72 74	mpbird	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \leq \frac{B - C}{N}$
76	9	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to B - C \in ℝ$
77		lemuldiv	$⊢ (z \in ℝ \land B - C \in ℝ \land (N \in ℝ \land 0 < N)) \to (z \cdot N \leq B - C \leftrightarrow z \leq \frac{B - C}{N})$
78	53 76 57 77	syl3anc	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (z \cdot N \leq B - C \leftrightarrow z \leq \frac{B - C}{N})$
79	75 78	mpbird	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N \leq B - C$
80	7	zred	$⊢ φ \to B \in ℝ$
81	80	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to B \in ℝ$
82		leaddsub	$⊢ (z \cdot N \in ℝ \land C \in ℝ \land B \in ℝ) \to (z \cdot N + C \leq B \leftrightarrow z \cdot N \leq B - C)$
83	65 64 81 82	syl3anc	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to (z \cdot N + C \leq B \leftrightarrow z \cdot N \leq B - C)$
84	79 83	mpbird	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N + C \leq B$
85	35 36 43 70 84	elfzd	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N + C \in (A \dots B)$
86		dvdsmul2	$⊢ (z \in ℤ \land N \in ℤ) \to N ∥ z \cdot N$
87	38 40 86	syl2anc	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to N ∥ z \cdot N$
88	41	zcnd	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N \in ℂ$
89	4	zcnd	$⊢ φ \to C \in ℂ$
90	89	adantr	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to C \in ℂ$
91	88 90	pncand	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N + C - C = z \cdot N$
92	87 91	breqtrrd	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to N ∥ (z \cdot N + C - C)$
93	34 85 92	elrabd	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \cdot N + C \in \{x \in (A \dots B) \| N ∥ (x - C)\}$
94	93	ex	$⊢ φ \to (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \to z \cdot N + C \in \{x \in (A \dots B) \| N ∥ (x - C)\})$
95		oveq1	$⊢ x = y \to x - C = y - C$
96	95	breq2d	$⊢ x = y \to (N ∥ (x - C) \leftrightarrow N ∥ (y - C))$
97	96	elrab	$⊢ y \in \{x \in (A \dots B) \| N ∥ (x - C)\} \leftrightarrow (y \in (A \dots B) \land N ∥ (y - C))$
98	17	peano2zd	$⊢ φ \to ⌊\frac{A - 1 - C}{N}⌋ + 1 \in ℤ$
99	98	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to ⌊\frac{A - 1 - C}{N}⌋ + 1 \in ℤ$
100	11	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to ⌊\frac{B - C}{N}⌋ \in ℤ$
101		simprr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to N ∥ (y - C)$
102	39	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to N \in ℤ$
103	1	nnne0d	$⊢ φ \to N \neq 0$
104	103	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to N \neq 0$
105		elfzelz	$⊢ y \in (A \dots B) \to y \in ℤ$
106	105	ad2antrl	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y \in ℤ$
107	4	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to C \in ℤ$
108	106 107	zsubcld	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y - C \in ℤ$
109		dvdsval2	$⊢ (N \in ℤ \land N \neq 0 \land y - C \in ℤ) \to (N ∥ (y - C) \leftrightarrow \frac{y - C}{N} \in ℤ)$
110	102 104 108 109	syl3anc	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (N ∥ (y - C) \leftrightarrow \frac{y - C}{N} \in ℤ)$
111	101 110	mpbid	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to \frac{y - C}{N} \in ℤ$
112	61	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to A - 1 \in ℝ$
113	106	zred	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y \in ℝ$
114	63	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to C \in ℝ$
115		elfzle1	$⊢ y \in (A \dots B) \to A \leq y$
116	115	ad2antrl	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to A \leq y$
117		zlem1lt	$⊢ (A \in ℤ \land y \in ℤ) \to (A \leq y \leftrightarrow A - 1 < y)$
118	2 106 117	syl2an2r	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (A \leq y \leftrightarrow A - 1 < y)$
119	116 118	mpbid	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to A - 1 < y$
120	112 113 114 119	ltsub1dd	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to A - 1 - C < y - C$
121	15	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to A - 1 - C \in ℝ$
122	108	zred	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y - C \in ℝ$
123	56	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (N \in ℝ \land 0 < N)$
124		ltdiv1	$⊢ (A - 1 - C \in ℝ \land y - C \in ℝ \land (N \in ℝ \land 0 < N)) \to (A - 1 - C < y - C \leftrightarrow \frac{A - 1 - C}{N} < \frac{y - C}{N})$
125	121 122 123 124	syl3anc	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (A - 1 - C < y - C \leftrightarrow \frac{A - 1 - C}{N} < \frac{y - C}{N})$
126	120 125	mpbid	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to \frac{A - 1 - C}{N} < \frac{y - C}{N}$
127		fllt	$⊢ (\frac{A - 1 - C}{N} \in ℝ \land \frac{y - C}{N} \in ℤ) \to (\frac{A - 1 - C}{N} < \frac{y - C}{N} \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ < \frac{y - C}{N})$
128	16 111 127	syl2an2r	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (\frac{A - 1 - C}{N} < \frac{y - C}{N} \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ < \frac{y - C}{N})$
129	126 128	mpbid	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to ⌊\frac{A - 1 - C}{N}⌋ < \frac{y - C}{N}$
130		zltp1le	$⊢ (⌊\frac{A - 1 - C}{N}⌋ \in ℤ \land \frac{y - C}{N} \in ℤ) \to (⌊\frac{A - 1 - C}{N}⌋ < \frac{y - C}{N} \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ + 1 \leq \frac{y - C}{N})$
131	17 111 130	syl2an2r	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (⌊\frac{A - 1 - C}{N}⌋ < \frac{y - C}{N} \leftrightarrow ⌊\frac{A - 1 - C}{N}⌋ + 1 \leq \frac{y - C}{N})$
132	129 131	mpbid	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to ⌊\frac{A - 1 - C}{N}⌋ + 1 \leq \frac{y - C}{N}$
133	80	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to B \in ℝ$
134		elfzle2	$⊢ y \in (A \dots B) \to y \leq B$
135	134	ad2antrl	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y \leq B$
136	113 133 114 135	lesub1dd	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y - C \leq B - C$
137	9	adantr	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to B - C \in ℝ$
138		lediv1	$⊢ (y - C \in ℝ \land B - C \in ℝ \land (N \in ℝ \land 0 < N)) \to (y - C \leq B - C \leftrightarrow \frac{y - C}{N} \leq \frac{B - C}{N})$
139	122 137 123 138	syl3anc	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (y - C \leq B - C \leftrightarrow \frac{y - C}{N} \leq \frac{B - C}{N})$
140	136 139	mpbid	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to \frac{y - C}{N} \leq \frac{B - C}{N}$
141		flge	$⊢ (\frac{B - C}{N} \in ℝ \land \frac{y - C}{N} \in ℤ) \to (\frac{y - C}{N} \leq \frac{B - C}{N} \leftrightarrow \frac{y - C}{N} \leq ⌊\frac{B - C}{N}⌋)$
142	10 111 141	syl2an2r	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to (\frac{y - C}{N} \leq \frac{B - C}{N} \leftrightarrow \frac{y - C}{N} \leq ⌊\frac{B - C}{N}⌋)$
143	140 142	mpbid	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to \frac{y - C}{N} \leq ⌊\frac{B - C}{N}⌋$
144	99 100 111 132 143	elfzd	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to \frac{y - C}{N} \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)$
145	144	ex	$⊢ φ \to ((y \in (A \dots B) \land N ∥ (y - C)) \to \frac{y - C}{N} \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋))$
146	97 145	biimtrid	$⊢ φ \to (y \in \{x \in (A \dots B) \| N ∥ (x - C)\} \to \frac{y - C}{N} \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋))$
147	97	anbi2i	$⊢ (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land y \in \{x \in (A \dots B) \| N ∥ (x - C)\}) \leftrightarrow (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))$
148	108	zcnd	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y - C \in ℂ$
149	148	adantrl	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to y - C \in ℂ$
150	38	zcnd	$⊢ (φ \land z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋)) \to z \in ℂ$
151	150	adantrr	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to z \in ℂ$
152	1	nncnd	$⊢ φ \to N \in ℂ$
153	152	adantr	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to N \in ℂ$
154	103	adantr	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to N \neq 0$
155	149 151 153 154	divmul3d	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to (\frac{y - C}{N} = z \leftrightarrow y - C = z \cdot N)$
156	106	zcnd	$⊢ (φ \land (y \in (A \dots B) \land N ∥ (y - C))) \to y \in ℂ$
157	156	adantrl	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to y \in ℂ$
158	89	adantr	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to C \in ℂ$
159	88	adantrr	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to z \cdot N \in ℂ$
160	157 158 159	subadd2d	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to (y - C = z \cdot N \leftrightarrow z \cdot N + C = y)$
161	155 160	bitrd	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to (\frac{y - C}{N} = z \leftrightarrow z \cdot N + C = y)$
162		eqcom	$⊢ z = \frac{y - C}{N} \leftrightarrow \frac{y - C}{N} = z$
163		eqcom	$⊢ y = z \cdot N + C \leftrightarrow z \cdot N + C = y$
164	161 162 163	3bitr4g	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (y \in (A \dots B) \land N ∥ (y - C)))) \to (z = \frac{y - C}{N} \leftrightarrow y = z \cdot N + C)$
165	147 164	sylan2b	$⊢ (φ \land (z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land y \in \{x \in (A \dots B) \| N ∥ (x - C)\})) \to (z = \frac{y - C}{N} \leftrightarrow y = z \cdot N + C)$
166	165	ex	$⊢ φ \to ((z \in (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land y \in \{x \in (A \dots B) \| N ∥ (x - C)\}) \to (z = \frac{y - C}{N} \leftrightarrow y = z \cdot N + C))$
167	29 32 94 146 166	en3d	$⊢ φ \to (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \approx \{x \in (A \dots B) \| N ∥ (x - C)\}$
168		entr	$⊢ ((1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \land (⌊\frac{A - 1 - C}{N}⌋ + 1 \dots ⌊\frac{B - C}{N}⌋) \approx \{x \in (A \dots B) \| N ∥ (x - C)\}) \to (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx \{x \in (A \dots B) \| N ∥ (x - C)\}$
169	28 167 168	syl2anc	$⊢ φ \to (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx \{x \in (A \dots B) \| N ∥ (x - C)\}$
170		fzfi	$⊢ (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \in Fin$
171		ssrab2	$⊢ \{x \in (A \dots B) \| N ∥ (x - C)\} \subseteq (A \dots B)$
172		ssfi	$⊢ ((A \dots B) \in Fin \land \{x \in (A \dots B) \| N ∥ (x - C)\} \subseteq (A \dots B)) \to \{x \in (A \dots B) \| N ∥ (x - C)\} \in Fin$
173	30 171 172	mp2an	$⊢ \{x \in (A \dots B) \| N ∥ (x - C)\} \in Fin$
174		hashen	$⊢ ((1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \in Fin \land \{x \in (A \dots B) \| N ∥ (x - C)\} \in Fin) \to (\|(1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋)\| = \|\{x \in (A \dots B) \| N ∥ (x - C)\}\| \leftrightarrow (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx \{x \in (A \dots B) \| N ∥ (x - C)\})$
175	170 173 174	mp2an	$⊢ \|(1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋)\| = \|\{x \in (A \dots B) \| N ∥ (x - C)\}\| \leftrightarrow (1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋) \approx \{x \in (A \dots B) \| N ∥ (x - C)\}$
176	169 175	sylibr	$⊢ φ \to \|(1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋)\| = \|\{x \in (A \dots B) \| N ∥ (x - C)\}\|$
177		eluzle	$⊢ B \in ℤ_{\geq (A - 1)} \to A - 1 \leq B$
178	3 177	syl	$⊢ φ \to A - 1 \leq B$
179		zre	$⊢ A - 1 \in ℤ \to A - 1 \in ℝ$
180		zre	$⊢ B \in ℤ \to B \in ℝ$
181		zre	$⊢ C \in ℤ \to C \in ℝ$
182		lesub1	$⊢ (A - 1 \in ℝ \land B \in ℝ \land C \in ℝ) \to (A - 1 \leq B \leftrightarrow A - 1 - C \leq B - C)$
183	179 180 181 182	syl3an	$⊢ (A - 1 \in ℤ \land B \in ℤ \land C \in ℤ) \to (A - 1 \leq B \leftrightarrow A - 1 - C \leq B - C)$
184	13 7 4 183	syl3anc	$⊢ φ \to (A - 1 \leq B \leftrightarrow A - 1 - C \leq B - C)$
185	178 184	mpbid	$⊢ φ \to A - 1 - C \leq B - C$
186		lediv1	$⊢ (A - 1 - C \in ℝ \land B - C \in ℝ \land (N \in ℝ \land 0 < N)) \to (A - 1 - C \leq B - C \leftrightarrow \frac{A - 1 - C}{N} \leq \frac{B - C}{N})$
187	15 9 56 186	syl3anc	$⊢ φ \to (A - 1 - C \leq B - C \leftrightarrow \frac{A - 1 - C}{N} \leq \frac{B - C}{N})$
188	185 187	mpbid	$⊢ φ \to \frac{A - 1 - C}{N} \leq \frac{B - C}{N}$
189		flword2	$⊢ (\frac{A - 1 - C}{N} \in ℝ \land \frac{B - C}{N} \in ℝ \land \frac{A - 1 - C}{N} \leq \frac{B - C}{N}) \to ⌊\frac{B - C}{N}⌋ \in ℤ_{\geq ⌊\frac{A - 1 - C}{N}⌋}$
190	16 10 188 189	syl3anc	$⊢ φ \to ⌊\frac{B - C}{N}⌋ \in ℤ_{\geq ⌊\frac{A - 1 - C}{N}⌋}$
191		uznn0sub	$⊢ ⌊\frac{B - C}{N}⌋ \in ℤ_{\geq ⌊\frac{A - 1 - C}{N}⌋} \to ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ \in ℕ_{0}$
192		hashfz1	$⊢ ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋ \in ℕ_{0} \to \|(1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋)\| = ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋$
193	190 191 192	3syl	$⊢ φ \to \|(1 \dots ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋)\| = ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋$
194	176 193	eqtr3d	$⊢ φ \to \|\{x \in (A \dots B) \| N ∥ (x - C)\}\| = ⌊\frac{B - C}{N}⌋ - ⌊\frac{A - 1 - C}{N}⌋$

Metamath Proof Explorer

Theorem hashdvds

Proof