MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashdvds Structured version   Visualization version   GIF version

Theorem hashdvds 16102
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.)
Hypotheses
Ref Expression
hashdvds.1 (𝜑𝑁 ∈ ℕ)
hashdvds.2 (𝜑𝐴 ∈ ℤ)
hashdvds.3 (𝜑𝐵 ∈ (ℤ‘(𝐴 − 1)))
hashdvds.4 (𝜑𝐶 ∈ ℤ)
Assertion
Ref Expression
hashdvds (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝑁
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem hashdvds
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1zzd 12001 . . . . . 6 (𝜑 → 1 ∈ ℤ)
2 hashdvds.3 . . . . . . . . . . . 12 (𝜑𝐵 ∈ (ℤ‘(𝐴 − 1)))
3 eluzelz 12241 . . . . . . . . . . . 12 (𝐵 ∈ (ℤ‘(𝐴 − 1)) → 𝐵 ∈ ℤ)
42, 3syl 17 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℤ)
5 hashdvds.4 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℤ)
64, 5zsubcld 12080 . . . . . . . . . 10 (𝜑 → (𝐵𝐶) ∈ ℤ)
76zred 12075 . . . . . . . . 9 (𝜑 → (𝐵𝐶) ∈ ℝ)
8 hashdvds.1 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
97, 8nndivred 11679 . . . . . . . 8 (𝜑 → ((𝐵𝐶) / 𝑁) ∈ ℝ)
109flcld 13163 . . . . . . 7 (𝜑 → (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℤ)
11 hashdvds.2 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℤ)
12 peano2zm 12013 . . . . . . . . . . . 12 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
1311, 12syl 17 . . . . . . . . . . 11 (𝜑 → (𝐴 − 1) ∈ ℤ)
1413, 5zsubcld 12080 . . . . . . . . . 10 (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℤ)
1514zred 12075 . . . . . . . . 9 (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℝ)
1615, 8nndivred 11679 . . . . . . . 8 (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ)
1716flcld 13163 . . . . . . 7 (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ)
1810, 17zsubcld 12080 . . . . . 6 (𝜑 → ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ)
19 fzen 12919 . . . . . 6 ((1 ∈ ℤ ∧ ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ ∧ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ) → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ ((1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))))
201, 18, 17, 19syl3anc 1368 . . . . 5 (𝜑 → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ ((1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))))
21 ax-1cn 10584 . . . . . . 7 1 ∈ ℂ
2217zcnd 12076 . . . . . . 7 (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ)
23 addcom 10815 . . . . . . 7 ((1 ∈ ℂ ∧ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) → (1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1))
2421, 22, 23sylancr 590 . . . . . 6 (𝜑 → (1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1))
2510zcnd 12076 . . . . . . 7 (𝜑 → (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℂ)
2625, 22npcand 10990 . . . . . 6 (𝜑 → (((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = (⌊‘((𝐵𝐶) / 𝑁)))
2724, 26oveq12d 7153 . . . . 5 (𝜑 → ((1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) = (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))))
2820, 27breqtrd 5056 . . . 4 (𝜑 → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))))
29 ovexd 7170 . . . . 5 (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∈ V)
30 fzfi 13335 . . . . . 6 (𝐴...𝐵) ∈ Fin
31 rabexg 5198 . . . . . 6 ((𝐴...𝐵) ∈ Fin → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ V)
3230, 31mp1i 13 . . . . 5 (𝜑 → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ V)
33 oveq1 7142 . . . . . . . 8 (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑥𝐶) = (((𝑧 · 𝑁) + 𝐶) − 𝐶))
3433breq2d 5042 . . . . . . 7 (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑁 ∥ (𝑥𝐶) ↔ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶)))
35 elfzle1 12905 . . . . . . . . . . . . . 14 (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)
3635adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)
37 elfzelz 12902 . . . . . . . . . . . . . 14 (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → 𝑧 ∈ ℤ)
38 zltp1le 12020 . . . . . . . . . . . . . 14 (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧))
3917, 37, 38syl2an 598 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧))
4036, 39mpbird 260 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)
41 fllt 13171 . . . . . . . . . . . . 13 (((((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧))
4216, 37, 41syl2an 598 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧))
4340, 42mpbird 260 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧)
4415adantr 484 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) ∈ ℝ)
4537adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ∈ ℤ)
4645zred 12075 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ∈ ℝ)
478nnred 11640 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
488nngt0d 11674 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
4947, 48jca 515 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
5049adantr 484 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
51 ltdivmul2 11506 . . . . . . . . . . . 12 ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁)))
5244, 46, 50, 51syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁)))
5343, 52mpbid 235 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))
5413zred 12075 . . . . . . . . . . . 12 (𝜑 → (𝐴 − 1) ∈ ℝ)
5554adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐴 − 1) ∈ ℝ)
565zred 12075 . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℝ)
5756adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐶 ∈ ℝ)
588nnzd 12074 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
5958adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑁 ∈ ℤ)
6045, 59zmulcld 12081 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℤ)
6160zred 12075 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℝ)
6255, 57, 61ltsubaddd 11225 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)))
6353, 62mpbid 235 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))
645adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐶 ∈ ℤ)
6560, 64zaddcld 12079 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ ℤ)
66 zlem1lt 12022 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)))
6711, 65, 66syl2an2r 684 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)))
6863, 67mpbird 260 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐴 ≤ ((𝑧 · 𝑁) + 𝐶))
69 elfzle2 12906 . . . . . . . . . . . 12 (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁)))
7069adantl 485 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁)))
71 flge 13170 . . . . . . . . . . . 12 ((((𝐵𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) → (𝑧 ≤ ((𝐵𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁))))
729, 37, 71syl2an 598 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 ≤ ((𝐵𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁))))
7370, 72mpbird 260 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ≤ ((𝐵𝐶) / 𝑁))
747adantr 484 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐵𝐶) ∈ ℝ)
75 lemuldiv 11509 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ∧ (𝐵𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑧 · 𝑁) ≤ (𝐵𝐶) ↔ 𝑧 ≤ ((𝐵𝐶) / 𝑁)))
7646, 74, 50, 75syl3anc 1368 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) ≤ (𝐵𝐶) ↔ 𝑧 ≤ ((𝐵𝐶) / 𝑁)))
7773, 76mpbird 260 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ≤ (𝐵𝐶))
784zred 12075 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
7978adantr 484 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐵 ∈ ℝ)
80 leaddsub 11105 . . . . . . . . . 10 (((𝑧 · 𝑁) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵𝐶)))
8161, 57, 79, 80syl3anc 1368 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵𝐶)))
8277, 81mpbird 260 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵)
8311adantr 484 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐴 ∈ ℤ)
844adantr 484 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐵 ∈ ℤ)
85 elfz 12891 . . . . . . . . 9 ((((𝑧 · 𝑁) + 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵)))
8665, 83, 84, 85syl3anc 1368 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵)))
8768, 82, 86mpbir2and 712 . . . . . . 7 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵))
88 dvdsmul2 15624 . . . . . . . . 9 ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑧 · 𝑁))
8945, 59, 88syl2anc 587 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑁 ∥ (𝑧 · 𝑁))
9060zcnd 12076 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℂ)
915zcnd 12076 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
9291adantr 484 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐶 ∈ ℂ)
9390, 92pncand 10987 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) − 𝐶) = (𝑧 · 𝑁))
9489, 93breqtrrd 5058 . . . . . . 7 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶))
9534, 87, 94elrabd 3630 . . . . . 6 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
9695ex 416 . . . . 5 (𝜑 → (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}))
97 oveq1 7142 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐶) = (𝑦𝐶))
9897breq2d 5042 . . . . . . 7 (𝑥 = 𝑦 → (𝑁 ∥ (𝑥𝐶) ↔ 𝑁 ∥ (𝑦𝐶)))
9998elrab 3628 . . . . . 6 (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ↔ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))
10054adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐴 − 1) ∈ ℝ)
101 elfzelz 12902 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐴...𝐵) → 𝑦 ∈ ℤ)
102101ad2antrl 727 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦 ∈ ℤ)
103102zred 12075 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦 ∈ ℝ)
10456adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐶 ∈ ℝ)
105 elfzle1 12905 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐴...𝐵) → 𝐴𝑦)
106105ad2antrl 727 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐴𝑦)
107 zlem1lt 12022 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝐴𝑦 ↔ (𝐴 − 1) < 𝑦))
10811, 102, 107syl2an2r 684 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐴𝑦 ↔ (𝐴 − 1) < 𝑦))
109106, 108mpbid 235 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐴 − 1) < 𝑦)
110100, 103, 104, 109ltsub1dd 11241 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝐴 − 1) − 𝐶) < (𝑦𝐶))
11115adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝐴 − 1) − 𝐶) ∈ ℝ)
1125adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐶 ∈ ℤ)
113102, 112zsubcld 12080 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ∈ ℤ)
114113zred 12075 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ∈ ℝ)
11549adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
116 ltdiv1 11493 . . . . . . . . . . . 12 ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝑦𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) < (𝑦𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁)))
117111, 114, 115, 116syl3anc 1368 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝐴 − 1) − 𝐶) < (𝑦𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁)))
118110, 117mpbid 235 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁))
119 simprr 772 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑁 ∥ (𝑦𝐶))
12058adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑁 ∈ ℤ)
1218nnne0d 11675 . . . . . . . . . . . . . 14 (𝜑𝑁 ≠ 0)
122121adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑁 ≠ 0)
123 dvdsval2 15602 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑦𝐶) ∈ ℤ) → (𝑁 ∥ (𝑦𝐶) ↔ ((𝑦𝐶) / 𝑁) ∈ ℤ))
124120, 122, 113, 123syl3anc 1368 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑁 ∥ (𝑦𝐶) ↔ ((𝑦𝐶) / 𝑁) ∈ ℤ))
125119, 124mpbid 235 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ∈ ℤ)
126 fllt 13171 . . . . . . . . . . 11 (((((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦𝐶) / 𝑁) ∈ ℤ) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁)))
12716, 125, 126syl2an2r 684 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁)))
128118, 127mpbid 235 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁))
129 zltp1le 12020 . . . . . . . . . 10 (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ ((𝑦𝐶) / 𝑁) ∈ ℤ) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁)))
13017, 125, 129syl2an2r 684 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁)))
131128, 130mpbid 235 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁))
13278adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐵 ∈ ℝ)
133 elfzle2 12906 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴...𝐵) → 𝑦𝐵)
134133ad2antrl 727 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦𝐵)
135103, 132, 104, 134lesub1dd 11245 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ≤ (𝐵𝐶))
1367adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐵𝐶) ∈ ℝ)
137 lediv1 11494 . . . . . . . . . . 11 (((𝑦𝐶) ∈ ℝ ∧ (𝐵𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑦𝐶) ≤ (𝐵𝐶) ↔ ((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
138114, 136, 115, 137syl3anc 1368 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) ≤ (𝐵𝐶) ↔ ((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
139135, 138mpbid 235 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁))
140 flge 13170 . . . . . . . . . 10 ((((𝐵𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦𝐶) / 𝑁) ∈ ℤ) → (((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁) ↔ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁))))
1419, 125, 140syl2an2r 684 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁) ↔ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁))))
142139, 141mpbid 235 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁)))
14317peano2zd 12078 . . . . . . . . . 10 (𝜑 → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ)
144143adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ)
14510adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℤ)
146 elfz 12891 . . . . . . . . 9 ((((𝑦𝐶) / 𝑁) ∈ ℤ ∧ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ ∧ (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℤ) → (((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁) ∧ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁)))))
147125, 144, 145, 146syl3anc 1368 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁) ∧ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁)))))
148131, 142, 147mpbir2and 712 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))))
149148ex 416 . . . . . 6 (𝜑 → ((𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)) → ((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))))
15099, 149syl5bi 245 . . . . 5 (𝜑 → (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} → ((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))))
15199anbi2i 625 . . . . . . 7 ((𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) ↔ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))))
152113zcnd 12076 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ∈ ℂ)
153152adantrl 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (𝑦𝐶) ∈ ℂ)
15445zcnd 12076 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ∈ ℂ)
155154adantrr 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑧 ∈ ℂ)
1568nncnd 11641 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
157156adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑁 ∈ ℂ)
158121adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑁 ≠ 0)
159153, 155, 157, 158divmul3d 11439 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (((𝑦𝐶) / 𝑁) = 𝑧 ↔ (𝑦𝐶) = (𝑧 · 𝑁)))
160102zcnd 12076 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦 ∈ ℂ)
161160adantrl 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑦 ∈ ℂ)
16291adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝐶 ∈ ℂ)
16390adantrr 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (𝑧 · 𝑁) ∈ ℂ)
164161, 162, 163subadd2d 11005 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → ((𝑦𝐶) = (𝑧 · 𝑁) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦))
165159, 164bitrd 282 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (((𝑦𝐶) / 𝑁) = 𝑧 ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦))
166 eqcom 2805 . . . . . . . 8 (𝑧 = ((𝑦𝐶) / 𝑁) ↔ ((𝑦𝐶) / 𝑁) = 𝑧)
167 eqcom 2805 . . . . . . . 8 (𝑦 = ((𝑧 · 𝑁) + 𝐶) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)
168165, 166, 1673bitr4g 317 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (𝑧 = ((𝑦𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶)))
169151, 168sylan2b 596 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})) → (𝑧 = ((𝑦𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶)))
170169ex 416 . . . . 5 (𝜑 → ((𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) → (𝑧 = ((𝑦𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))))
17129, 32, 96, 150, 170en3d 8529 . . . 4 (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
172 entr 8544 . . . 4 (((1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
17328, 171, 172syl2anc 587 . . 3 (𝜑 → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
174 fzfi 13335 . . . 4 (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin
175 ssrab2 4007 . . . . 5 {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ⊆ (𝐴...𝐵)
176 ssfi 8722 . . . . 5 (((𝐴...𝐵) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ⊆ (𝐴...𝐵)) → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ Fin)
17730, 175, 176mp2an 691 . . . 4 {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ Fin
178 hashen 13703 . . . 4 (((1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ Fin) → ((♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) ↔ (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}))
179174, 177, 178mp2an 691 . . 3 ((♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) ↔ (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
180173, 179sylibr 237 . 2 (𝜑 → (♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}))
181 eluzle 12244 . . . . . . 7 (𝐵 ∈ (ℤ‘(𝐴 − 1)) → (𝐴 − 1) ≤ 𝐵)
1822, 181syl 17 . . . . . 6 (𝜑 → (𝐴 − 1) ≤ 𝐵)
183 zre 11973 . . . . . . . 8 ((𝐴 − 1) ∈ ℤ → (𝐴 − 1) ∈ ℝ)
184 zre 11973 . . . . . . . 8 (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
185 zre 11973 . . . . . . . 8 (𝐶 ∈ ℤ → 𝐶 ∈ ℝ)
186 lesub1 11123 . . . . . . . 8 (((𝐴 − 1) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶)))
187183, 184, 185, 186syl3an 1157 . . . . . . 7 (((𝐴 − 1) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶)))
18813, 4, 5, 187syl3anc 1368 . . . . . 6 (𝜑 → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶)))
189182, 188mpbid 235 . . . . 5 (𝜑 → ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶))
190 lediv1 11494 . . . . . 6 ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝐵𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
19115, 7, 49, 190syl3anc 1368 . . . . 5 (𝜑 → (((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
192189, 191mpbid 235 . . . 4 (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁))
193 flword2 13178 . . . 4 (((((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ ∧ ((𝐵𝐶) / 𝑁) ∈ ℝ ∧ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)) → (⌊‘((𝐵𝐶) / 𝑁)) ∈ (ℤ‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
19416, 9, 192, 193syl3anc 1368 . . 3 (𝜑 → (⌊‘((𝐵𝐶) / 𝑁)) ∈ (ℤ‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
195 uznn0sub 12265 . . 3 ((⌊‘((𝐵𝐶) / 𝑁)) ∈ (ℤ‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) → ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℕ0)
196 hashfz1 13702 . . 3 (((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℕ0 → (♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
197194, 195, 1963syl 18 . 2 (𝜑 → (♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
198180, 197eqtr3d 2835 1 (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2111  wne 2987  {crab 3110  Vcvv 3441  wss 3881   class class class wbr 5030  cfv 6324  (class class class)co 7135  cen 8489  Fincfn 8492  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531   < clt 10664  cle 10665  cmin 10859   / cdiv 11286  cn 11625  0cn0 11885  cz 11969  cuz 12231  ...cfz 12885  cfl 13155  chash 13686  cdvds 15599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-sup 8890  df-inf 8891  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fl 13157  df-hash 13687  df-dvds 15600
This theorem is referenced by:  phiprmpw  16103  prmreclem4  16245  ppiub  25788  hashnzfz  41019
  Copyright terms: Public domain W3C validator