Step | Hyp | Ref
| Expression |
1 | | 1zzd 11737 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
2 | | hashdvds.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘(𝐴 − 1))) |
3 | | eluzelz 11979 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈
(ℤ≥‘(𝐴 − 1)) → 𝐵 ∈ ℤ) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ) |
5 | | hashdvds.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℤ) |
6 | 4, 5 | zsubcld 11816 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ) |
7 | 6 | zred 11811 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℝ) |
8 | | hashdvds.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | 7, 8 | nndivred 11406 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐶) / 𝑁) ∈ ℝ) |
10 | 9 | flcld 12895 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℤ) |
11 | | hashdvds.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
12 | | peano2zm 11749 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 1) ∈ ℤ) |
14 | 13, 5 | zsubcld 11816 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℤ) |
15 | 14 | zred 11811 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
16 | 15, 8 | nndivred 11406 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ) |
17 | 16 | flcld 12895 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ) |
18 | 10, 17 | zsubcld 11816 |
. . . . . 6
⊢ (𝜑 → ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ) |
19 | | fzen 12652 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ ∧
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)) ∈ ℤ) →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) |
20 | 1, 18, 17, 19 | syl3anc 1496 |
. . . . 5
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) |
21 | | ax-1cn 10311 |
. . . . . . 7
⊢ 1 ∈
ℂ |
22 | 17 | zcnd 11812 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) |
23 | | addcom 10542 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) → (1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)) |
24 | 21, 22, 23 | sylancr 583 |
. . . . . 6
⊢ (𝜑 → (1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)) |
25 | 10 | zcnd 11812 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℂ) |
26 | 25, 22 | npcand 10718 |
. . . . . 6
⊢ (𝜑 → (((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = (⌊‘((𝐵 − 𝐶) / 𝑁))) |
27 | 24, 26 | oveq12d 6924 |
. . . . 5
⊢ (𝜑 → ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) = (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) |
28 | 20, 27 | breqtrd 4900 |
. . . 4
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁)))) |
29 | | ovexd 6940 |
. . . . 5
⊢ (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∈ V) |
30 | | fzfi 13067 |
. . . . . 6
⊢ (𝐴...𝐵) ∈ Fin |
31 | | rabexg 5037 |
. . . . . 6
⊢ ((𝐴...𝐵) ∈ Fin → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ V) |
32 | 30, 31 | mp1i 13 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ V) |
33 | | elfzle1 12638 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) + 1) ≤ 𝑧) |
34 | 33 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧) |
35 | | elfzelz 12636 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) → 𝑧 ∈ ℤ) |
36 | | zltp1le 11756 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)) |
37 | 17, 35, 36 | syl2an 591 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)) |
38 | 34, 37 | mpbird 249 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧) |
39 | | fllt 12903 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) →
((((𝐴 − 1) −
𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)) |
40 | 16, 35, 39 | syl2an 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)) |
41 | 38, 40 | mpbird 249 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧) |
42 | 15 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
43 | 35 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℤ) |
44 | 43 | zred 11811 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℝ) |
45 | 8 | nnred 11368 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
46 | 8 | nngt0d 11401 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
47 | 45, 46 | jca 509 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
48 | 47 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
49 | | ltdivmul2 11231 |
. . . . . . . . . . . 12
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))) |
50 | 42, 44, 48, 49 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))) |
51 | 41, 50 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁)) |
52 | 13 | zred 11811 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 − 1) ∈ ℝ) |
53 | 52 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 − 1) ∈ ℝ) |
54 | 5 | zred 11811 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℝ) |
55 | 54 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℝ) |
56 | 8 | nnzd 11810 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
57 | 56 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∈ ℤ) |
58 | 43, 57 | zmulcld 11817 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℤ) |
59 | 58 | zred 11811 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℝ) |
60 | 53, 55, 59 | ltsubaddd 10949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
61 | 51, 60 | mpbid 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)) |
62 | 11 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐴 ∈ ℤ) |
63 | 5 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℤ) |
64 | 58, 63 | zaddcld 11815 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) |
65 | | zlem1lt 11758 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
66 | 62, 64, 65 | syl2anc 581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
67 | 61, 66 | mpbird 249 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐴 ≤ ((𝑧 · 𝑁) + 𝐶)) |
68 | | elfzle2 12639 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) → 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
69 | 68 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
70 | | flge 12902 |
. . . . . . . . . . . 12
⊢ ((((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) → (𝑧 ≤ ((𝐵 − 𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
71 | 9, 35, 70 | syl2an 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 ≤ ((𝐵 − 𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
72 | 69, 71 | mpbird 249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁)) |
73 | 7 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐵 − 𝐶) ∈ ℝ) |
74 | | lemuldiv 11234 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑧 · 𝑁) ≤ (𝐵 − 𝐶) ↔ 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁))) |
75 | 44, 73, 48, 74 | syl3anc 1496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) ≤ (𝐵 − 𝐶) ↔ 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁))) |
76 | 72, 75 | mpbird 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ≤ (𝐵 − 𝐶)) |
77 | 4 | zred 11811 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
78 | 77 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐵 ∈ ℝ) |
79 | | leaddsub 10829 |
. . . . . . . . . 10
⊢ (((𝑧 · 𝑁) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵 − 𝐶))) |
80 | 59, 55, 78, 79 | syl3anc 1496 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵 − 𝐶))) |
81 | 76, 80 | mpbird 249 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵) |
82 | 4 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐵 ∈ ℤ) |
83 | | elfz 12626 |
. . . . . . . . 9
⊢ ((((𝑧 · 𝑁) + 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵))) |
84 | 64, 62, 82, 83 | syl3anc 1496 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵))) |
85 | 67, 81, 84 | mpbir2and 706 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵)) |
86 | | dvdsmul2 15382 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑧 · 𝑁)) |
87 | 43, 57, 86 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∥ (𝑧 · 𝑁)) |
88 | 58 | zcnd 11812 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℂ) |
89 | 5 | zcnd 11812 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
90 | 89 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℂ) |
91 | 88, 90 | pncand 10715 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) − 𝐶) = (𝑧 · 𝑁)) |
92 | 87, 91 | breqtrrd 4902 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶)) |
93 | | oveq1 6913 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑥 − 𝐶) = (((𝑧 · 𝑁) + 𝐶) − 𝐶)) |
94 | 93 | breq2d 4886 |
. . . . . . . 8
⊢ (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑁 ∥ (𝑥 − 𝐶) ↔ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶))) |
95 | 94 | elrab 3586 |
. . . . . . 7
⊢ (((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ↔ (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶))) |
96 | 85, 92, 95 | sylanbrc 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
97 | 96 | ex 403 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
98 | | oveq1 6913 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐶) = (𝑦 − 𝐶)) |
99 | 98 | breq2d 4886 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑁 ∥ (𝑥 − 𝐶) ↔ 𝑁 ∥ (𝑦 − 𝐶))) |
100 | 99 | elrab 3586 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ↔ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) |
101 | 52 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 − 1) ∈ ℝ) |
102 | | elfzelz 12636 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝑦 ∈ ℤ) |
103 | 102 | ad2antrl 721 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℤ) |
104 | 103 | zred 11811 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℝ) |
105 | 54 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐶 ∈ ℝ) |
106 | | elfzle1 12638 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝐴 ≤ 𝑦) |
107 | 106 | ad2antrl 721 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐴 ≤ 𝑦) |
108 | 11 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐴 ∈ ℤ) |
109 | | zlem1lt 11758 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝐴 ≤ 𝑦 ↔ (𝐴 − 1) < 𝑦)) |
110 | 108, 103,
109 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 ≤ 𝑦 ↔ (𝐴 − 1) < 𝑦)) |
111 | 107, 110 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 − 1) < 𝑦) |
112 | 101, 104,
105, 111 | ltsub1dd 10965 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶)) |
113 | 15 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
114 | 5 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐶 ∈ ℤ) |
115 | 103, 114 | zsubcld 11816 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℤ) |
116 | 115 | zred 11811 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℝ) |
117 | 47 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
118 | | ltdiv1 11218 |
. . . . . . . . . . . 12
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝑦 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁))) |
119 | 113, 116,
117, 118 | syl3anc 1496 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁))) |
120 | 112, 119 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁)) |
121 | 16 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ) |
122 | | simprr 791 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ∥ (𝑦 − 𝐶)) |
123 | 56 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ∈ ℤ) |
124 | 8 | nnne0d 11402 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≠ 0) |
125 | 124 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ≠ 0) |
126 | | dvdsval2 15361 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑦 − 𝐶) ∈ ℤ) → (𝑁 ∥ (𝑦 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ)) |
127 | 123, 125,
115, 126 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑁 ∥ (𝑦 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ)) |
128 | 122, 127 | mpbid 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) |
129 | | fllt 12903 |
. . . . . . . . . . 11
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁))) |
130 | 121, 128,
129 | syl2anc 581 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁))) |
131 | 120, 130 | mpbid 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁)) |
132 | 17 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ) |
133 | | zltp1le 11756 |
. . . . . . . . . 10
⊢
(((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) < ((𝑦 − 𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁))) |
134 | 132, 128,
133 | syl2anc 581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁))) |
135 | 131, 134 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁)) |
136 | 77 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐵 ∈ ℝ) |
137 | | elfzle2 12639 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝑦 ≤ 𝐵) |
138 | 137 | ad2antrl 721 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ≤ 𝐵) |
139 | 104, 136,
105, 138 | lesub1dd 10969 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ≤ (𝐵 − 𝐶)) |
140 | 7 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐵 − 𝐶) ∈ ℝ) |
141 | | lediv1 11219 |
. . . . . . . . . . 11
⊢ (((𝑦 − 𝐶) ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑦 − 𝐶) ≤ (𝐵 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
142 | 116, 140,
117, 141 | syl3anc 1496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) ≤ (𝐵 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
143 | 139, 142 | mpbid 224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) |
144 | 9 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐵 − 𝐶) / 𝑁) ∈ ℝ) |
145 | | flge 12902 |
. . . . . . . . . 10
⊢ ((((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) → (((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
146 | 144, 128,
145 | syl2anc 581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
147 | 143, 146 | mpbid 224 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
148 | 17 | peano2zd 11814 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ) |
149 | 148 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ) |
150 | 10 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℤ) |
151 | | elfz 12626 |
. . . . . . . . 9
⊢ ((((𝑦 − 𝐶) / 𝑁) ∈ ℤ ∧
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) + 1) ∈ ℤ
∧ (⌊‘((𝐵
− 𝐶) / 𝑁)) ∈ ℤ) →
(((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁) ∧ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))))) |
152 | 128, 149,
150, 151 | syl3anc 1496 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁) ∧ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))))) |
153 | 135, 147,
152 | mpbir2and 706 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) |
154 | 153 | ex 403 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)) → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))))) |
155 | 100, 154 | syl5bi 234 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))))) |
156 | 100 | anbi2i 618 |
. . . . . . 7
⊢ ((𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) |
157 | 115 | zcnd 11812 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℂ) |
158 | 157 | adantrl 709 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑦 − 𝐶) ∈ ℂ) |
159 | 43 | zcnd 11812 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℂ) |
160 | 159 | adantrr 710 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑧 ∈ ℂ) |
161 | 8 | nncnd 11369 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
162 | 161 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑁 ∈ ℂ) |
163 | 124 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑁 ≠ 0) |
164 | 158, 160,
162, 163 | divmul3d 11162 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (((𝑦 − 𝐶) / 𝑁) = 𝑧 ↔ (𝑦 − 𝐶) = (𝑧 · 𝑁))) |
165 | 103 | zcnd 11812 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℂ) |
166 | 165 | adantrl 709 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑦 ∈ ℂ) |
167 | 89 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝐶 ∈ ℂ) |
168 | 88 | adantrr 710 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑧 · 𝑁) ∈ ℂ) |
169 | 166, 167,
168 | subadd2d 10733 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → ((𝑦 − 𝐶) = (𝑧 · 𝑁) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)) |
170 | 164, 169 | bitrd 271 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (((𝑦 − 𝐶) / 𝑁) = 𝑧 ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)) |
171 | | eqcom 2833 |
. . . . . . . 8
⊢ (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) = 𝑧) |
172 | | eqcom 2833 |
. . . . . . . 8
⊢ (𝑦 = ((𝑧 · 𝑁) + 𝐶) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦) |
173 | 170, 171,
172 | 3bitr4g 306 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))) |
174 | 156, 173 | sylan2b 589 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))) |
175 | 174 | ex 403 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶)))) |
176 | 29, 32, 97, 155, 175 | en3d 8260 |
. . . 4
⊢ (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
177 | | entr 8275 |
. . . 4
⊢
(((1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) → (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
178 | 28, 176, 177 | syl2anc 581 |
. . 3
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
179 | | fzfi 13067 |
. . . 4
⊢
(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin |
180 | | ssrab2 3913 |
. . . . 5
⊢ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ⊆ (𝐴...𝐵) |
181 | | ssfi 8450 |
. . . . 5
⊢ (((𝐴...𝐵) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ⊆ (𝐴...𝐵)) → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin) |
182 | 30, 180, 181 | mp2an 685 |
. . . 4
⊢ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin |
183 | | hashen 13428 |
. . . 4
⊢
(((1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin) →
((♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
184 | 179, 182,
183 | mp2an 685 |
. . 3
⊢
((♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
185 | 178, 184 | sylibr 226 |
. 2
⊢ (𝜑 →
(♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
186 | | eluzle 11982 |
. . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘(𝐴 − 1)) → (𝐴 − 1) ≤ 𝐵) |
187 | 2, 186 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 − 1) ≤ 𝐵) |
188 | | zre 11709 |
. . . . . . . 8
⊢ ((𝐴 − 1) ∈ ℤ
→ (𝐴 − 1) ∈
ℝ) |
189 | | zre 11709 |
. . . . . . . 8
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
190 | | zre 11709 |
. . . . . . . 8
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℝ) |
191 | | lesub1 10847 |
. . . . . . . 8
⊢ (((𝐴 − 1) ∈ ℝ ∧
𝐵 ∈ ℝ ∧
𝐶 ∈ ℝ) →
((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
192 | 188, 189,
190, 191 | syl3an 1205 |
. . . . . . 7
⊢ (((𝐴 − 1) ∈ ℤ ∧
𝐵 ∈ ℤ ∧
𝐶 ∈ ℤ) →
((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
193 | 13, 4, 5, 192 | syl3anc 1496 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
194 | 187, 193 | mpbid 224 |
. . . . 5
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶)) |
195 | | lediv1 11219 |
. . . . . 6
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
196 | 15, 7, 47, 195 | syl3anc 1496 |
. . . . 5
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
197 | 194, 196 | mpbid 224 |
. . . 4
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) |
198 | | flword2 12910 |
. . . 4
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ ((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
199 | 16, 9, 197, 198 | syl3anc 1496 |
. . 3
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
200 | | uznn0sub 12002 |
. . 3
⊢
((⌊‘((𝐵
− 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) → ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈
ℕ0) |
201 | | hashfz1 13427 |
. . 3
⊢
(((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) ∈ ℕ0
→ (♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
202 | 199, 200,
201 | 3syl 18 |
. 2
⊢ (𝜑 →
(♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
203 | 185, 202 | eqtr3d 2864 |
1
⊢ (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |