Step | Hyp | Ref
| Expression |
1 | | 1zzd 11285 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
2 | | hashdvds.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘(𝐴 − 1))) |
3 | | eluzelz 11573 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈
(ℤ≥‘(𝐴 − 1)) → 𝐵 ∈ ℤ) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ) |
5 | | hashdvds.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℤ) |
6 | 4, 5 | zsubcld 11363 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ) |
7 | 6 | zred 11358 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℝ) |
8 | | hashdvds.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | 7, 8 | nndivred 10946 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐶) / 𝑁) ∈ ℝ) |
10 | 9 | flcld 12461 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℤ) |
11 | | hashdvds.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
12 | | peano2zm 11297 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 1) ∈ ℤ) |
14 | 13, 5 | zsubcld 11363 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℤ) |
15 | 14 | zred 11358 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
16 | 15, 8 | nndivred 10946 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ) |
17 | 16 | flcld 12461 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ) |
18 | 10, 17 | zsubcld 11363 |
. . . . . 6
⊢ (𝜑 → ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ) |
19 | | fzen 12229 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ ∧
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)) ∈ ℤ) →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) |
20 | 1, 18, 17, 19 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) |
21 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
22 | 17 | zcnd 11359 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) |
23 | | addcom 10101 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) → (1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)) |
24 | 21, 22, 23 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → (1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)) |
25 | 10 | zcnd 11359 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℂ) |
26 | 25, 22 | npcand 10275 |
. . . . . 6
⊢ (𝜑 → (((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = (⌊‘((𝐵 − 𝐶) / 𝑁))) |
27 | 24, 26 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) = (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) |
28 | 20, 27 | breqtrd 4609 |
. . . 4
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁)))) |
29 | | ovex 6577 |
. . . . . 6
⊢
(((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∈ V |
30 | 29 | a1i 11 |
. . . . 5
⊢ (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∈ V) |
31 | | fzfi 12633 |
. . . . . 6
⊢ (𝐴...𝐵) ∈ Fin |
32 | | rabexg 4739 |
. . . . . 6
⊢ ((𝐴...𝐵) ∈ Fin → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ V) |
33 | 31, 32 | mp1i 13 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ V) |
34 | | elfzle1 12215 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) + 1) ≤ 𝑧) |
35 | 34 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧) |
36 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) → 𝑧 ∈ ℤ) |
37 | | zltp1le 11304 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)) |
38 | 17, 36, 37 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)) |
39 | 35, 38 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧) |
40 | | fllt 12469 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) →
((((𝐴 − 1) −
𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)) |
41 | 16, 36, 40 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)) |
42 | 39, 41 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧) |
43 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
44 | 36 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℤ) |
45 | 44 | zred 11358 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℝ) |
46 | 8 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
47 | 8 | nngt0d 10941 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
48 | 46, 47 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
49 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
50 | | ltdivmul2 10779 |
. . . . . . . . . . . 12
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))) |
51 | 43, 45, 49, 50 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))) |
52 | 42, 51 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁)) |
53 | 13 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 − 1) ∈ ℝ) |
54 | 53 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 − 1) ∈ ℝ) |
55 | 5 | zred 11358 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℝ) |
56 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℝ) |
57 | 8 | nnzd 11357 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∈ ℤ) |
59 | 44, 58 | zmulcld 11364 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℤ) |
60 | 59 | zred 11358 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℝ) |
61 | 54, 56, 60 | ltsubaddd 10502 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
62 | 52, 61 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)) |
63 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐴 ∈ ℤ) |
64 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℤ) |
65 | 59, 64 | zaddcld 11362 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) |
66 | | zlem1lt 11306 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
67 | 63, 65, 66 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
68 | 62, 67 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐴 ≤ ((𝑧 · 𝑁) + 𝐶)) |
69 | | elfzle2 12216 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) → 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
70 | 69 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
71 | | flge 12468 |
. . . . . . . . . . . 12
⊢ ((((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) → (𝑧 ≤ ((𝐵 − 𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
72 | 9, 36, 71 | syl2an 493 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 ≤ ((𝐵 − 𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
73 | 70, 72 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁)) |
74 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐵 − 𝐶) ∈ ℝ) |
75 | | lemuldiv 10782 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑧 · 𝑁) ≤ (𝐵 − 𝐶) ↔ 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁))) |
76 | 45, 74, 49, 75 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) ≤ (𝐵 − 𝐶) ↔ 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁))) |
77 | 73, 76 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ≤ (𝐵 − 𝐶)) |
78 | 4 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
79 | 78 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐵 ∈ ℝ) |
80 | | leaddsub 10383 |
. . . . . . . . . 10
⊢ (((𝑧 · 𝑁) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵 − 𝐶))) |
81 | 60, 56, 79, 80 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵 − 𝐶))) |
82 | 77, 81 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵) |
83 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐵 ∈ ℤ) |
84 | | elfz 12203 |
. . . . . . . . 9
⊢ ((((𝑧 · 𝑁) + 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵))) |
85 | 65, 63, 83, 84 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵))) |
86 | 68, 82, 85 | mpbir2and 959 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵)) |
87 | | dvdsmul2 14842 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑧 · 𝑁)) |
88 | 44, 58, 87 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∥ (𝑧 · 𝑁)) |
89 | 59 | zcnd 11359 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℂ) |
90 | 5 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
91 | 90 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℂ) |
92 | 89, 91 | pncand 10272 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) − 𝐶) = (𝑧 · 𝑁)) |
93 | 88, 92 | breqtrrd 4611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶)) |
94 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑥 − 𝐶) = (((𝑧 · 𝑁) + 𝐶) − 𝐶)) |
95 | 94 | breq2d 4595 |
. . . . . . . 8
⊢ (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑁 ∥ (𝑥 − 𝐶) ↔ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶))) |
96 | 95 | elrab 3331 |
. . . . . . 7
⊢ (((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ↔ (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶))) |
97 | 86, 93, 96 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
98 | 97 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
99 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐶) = (𝑦 − 𝐶)) |
100 | 99 | breq2d 4595 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑁 ∥ (𝑥 − 𝐶) ↔ 𝑁 ∥ (𝑦 − 𝐶))) |
101 | 100 | elrab 3331 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ↔ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) |
102 | 53 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 − 1) ∈ ℝ) |
103 | | elfzelz 12213 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝑦 ∈ ℤ) |
104 | 103 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℤ) |
105 | 104 | zred 11358 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℝ) |
106 | 55 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐶 ∈ ℝ) |
107 | | elfzle1 12215 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝐴 ≤ 𝑦) |
108 | 107 | ad2antrl 760 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐴 ≤ 𝑦) |
109 | 11 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐴 ∈ ℤ) |
110 | | zlem1lt 11306 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝐴 ≤ 𝑦 ↔ (𝐴 − 1) < 𝑦)) |
111 | 109, 104,
110 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 ≤ 𝑦 ↔ (𝐴 − 1) < 𝑦)) |
112 | 108, 111 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 − 1) < 𝑦) |
113 | 102, 105,
106, 112 | ltsub1dd 10518 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶)) |
114 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
115 | 5 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐶 ∈ ℤ) |
116 | 104, 115 | zsubcld 11363 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℤ) |
117 | 116 | zred 11358 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℝ) |
118 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
119 | | ltdiv1 10766 |
. . . . . . . . . . . 12
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝑦 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁))) |
120 | 114, 117,
118, 119 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁))) |
121 | 113, 120 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁)) |
122 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ) |
123 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ∥ (𝑦 − 𝐶)) |
124 | 57 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ∈ ℤ) |
125 | 8 | nnne0d 10942 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≠ 0) |
126 | 125 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ≠ 0) |
127 | | dvdsval2 14824 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑦 − 𝐶) ∈ ℤ) → (𝑁 ∥ (𝑦 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ)) |
128 | 124, 126,
116, 127 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑁 ∥ (𝑦 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ)) |
129 | 123, 128 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) |
130 | | fllt 12469 |
. . . . . . . . . . 11
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁))) |
131 | 122, 129,
130 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁))) |
132 | 121, 131 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁)) |
133 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ) |
134 | | zltp1le 11304 |
. . . . . . . . . 10
⊢
(((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) < ((𝑦 − 𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁))) |
135 | 133, 129,
134 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁))) |
136 | 132, 135 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁)) |
137 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐵 ∈ ℝ) |
138 | | elfzle2 12216 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝑦 ≤ 𝐵) |
139 | 138 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ≤ 𝐵) |
140 | 105, 137,
106, 139 | lesub1dd 10522 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ≤ (𝐵 − 𝐶)) |
141 | 7 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐵 − 𝐶) ∈ ℝ) |
142 | | lediv1 10767 |
. . . . . . . . . . 11
⊢ (((𝑦 − 𝐶) ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑦 − 𝐶) ≤ (𝐵 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
143 | 117, 141,
118, 142 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) ≤ (𝐵 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
144 | 140, 143 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) |
145 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐵 − 𝐶) / 𝑁) ∈ ℝ) |
146 | | flge 12468 |
. . . . . . . . . 10
⊢ ((((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) → (((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
147 | 145, 129,
146 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
148 | 144, 147 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
149 | 17 | peano2zd 11361 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ) |
150 | 149 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ) |
151 | 10 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℤ) |
152 | | elfz 12203 |
. . . . . . . . 9
⊢ ((((𝑦 − 𝐶) / 𝑁) ∈ ℤ ∧
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) + 1) ∈ ℤ
∧ (⌊‘((𝐵
− 𝐶) / 𝑁)) ∈ ℤ) →
(((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁) ∧ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))))) |
153 | 129, 150,
151, 152 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁) ∧ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))))) |
154 | 136, 148,
153 | mpbir2and 959 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) |
155 | 154 | ex 449 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)) → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))))) |
156 | 101, 155 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))))) |
157 | 101 | anbi2i 726 |
. . . . . . 7
⊢ ((𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) |
158 | 116 | zcnd 11359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℂ) |
159 | 158 | adantrl 748 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑦 − 𝐶) ∈ ℂ) |
160 | 44 | zcnd 11359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℂ) |
161 | 160 | adantrr 749 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑧 ∈ ℂ) |
162 | 8 | nncnd 10913 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
163 | 162 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑁 ∈ ℂ) |
164 | 125 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑁 ≠ 0) |
165 | 159, 161,
163, 164 | divmul3d 10714 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (((𝑦 − 𝐶) / 𝑁) = 𝑧 ↔ (𝑦 − 𝐶) = (𝑧 · 𝑁))) |
166 | 104 | zcnd 11359 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℂ) |
167 | 166 | adantrl 748 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑦 ∈ ℂ) |
168 | 90 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝐶 ∈ ℂ) |
169 | 89 | adantrr 749 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑧 · 𝑁) ∈ ℂ) |
170 | 167, 168,
169 | subadd2d 10290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → ((𝑦 − 𝐶) = (𝑧 · 𝑁) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)) |
171 | 165, 170 | bitrd 267 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (((𝑦 − 𝐶) / 𝑁) = 𝑧 ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)) |
172 | | eqcom 2617 |
. . . . . . . 8
⊢ (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) = 𝑧) |
173 | | eqcom 2617 |
. . . . . . . 8
⊢ (𝑦 = ((𝑧 · 𝑁) + 𝐶) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦) |
174 | 171, 172,
173 | 3bitr4g 302 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))) |
175 | 157, 174 | sylan2b 491 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))) |
176 | 175 | ex 449 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶)))) |
177 | 30, 33, 98, 156, 176 | en3d 7878 |
. . . 4
⊢ (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
178 | | entr 7894 |
. . . 4
⊢
(((1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) → (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
179 | 28, 177, 178 | syl2anc 691 |
. . 3
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
180 | | fzfi 12633 |
. . . 4
⊢
(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin |
181 | | ssrab2 3650 |
. . . . 5
⊢ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ⊆ (𝐴...𝐵) |
182 | | ssfi 8065 |
. . . . 5
⊢ (((𝐴...𝐵) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ⊆ (𝐴...𝐵)) → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin) |
183 | 31, 181, 182 | mp2an 704 |
. . . 4
⊢ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin |
184 | | hashen 12997 |
. . . 4
⊢
(((1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin) →
((#‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (#‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
185 | 180, 183,
184 | mp2an 704 |
. . 3
⊢
((#‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (#‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
186 | 179, 185 | sylibr 223 |
. 2
⊢ (𝜑 →
(#‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (#‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
187 | | eluzle 11576 |
. . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘(𝐴 − 1)) → (𝐴 − 1) ≤ 𝐵) |
188 | 2, 187 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 − 1) ≤ 𝐵) |
189 | | zre 11258 |
. . . . . . . 8
⊢ ((𝐴 − 1) ∈ ℤ
→ (𝐴 − 1) ∈
ℝ) |
190 | | zre 11258 |
. . . . . . . 8
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
191 | | zre 11258 |
. . . . . . . 8
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℝ) |
192 | | lesub1 10401 |
. . . . . . . 8
⊢ (((𝐴 − 1) ∈ ℝ ∧
𝐵 ∈ ℝ ∧
𝐶 ∈ ℝ) →
((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
193 | 189, 190,
191, 192 | syl3an 1360 |
. . . . . . 7
⊢ (((𝐴 − 1) ∈ ℤ ∧
𝐵 ∈ ℤ ∧
𝐶 ∈ ℤ) →
((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
194 | 13, 4, 5, 193 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
195 | 188, 194 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶)) |
196 | | lediv1 10767 |
. . . . . 6
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
197 | 15, 7, 48, 196 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
198 | 195, 197 | mpbid 221 |
. . . 4
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) |
199 | | flword2 12476 |
. . . 4
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ ((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
200 | 16, 9, 198, 199 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
201 | | uznn0sub 11595 |
. . 3
⊢
((⌊‘((𝐵
− 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) → ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈
ℕ0) |
202 | | hashfz1 12996 |
. . 3
⊢
(((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) ∈ ℕ0
→ (#‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
203 | 200, 201,
202 | 3syl 18 |
. 2
⊢ (𝜑 →
(#‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
204 | 186, 203 | eqtr3d 2646 |
1
⊢ (𝜑 → (#‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |