ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  hashdvds GIF version

Theorem hashdvds 11103
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 8713 . . . . . 6 (𝜑 → 1 ∈ ℤ)
2 hashdvds.3 . . . . . . . . . . 11 (𝜑𝐵 ∈ (ℤ‘(𝐴 − 1)))
3 eluzelz 8963 . . . . . . . . . . 11 (𝐵 ∈ (ℤ‘(𝐴 − 1)) → 𝐵 ∈ ℤ)
42, 3syl 14 . . . . . . . . . 10 (𝜑𝐵 ∈ ℤ)
5 hashdvds.4 . . . . . . . . . 10 (𝜑𝐶 ∈ ℤ)
64, 5zsubcld 8809 . . . . . . . . 9 (𝜑 → (𝐵𝐶) ∈ ℤ)
7 hashdvds.1 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
8 znq 9044 . . . . . . . . 9 (((𝐵𝐶) ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐵𝐶) / 𝑁) ∈ ℚ)
96, 7, 8syl2anc 403 . . . . . . . 8 (𝜑 → ((𝐵𝐶) / 𝑁) ∈ ℚ)
109flqcld 9615 . . . . . . 7 (𝜑 → (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℤ)
11 hashdvds.2 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℤ)
12 peano2zm 8724 . . . . . . . . . . 11 (𝐴 ∈ ℤ → (𝐴 − 1) ∈ ℤ)
1311, 12syl 14 . . . . . . . . . 10 (𝜑 → (𝐴 − 1) ∈ ℤ)
1413, 5zsubcld 8809 . . . . . . . . 9 (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℤ)
15 znq 9044 . . . . . . . . 9 ((((𝐴 − 1) − 𝐶) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℚ)
1614, 7, 15syl2anc 403 . . . . . . . 8 (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℚ)
1716flqcld 9615 . . . . . . 7 (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ)
1810, 17zsubcld 8809 . . . . . 6 (𝜑 → ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ)
19 fzen 9392 . . . . . 6 ((1 ∈ ℤ ∧ ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ ∧ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ) → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ ((1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))))
201, 18, 17, 19syl3anc 1172 . . . . 5 (𝜑 → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ ((1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))))
21 ax-1cn 7385 . . . . . . 7 1 ∈ ℂ
2217zcnd 8805 . . . . . . 7 (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ)
23 addcom 7566 . . . . . . 7 ((1 ∈ ℂ ∧ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) → (1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1))
2421, 22, 23sylancr 405 . . . . . 6 (𝜑 → (1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1))
2510zcnd 8805 . . . . . . 7 (𝜑 → (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℂ)
2625, 22npcand 7744 . . . . . 6 (𝜑 → (((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = (⌊‘((𝐵𝐶) / 𝑁)))
2724, 26oveq12d 5633 . . . . 5 (𝜑 → ((1 + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) = (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))))
2820, 27breqtrd 3846 . . . 4 (𝜑 → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))))
2917peano2zd 8807 . . . . . . 7 (𝜑 → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ)
3029, 10fzfigd 9769 . . . . . 6 (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∈ Fin)
3130elexd 2626 . . . . 5 (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∈ V)
3211, 4fzfigd 9769 . . . . . . 7 (𝜑 → (𝐴...𝐵) ∈ Fin)
33 elfzelz 9375 . . . . . . . . . . . 12 (𝑎 ∈ (𝐴...𝐵) → 𝑎 ∈ ℤ)
3433adantl 271 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (𝐴...𝐵)) → 𝑎 ∈ ℤ)
355adantr 270 . . . . . . . . . . 11 ((𝜑𝑎 ∈ (𝐴...𝐵)) → 𝐶 ∈ ℤ)
3634, 35zsubcld 8809 . . . . . . . . . 10 ((𝜑𝑎 ∈ (𝐴...𝐵)) → (𝑎𝐶) ∈ ℤ)
37 dvdsdc 10710 . . . . . . . . . 10 ((𝑁 ∈ ℕ ∧ (𝑎𝐶) ∈ ℤ) → DECID 𝑁 ∥ (𝑎𝐶))
387, 36, 37syl2an2r 560 . . . . . . . . 9 ((𝜑𝑎 ∈ (𝐴...𝐵)) → DECID 𝑁 ∥ (𝑎𝐶))
3938ralrimiva 2442 . . . . . . . 8 (𝜑 → ∀𝑎 ∈ (𝐴...𝐵)DECID 𝑁 ∥ (𝑎𝐶))
40 oveq1 5622 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝐶) = (𝑎𝐶))
4140breq2d 3834 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑁 ∥ (𝑥𝐶) ↔ 𝑁 ∥ (𝑎𝐶)))
4241dcbid 784 . . . . . . . . 9 (𝑥 = 𝑎 → (DECID 𝑁 ∥ (𝑥𝐶) ↔ DECID 𝑁 ∥ (𝑎𝐶)))
4342cbvralv 2586 . . . . . . . 8 (∀𝑥 ∈ (𝐴...𝐵)DECID 𝑁 ∥ (𝑥𝐶) ↔ ∀𝑎 ∈ (𝐴...𝐵)DECID 𝑁 ∥ (𝑎𝐶))
4439, 43sylibr 132 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (𝐴...𝐵)DECID 𝑁 ∥ (𝑥𝐶))
4532, 44ssfirab 6596 . . . . . 6 (𝜑 → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ Fin)
4645elexd 2626 . . . . 5 (𝜑 → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ V)
47 elfzle1 9376 . . . . . . . . . . . . . 14 (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)
4847adantl 271 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)
49 elfzelz 9375 . . . . . . . . . . . . . 14 (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → 𝑧 ∈ ℤ)
50 zltp1le 8740 . . . . . . . . . . . . . 14 (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ 𝑧 ∈ ℤ) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧))
5117, 49, 50syl2an 283 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧))
5248, 51mpbird 165 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)
53 flqlt 9621 . . . . . . . . . . . . 13 (((((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℚ ∧ 𝑧 ∈ ℤ) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧))
5416, 49, 53syl2an 283 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧))
5552, 54mpbird 165 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧)
5614zred 8804 . . . . . . . . . . . . 13 (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℝ)
5756adantr 270 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) ∈ ℝ)
5849adantl 271 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ∈ ℤ)
5958zred 8804 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ∈ ℝ)
607nnred 8373 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℝ)
617nngt0d 8403 . . . . . . . . . . . . . 14 (𝜑 → 0 < 𝑁)
6260, 61jca 300 . . . . . . . . . . . . 13 (𝜑 → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
6362adantr 270 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
64 ltdivmul2 8277 . . . . . . . . . . . 12 ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁)))
6557, 59, 63, 64syl3anc 1172 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁)))
6655, 65mpbid 145 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))
6713zred 8804 . . . . . . . . . . . 12 (𝜑 → (𝐴 − 1) ∈ ℝ)
6867adantr 270 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐴 − 1) ∈ ℝ)
695zred 8804 . . . . . . . . . . . 12 (𝜑𝐶 ∈ ℝ)
7069adantr 270 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐶 ∈ ℝ)
717nnzd 8803 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
7271adantr 270 . . . . . . . . . . . . 13 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑁 ∈ ℤ)
7358, 72zmulcld 8810 . . . . . . . . . . . 12 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℤ)
7473zred 8804 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℝ)
7568, 70, 74ltsubaddd 7962 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)))
7666, 75mpbid 145 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))
775adantr 270 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐶 ∈ ℤ)
7873, 77zaddcld 8808 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ ℤ)
79 zlem1lt 8742 . . . . . . . . . 10 ((𝐴 ∈ ℤ ∧ ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)))
8011, 78, 79syl2an2r 560 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)))
8176, 80mpbird 165 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐴 ≤ ((𝑧 · 𝑁) + 𝐶))
82 elfzle2 9377 . . . . . . . . . . . 12 (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁)))
8382adantl 271 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁)))
84 flqge 9620 . . . . . . . . . . . 12 ((((𝐵𝐶) / 𝑁) ∈ ℚ ∧ 𝑧 ∈ ℤ) → (𝑧 ≤ ((𝐵𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁))))
859, 49, 84syl2an 283 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 ≤ ((𝐵𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵𝐶) / 𝑁))))
8683, 85mpbird 165 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ≤ ((𝐵𝐶) / 𝑁))
876zred 8804 . . . . . . . . . . . 12 (𝜑 → (𝐵𝐶) ∈ ℝ)
8887adantr 270 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝐵𝐶) ∈ ℝ)
89 lemuldiv 8280 . . . . . . . . . . 11 ((𝑧 ∈ ℝ ∧ (𝐵𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑧 · 𝑁) ≤ (𝐵𝐶) ↔ 𝑧 ≤ ((𝐵𝐶) / 𝑁)))
9059, 88, 63, 89syl3anc 1172 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) ≤ (𝐵𝐶) ↔ 𝑧 ≤ ((𝐵𝐶) / 𝑁)))
9186, 90mpbird 165 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ≤ (𝐵𝐶))
924zred 8804 . . . . . . . . . . 11 (𝜑𝐵 ∈ ℝ)
9392adantr 270 . . . . . . . . . 10 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐵 ∈ ℝ)
94 leaddsub 7863 . . . . . . . . . 10 (((𝑧 · 𝑁) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵𝐶)))
9574, 70, 93, 94syl3anc 1172 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵𝐶)))
9691, 95mpbird 165 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵)
9711adantr 270 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐴 ∈ ℤ)
984adantr 270 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐵 ∈ ℤ)
99 elfz 9365 . . . . . . . . 9 ((((𝑧 · 𝑁) + 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵)))
10078, 97, 98, 99syl3anc 1172 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵)))
10181, 96, 100mpbir2and 888 . . . . . . 7 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵))
102 dvdsmul2 10725 . . . . . . . . 9 ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑧 · 𝑁))
10358, 72, 102syl2anc 403 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑁 ∥ (𝑧 · 𝑁))
10473zcnd 8805 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℂ)
1055zcnd 8805 . . . . . . . . . 10 (𝜑𝐶 ∈ ℂ)
106105adantr 270 . . . . . . . . 9 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝐶 ∈ ℂ)
107104, 106pncand 7741 . . . . . . . 8 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) − 𝐶) = (𝑧 · 𝑁))
108103, 107breqtrrd 3848 . . . . . . 7 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶))
109 oveq1 5622 . . . . . . . . 9 (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑥𝐶) = (((𝑧 · 𝑁) + 𝐶) − 𝐶))
110109breq2d 3834 . . . . . . . 8 (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑁 ∥ (𝑥𝐶) ↔ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶)))
111110elrab 2762 . . . . . . 7 (((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ↔ (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶)))
112101, 108, 111sylanbrc 408 . . . . . 6 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
113112ex 113 . . . . 5 (𝜑 → (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}))
114 oveq1 5622 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐶) = (𝑦𝐶))
115114breq2d 3834 . . . . . . 7 (𝑥 = 𝑦 → (𝑁 ∥ (𝑥𝐶) ↔ 𝑁 ∥ (𝑦𝐶)))
116115elrab 2762 . . . . . 6 (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ↔ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))
11767adantr 270 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐴 − 1) ∈ ℝ)
118 elfzelz 9375 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐴...𝐵) → 𝑦 ∈ ℤ)
119118ad2antrl 474 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦 ∈ ℤ)
120119zred 8804 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦 ∈ ℝ)
12169adantr 270 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐶 ∈ ℝ)
122 elfzle1 9376 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝐴...𝐵) → 𝐴𝑦)
123122ad2antrl 474 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐴𝑦)
124 zlem1lt 8742 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝐴𝑦 ↔ (𝐴 − 1) < 𝑦))
12511, 119, 124syl2an2r 560 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐴𝑦 ↔ (𝐴 − 1) < 𝑦))
126123, 125mpbid 145 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐴 − 1) < 𝑦)
127117, 120, 121, 126ltsub1dd 7978 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝐴 − 1) − 𝐶) < (𝑦𝐶))
12856adantr 270 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝐴 − 1) − 𝐶) ∈ ℝ)
1295adantr 270 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐶 ∈ ℤ)
130119, 129zsubcld 8809 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ∈ ℤ)
131130zred 8804 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ∈ ℝ)
13262adantr 270 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁))
133 ltdiv1 8267 . . . . . . . . . . . 12 ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝑦𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) < (𝑦𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁)))
134128, 131, 132, 133syl3anc 1172 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝐴 − 1) − 𝐶) < (𝑦𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁)))
135127, 134mpbid 145 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁))
136 simprr 499 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑁 ∥ (𝑦𝐶))
13771adantr 270 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑁 ∈ ℤ)
1387nnne0d 8404 . . . . . . . . . . . . . 14 (𝜑𝑁 ≠ 0)
139138adantr 270 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑁 ≠ 0)
140 dvdsval2 10705 . . . . . . . . . . . . 13 ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑦𝐶) ∈ ℤ) → (𝑁 ∥ (𝑦𝐶) ↔ ((𝑦𝐶) / 𝑁) ∈ ℤ))
141137, 139, 130, 140syl3anc 1172 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑁 ∥ (𝑦𝐶) ↔ ((𝑦𝐶) / 𝑁) ∈ ℤ))
142136, 141mpbid 145 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ∈ ℤ)
143 flqlt 9621 . . . . . . . . . . 11 (((((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℚ ∧ ((𝑦𝐶) / 𝑁) ∈ ℤ) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁)))
14416, 142, 143syl2an2r 560 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁)))
145135, 144mpbid 145 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁))
146 zltp1le 8740 . . . . . . . . . 10 (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ ((𝑦𝐶) / 𝑁) ∈ ℤ) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁)))
14717, 142, 146syl2an2r 560 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁)))
148145, 147mpbid 145 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁))
14992adantr 270 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝐵 ∈ ℝ)
150 elfzle2 9377 . . . . . . . . . . . 12 (𝑦 ∈ (𝐴...𝐵) → 𝑦𝐵)
151150ad2antrl 474 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦𝐵)
152120, 149, 121, 151lesub1dd 7982 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ≤ (𝐵𝐶))
15387adantr 270 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝐵𝐶) ∈ ℝ)
154 lediv1 8268 . . . . . . . . . . 11 (((𝑦𝐶) ∈ ℝ ∧ (𝐵𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑦𝐶) ≤ (𝐵𝐶) ↔ ((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
155131, 153, 132, 154syl3anc 1172 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) ≤ (𝐵𝐶) ↔ ((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
156152, 155mpbid 145 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁))
157 flqge 9620 . . . . . . . . . 10 ((((𝐵𝐶) / 𝑁) ∈ ℚ ∧ ((𝑦𝐶) / 𝑁) ∈ ℤ) → (((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁) ↔ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁))))
1589, 142, 157syl2an2r 560 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝑦𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁) ↔ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁))))
159156, 158mpbid 145 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁)))
16029adantr 270 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ)
16110adantr 270 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℤ)
162 elfz 9365 . . . . . . . . 9 ((((𝑦𝐶) / 𝑁) ∈ ℤ ∧ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ ∧ (⌊‘((𝐵𝐶) / 𝑁)) ∈ ℤ) → (((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁) ∧ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁)))))
163142, 160, 161, 162syl3anc 1172 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦𝐶) / 𝑁) ∧ ((𝑦𝐶) / 𝑁) ≤ (⌊‘((𝐵𝐶) / 𝑁)))))
164148, 159, 163mpbir2and 888 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → ((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))))
165164ex 113 . . . . . 6 (𝜑 → ((𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)) → ((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))))
166116, 165syl5bi 150 . . . . 5 (𝜑 → (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} → ((𝑦𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))))
167116anbi2i 445 . . . . . . 7 ((𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) ↔ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))))
168130zcnd 8805 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → (𝑦𝐶) ∈ ℂ)
169168adantrl 462 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (𝑦𝐶) ∈ ℂ)
17058zcnd 8805 . . . . . . . . . . 11 ((𝜑𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁)))) → 𝑧 ∈ ℂ)
171170adantrr 463 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑧 ∈ ℂ)
1727nncnd 8374 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℂ)
173172adantr 270 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑁 ∈ ℂ)
1747nnap0d 8405 . . . . . . . . . . 11 (𝜑𝑁 # 0)
175174adantr 270 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑁 # 0)
176169, 171, 173, 175divmulap3d 8232 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (((𝑦𝐶) / 𝑁) = 𝑧 ↔ (𝑦𝐶) = (𝑧 · 𝑁)))
177119zcnd 8805 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶))) → 𝑦 ∈ ℂ)
178177adantrl 462 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝑦 ∈ ℂ)
179105adantr 270 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → 𝐶 ∈ ℂ)
180104adantrr 463 . . . . . . . . . 10 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (𝑧 · 𝑁) ∈ ℂ)
181178, 179, 180subadd2d 7759 . . . . . . . . 9 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → ((𝑦𝐶) = (𝑧 · 𝑁) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦))
182176, 181bitrd 186 . . . . . . . 8 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (((𝑦𝐶) / 𝑁) = 𝑧 ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦))
183 eqcom 2087 . . . . . . . 8 (𝑧 = ((𝑦𝐶) / 𝑁) ↔ ((𝑦𝐶) / 𝑁) = 𝑧)
184 eqcom 2087 . . . . . . . 8 (𝑦 = ((𝑧 · 𝑁) + 𝐶) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)
185182, 183, 1843bitr4g 221 . . . . . . 7 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦𝐶)))) → (𝑧 = ((𝑦𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶)))
186167, 185sylan2b 281 . . . . . 6 ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})) → (𝑧 = ((𝑦𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶)))
187186ex 113 . . . . 5 (𝜑 → ((𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) → (𝑧 = ((𝑦𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))))
18831, 46, 113, 166, 187en3d 6440 . . . 4 (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
189 entr 6455 . . . 4 (((1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ∧ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
19028, 188, 189syl2anc 403 . . 3 (𝜑 → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)})
1911, 18fzfigd 9769 . . . 4 (𝜑 → (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin)
192 hashen 10092 . . . 4 (((1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)} ∈ Fin) → ((♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) ↔ (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}))
193191, 45, 192syl2anc 403 . . 3 (𝜑 → ((♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) ↔ (1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}))
194190, 193mpbird 165 . 2 (𝜑 → (♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}))
195 eluzle 8966 . . . . . . 7 (𝐵 ∈ (ℤ‘(𝐴 − 1)) → (𝐴 − 1) ≤ 𝐵)
1962, 195syl 14 . . . . . 6 (𝜑 → (𝐴 − 1) ≤ 𝐵)
197 zre 8690 . . . . . . . 8 ((𝐴 − 1) ∈ ℤ → (𝐴 − 1) ∈ ℝ)
198 zre 8690 . . . . . . . 8 (𝐵 ∈ ℤ → 𝐵 ∈ ℝ)
199 zre 8690 . . . . . . . 8 (𝐶 ∈ ℤ → 𝐶 ∈ ℝ)
200 lesub1 7881 . . . . . . . 8 (((𝐴 − 1) ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶)))
201197, 198, 199, 200syl3an 1214 . . . . . . 7 (((𝐴 − 1) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶)))
20213, 4, 5, 201syl3anc 1172 . . . . . 6 (𝜑 → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶)))
203196, 202mpbid 145 . . . . 5 (𝜑 → ((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶))
204 lediv1 8268 . . . . . 6 ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝐵𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
20556, 87, 62, 204syl3anc 1172 . . . . 5 (𝜑 → (((𝐴 − 1) − 𝐶) ≤ (𝐵𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)))
206203, 205mpbid 145 . . . 4 (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁))
207 flqword2 9627 . . . 4 (((((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℚ ∧ ((𝐵𝐶) / 𝑁) ∈ ℚ ∧ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵𝐶) / 𝑁)) → (⌊‘((𝐵𝐶) / 𝑁)) ∈ (ℤ‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
20816, 9, 206, 207syl3anc 1172 . . 3 (𝜑 → (⌊‘((𝐵𝐶) / 𝑁)) ∈ (ℤ‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
209 uznn0sub 8985 . . 3 ((⌊‘((𝐵𝐶) / 𝑁)) ∈ (ℤ‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) → ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℕ0)
210 hashfz1 10091 . . 3 (((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℕ0 → (♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
211208, 209, 2103syl 17 . 2 (𝜑 → (♯‘(1...((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
212194, 211eqtr3d 2119 1 (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥𝐶)}) = ((⌊‘((𝐵𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  DECID wdc 778   = wceq 1287  wcel 1436  wne 2251  wral 2355  {crab 2359   class class class wbr 3822  cfv 4983  (class class class)co 5615  cen 6409  Fincfn 6411  cc 7295  cr 7296  0cc0 7297  1c1 7298   + caddc 7300   · cmul 7302   < clt 7469  cle 7470  cmin 7600   # cap 8002   / cdiv 8081  cn 8360  0cn0 8609  cz 8686  cuz 8954  cq 9039  ...cfz 9359  cfl 9606  chash 10083  cdvds 10702
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-coll 3931  ax-sep 3934  ax-nul 3942  ax-pow 3986  ax-pr 4012  ax-un 4236  ax-setind 4328  ax-iinf 4378  ax-cnex 7383  ax-resscn 7384  ax-1cn 7385  ax-1re 7386  ax-icn 7387  ax-addcl 7388  ax-addrcl 7389  ax-mulcl 7390  ax-mulrcl 7391  ax-addcom 7392  ax-mulcom 7393  ax-addass 7394  ax-mulass 7395  ax-distr 7396  ax-i2m1 7397  ax-0lt1 7398  ax-1rid 7399  ax-0id 7400  ax-rnegex 7401  ax-precex 7402  ax-cnre 7403  ax-pre-ltirr 7404  ax-pre-ltwlin 7405  ax-pre-lttrn 7406  ax-pre-apti 7407  ax-pre-ltadd 7408  ax-pre-mulgt0 7409  ax-pre-mulext 7410  ax-arch 7411
This theorem depends on definitions:  df-bi 115  df-dc 779  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-nul 3276  df-if 3380  df-pw 3417  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3639  df-int 3674  df-iun 3717  df-br 3823  df-opab 3877  df-mpt 3878  df-tr 3914  df-id 4096  df-po 4099  df-iso 4100  df-iord 4169  df-on 4171  df-ilim 4172  df-suc 4174  df-iom 4381  df-xp 4419  df-rel 4420  df-cnv 4421  df-co 4422  df-dm 4423  df-rn 4424  df-res 4425  df-ima 4426  df-iota 4948  df-fun 4985  df-fn 4986  df-f 4987  df-f1 4988  df-fo 4989  df-f1o 4990  df-fv 4991  df-riota 5571  df-ov 5618  df-oprab 5619  df-mpt2 5620  df-1st 5870  df-2nd 5871  df-recs 6026  df-frec 6112  df-1o 6137  df-er 6246  df-en 6412  df-dom 6413  df-fin 6414  df-pnf 7471  df-mnf 7472  df-xr 7473  df-ltxr 7474  df-le 7475  df-sub 7602  df-neg 7603  df-reap 7996  df-ap 8003  df-div 8082  df-inn 8361  df-n0 8610  df-z 8687  df-uz 8955  df-q 9040  df-rp 9070  df-fz 9360  df-fl 9608  df-mod 9661  df-ihash 10084  df-dvds 10703
This theorem is referenced by:  phiprmpw  11104
  Copyright terms: Public domain W3C validator