This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) − 𝐶 ) / 𝑁 ) ) ) )