Theorem 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	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	hashdvds.2	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
	hashdvds.3	⊢ ( 𝜑 → 𝐵 ∈ ( ℤ≥ ‘ ( 𝐴 − 1 ) ) )
	hashdvds.4	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
Assertion	hashdvds	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ ( 𝐴 ... 𝐵 ) ∣ 𝑁 ∥ ( 𝑥 − 𝐶 ) } ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝐶 ) / 𝑁 ) ) − ( ⌊ ‘ ( ( ( 𝐴 − 1 ) − 𝐶 ) / 𝑁 ) ) ) )

Proof

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