Step | Hyp | Ref
| Expression |
1 | | 1zzd 12005 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
2 | | hashdvds.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘(𝐴 − 1))) |
3 | | eluzelz 12245 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈
(ℤ≥‘(𝐴 − 1)) → 𝐵 ∈ ℤ) |
4 | 2, 3 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℤ) |
5 | | hashdvds.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℤ) |
6 | 4, 5 | zsubcld 12084 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℤ) |
7 | 6 | zred 12079 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − 𝐶) ∈ ℝ) |
8 | | hashdvds.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | 7, 8 | nndivred 11683 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − 𝐶) / 𝑁) ∈ ℝ) |
10 | 9 | flcld 13160 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℤ) |
11 | | hashdvds.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
12 | | peano2zm 12017 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℤ → (𝐴 − 1) ∈
ℤ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 − 1) ∈ ℤ) |
14 | 13, 5 | zsubcld 12084 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℤ) |
15 | 14 | zred 12079 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
16 | 15, 8 | nndivred 11683 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ∈ ℝ) |
17 | 16 | flcld 13160 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ) |
18 | 10, 17 | zsubcld 12084 |
. . . . . 6
⊢ (𝜑 → ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ) |
19 | | fzen 12916 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈ ℤ ∧
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)) ∈ ℤ) →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) |
20 | 1, 18, 17, 19 | syl3anc 1366 |
. . . . 5
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) |
21 | | ax-1cn 10587 |
. . . . . . 7
⊢ 1 ∈
ℂ |
22 | 17 | zcnd 12080 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) |
23 | | addcom 10818 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℂ) → (1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)) |
24 | 21, 22, 23 | sylancr 589 |
. . . . . 6
⊢ (𝜑 → (1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) = ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)) |
25 | 10 | zcnd 12080 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℂ) |
26 | 25, 22 | npcand 10993 |
. . . . . 6
⊢ (𝜑 → (((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) = (⌊‘((𝐵 − 𝐶) / 𝑁))) |
27 | 24, 26 | oveq12d 7166 |
. . . . 5
⊢ (𝜑 → ((1 +
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))...(((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) + (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) = (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) |
28 | 20, 27 | breqtrd 5083 |
. . . 4
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁)))) |
29 | | ovexd 7183 |
. . . . 5
⊢ (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∈ V) |
30 | | fzfi 13332 |
. . . . . 6
⊢ (𝐴...𝐵) ∈ Fin |
31 | | rabexg 5225 |
. . . . . 6
⊢ ((𝐴...𝐵) ∈ Fin → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ V) |
32 | 30, 31 | mp1i 13 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ V) |
33 | | oveq1 7155 |
. . . . . . . 8
⊢ (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑥 − 𝐶) = (((𝑧 · 𝑁) + 𝐶) − 𝐶)) |
34 | 33 | breq2d 5069 |
. . . . . . 7
⊢ (𝑥 = ((𝑧 · 𝑁) + 𝐶) → (𝑁 ∥ (𝑥 − 𝐶) ↔ 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶))) |
35 | | elfzle1 12902 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) + 1) ≤ 𝑧) |
36 | 35 | adantl 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧) |
37 | | elfzelz 12900 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) → 𝑧 ∈ ℤ) |
38 | | zltp1le 12024 |
. . . . . . . . . . . . . 14
⊢
(((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ 𝑧 ∈ ℤ) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)) |
39 | 17, 37, 38 | syl2an 597 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧 ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ 𝑧)) |
40 | 36, 39 | mpbird 259 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧) |
41 | | fllt 13168 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) →
((((𝐴 − 1) −
𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)) |
42 | 16, 37, 41 | syl2an 597 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < 𝑧)) |
43 | 40, 42 | mpbird 259 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧) |
44 | 15 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
45 | 37 | adantl 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℤ) |
46 | 45 | zred 12079 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℝ) |
47 | 8 | nnred 11645 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) |
48 | 8 | nngt0d 11678 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
49 | 47, 48 | jca 514 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
50 | 49 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
51 | | ltdivmul2 11509 |
. . . . . . . . . . . 12
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 <
𝑁)) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))) |
52 | 44, 46, 50, 51 | syl3anc 1366 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < 𝑧 ↔ ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁))) |
53 | 43, 52 | mpbid 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁)) |
54 | 13 | zred 12079 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 − 1) ∈ ℝ) |
55 | 54 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 − 1) ∈ ℝ) |
56 | 5 | zred 12079 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ℝ) |
57 | 56 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℝ) |
58 | 8 | nnzd 12078 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℤ) |
59 | 58 | adantr 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∈ ℤ) |
60 | 45, 59 | zmulcld 12085 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℤ) |
61 | 60 | zred 12079 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℝ) |
62 | 55, 57, 61 | ltsubaddd 11228 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝐴 − 1) − 𝐶) < (𝑧 · 𝑁) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
63 | 53, 62 | mpbid 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶)) |
64 | 5 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℤ) |
65 | 60, 64 | zaddcld 12083 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) |
66 | | zlem1lt 12026 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ ((𝑧 · 𝑁) + 𝐶) ∈ ℤ) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
67 | 11, 65, 66 | syl2an2r 683 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ↔ (𝐴 − 1) < ((𝑧 · 𝑁) + 𝐶))) |
68 | 63, 67 | mpbird 259 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐴 ≤ ((𝑧 · 𝑁) + 𝐶)) |
69 | | elfzle2 12903 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) → 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
70 | 69 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
71 | | flge 13167 |
. . . . . . . . . . . 12
⊢ ((((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ 𝑧 ∈ ℤ) → (𝑧 ≤ ((𝐵 − 𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
72 | 9, 37, 71 | syl2an 597 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 ≤ ((𝐵 − 𝐶) / 𝑁) ↔ 𝑧 ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
73 | 70, 72 | mpbird 259 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁)) |
74 | 7 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝐵 − 𝐶) ∈ ℝ) |
75 | | lemuldiv 11512 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑧 · 𝑁) ≤ (𝐵 − 𝐶) ↔ 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁))) |
76 | 46, 74, 50, 75 | syl3anc 1366 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) ≤ (𝐵 − 𝐶) ↔ 𝑧 ≤ ((𝐵 − 𝐶) / 𝑁))) |
77 | 73, 76 | mpbird 259 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ≤ (𝐵 − 𝐶)) |
78 | 4 | zred 12079 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) |
79 | 78 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐵 ∈ ℝ) |
80 | | leaddsub 11108 |
. . . . . . . . . 10
⊢ (((𝑧 · 𝑁) ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵 − 𝐶))) |
81 | 61, 57, 79, 80 | syl3anc 1366 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ≤ 𝐵 ↔ (𝑧 · 𝑁) ≤ (𝐵 − 𝐶))) |
82 | 77, 81 | mpbird 259 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵) |
83 | 11 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐴 ∈ ℤ) |
84 | 4 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐵 ∈ ℤ) |
85 | | elfz 12890 |
. . . . . . . . 9
⊢ ((((𝑧 · 𝑁) + 𝐶) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵))) |
86 | 65, 83, 84, 85 | syl3anc 1366 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵) ↔ (𝐴 ≤ ((𝑧 · 𝑁) + 𝐶) ∧ ((𝑧 · 𝑁) + 𝐶) ≤ 𝐵))) |
87 | 68, 82, 86 | mpbir2and 711 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ (𝐴...𝐵)) |
88 | | dvdsmul2 15624 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑧 · 𝑁)) |
89 | 45, 59, 88 | syl2anc 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∥ (𝑧 · 𝑁)) |
90 | 60 | zcnd 12080 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (𝑧 · 𝑁) ∈ ℂ) |
91 | 5 | zcnd 12080 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℂ) |
92 | 91 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝐶 ∈ ℂ) |
93 | 90, 92 | pncand 10990 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → (((𝑧 · 𝑁) + 𝐶) − 𝐶) = (𝑧 · 𝑁)) |
94 | 89, 93 | breqtrrd 5085 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑁 ∥ (((𝑧 · 𝑁) + 𝐶) − 𝐶)) |
95 | 34, 87, 94 | elrabd 3680 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
96 | 95 | ex 415 |
. . . . 5
⊢ (𝜑 → (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) → ((𝑧 · 𝑁) + 𝐶) ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
97 | | oveq1 7155 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 − 𝐶) = (𝑦 − 𝐶)) |
98 | 97 | breq2d 5069 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑁 ∥ (𝑥 − 𝐶) ↔ 𝑁 ∥ (𝑦 − 𝐶))) |
99 | 98 | elrab 3678 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ↔ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) |
100 | 54 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 − 1) ∈ ℝ) |
101 | | elfzelz 12900 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝑦 ∈ ℤ) |
102 | 101 | ad2antrl 726 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℤ) |
103 | 102 | zred 12079 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℝ) |
104 | 56 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐶 ∈ ℝ) |
105 | | elfzle1 12902 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝐴 ≤ 𝑦) |
106 | 105 | ad2antrl 726 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐴 ≤ 𝑦) |
107 | | zlem1lt 12026 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝑦 ∈ ℤ) → (𝐴 ≤ 𝑦 ↔ (𝐴 − 1) < 𝑦)) |
108 | 11, 102, 107 | syl2an2r 683 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 ≤ 𝑦 ↔ (𝐴 − 1) < 𝑦)) |
109 | 106, 108 | mpbid 234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐴 − 1) < 𝑦) |
110 | 100, 103,
104, 109 | ltsub1dd 11244 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶)) |
111 | 15 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝐴 − 1) − 𝐶) ∈ ℝ) |
112 | 5 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐶 ∈ ℤ) |
113 | 102, 112 | zsubcld 12084 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℤ) |
114 | 113 | zred 12079 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℝ) |
115 | 49 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑁 ∈ ℝ ∧ 0 < 𝑁)) |
116 | | ltdiv1 11496 |
. . . . . . . . . . . 12
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝑦 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁))) |
117 | 111, 114,
115, 116 | syl3anc 1366 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) < (𝑦 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁))) |
118 | 110, 117 | mpbid 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁)) |
119 | | simprr 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ∥ (𝑦 − 𝐶)) |
120 | 58 | adantr 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ∈ ℤ) |
121 | 8 | nnne0d 11679 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ≠ 0) |
122 | 121 | adantr 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑁 ≠ 0) |
123 | | dvdsval2 15602 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ∧ (𝑦 − 𝐶) ∈ ℤ) → (𝑁 ∥ (𝑦 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ)) |
124 | 120, 122,
113, 123 | syl3anc 1366 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑁 ∥ (𝑦 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ)) |
125 | 119, 124 | mpbid 234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) |
126 | | fllt 13168 |
. . . . . . . . . . 11
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁))) |
127 | 16, 125, 126 | syl2an2r 683 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((((𝐴 − 1) − 𝐶) / 𝑁) < ((𝑦 − 𝐶) / 𝑁) ↔ (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁))) |
128 | 118, 127 | mpbid 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁)) |
129 | | zltp1le 12024 |
. . . . . . . . . 10
⊢
(((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) ∈ ℤ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) →
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) < ((𝑦 − 𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁))) |
130 | 17, 125, 129 | syl2an2r 683 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) < ((𝑦 − 𝐶) / 𝑁) ↔ ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁))) |
131 | 128, 130 | mpbid 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁)) |
132 | 78 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝐵 ∈ ℝ) |
133 | | elfzle2 12903 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝑦 ≤ 𝐵) |
134 | 133 | ad2antrl 726 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ≤ 𝐵) |
135 | 103, 132,
104, 134 | lesub1dd 11248 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ≤ (𝐵 − 𝐶)) |
136 | 7 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝐵 − 𝐶) ∈ ℝ) |
137 | | lediv1 11497 |
. . . . . . . . . . 11
⊢ (((𝑦 − 𝐶) ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → ((𝑦 − 𝐶) ≤ (𝐵 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
138 | 114, 136,
115, 137 | syl3anc 1366 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) ≤ (𝐵 − 𝐶) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
139 | 135, 138 | mpbid 234 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) |
140 | | flge 13167 |
. . . . . . . . . 10
⊢ ((((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ ((𝑦 − 𝐶) / 𝑁) ∈ ℤ) → (((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
141 | 9, 125, 140 | syl2an2r 683 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝑦 − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁)))) |
142 | 139, 141 | mpbid 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))) |
143 | 17 | peano2zd 12082 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ) |
144 | 143 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ∈ ℤ) |
145 | 10 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈ ℤ) |
146 | | elfz 12890 |
. . . . . . . . 9
⊢ ((((𝑦 − 𝐶) / 𝑁) ∈ ℤ ∧
((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) + 1) ∈ ℤ
∧ (⌊‘((𝐵
− 𝐶) / 𝑁)) ∈ ℤ) →
(((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁) ∧ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))))) |
147 | 125, 144,
145, 146 | syl3anc 1366 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ↔ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1) ≤ ((𝑦 − 𝐶) / 𝑁) ∧ ((𝑦 − 𝐶) / 𝑁) ≤ (⌊‘((𝐵 − 𝐶) / 𝑁))))) |
148 | 131, 142,
147 | mpbir2and 711 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) |
149 | 148 | ex 415 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)) → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))))) |
150 | 99, 149 | syl5bi 244 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} → ((𝑦 − 𝐶) / 𝑁) ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))))) |
151 | 99 | anbi2i 624 |
. . . . . . 7
⊢ ((𝑧 ∈
(((⌊‘(((𝐴
− 1) − 𝐶) /
𝑁)) +
1)...(⌊‘((𝐵
− 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) |
152 | 113 | zcnd 12080 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → (𝑦 − 𝐶) ∈ ℂ) |
153 | 152 | adantrl 714 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑦 − 𝐶) ∈ ℂ) |
154 | 45 | zcnd 12080 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁)))) → 𝑧 ∈ ℂ) |
155 | 154 | adantrr 715 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑧 ∈ ℂ) |
156 | 8 | nncnd 11646 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
157 | 156 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑁 ∈ ℂ) |
158 | 121 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑁 ≠ 0) |
159 | 153, 155,
157, 158 | divmul3d 11442 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (((𝑦 − 𝐶) / 𝑁) = 𝑧 ↔ (𝑦 − 𝐶) = (𝑧 · 𝑁))) |
160 | 102 | zcnd 12080 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶))) → 𝑦 ∈ ℂ) |
161 | 160 | adantrl 714 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝑦 ∈ ℂ) |
162 | 91 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → 𝐶 ∈ ℂ) |
163 | 90 | adantrr 715 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑧 · 𝑁) ∈ ℂ) |
164 | 161, 162,
163 | subadd2d 11008 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → ((𝑦 − 𝐶) = (𝑧 · 𝑁) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)) |
165 | 159, 164 | bitrd 281 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (((𝑦 − 𝐶) / 𝑁) = 𝑧 ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦)) |
166 | | eqcom 2826 |
. . . . . . . 8
⊢ (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ ((𝑦 − 𝐶) / 𝑁) = 𝑧) |
167 | | eqcom 2826 |
. . . . . . . 8
⊢ (𝑦 = ((𝑧 · 𝑁) + 𝐶) ↔ ((𝑧 · 𝑁) + 𝐶) = 𝑦) |
168 | 165, 166,
167 | 3bitr4g 316 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (𝑦 ∈ (𝐴...𝐵) ∧ 𝑁 ∥ (𝑦 − 𝐶)))) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))) |
169 | 151, 168 | sylan2b 595 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶))) |
170 | 169 | ex 415 |
. . . . 5
⊢ (𝜑 → ((𝑧 ∈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ 𝑦 ∈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) → (𝑧 = ((𝑦 − 𝐶) / 𝑁) ↔ 𝑦 = ((𝑧 · 𝑁) + 𝐶)))) |
171 | 29, 32, 96, 150, 170 | en3d 8538 |
. . . 4
⊢ (𝜑 → (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
172 | | entr 8553 |
. . . 4
⊢
(((1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ∧ (((⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)) + 1)...(⌊‘((𝐵 − 𝐶) / 𝑁))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) → (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
173 | 28, 171, 172 | syl2anc 586 |
. . 3
⊢ (𝜑 →
(1...((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
174 | | fzfi 13332 |
. . . 4
⊢
(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin |
175 | | ssrab2 4054 |
. . . . 5
⊢ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ⊆ (𝐴...𝐵) |
176 | | ssfi 8730 |
. . . . 5
⊢ (((𝐴...𝐵) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ⊆ (𝐴...𝐵)) → {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin) |
177 | 30, 175, 176 | mp2an 690 |
. . . 4
⊢ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin |
178 | | hashen 13699 |
. . . 4
⊢
(((1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ∈ Fin ∧ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)} ∈ Fin) →
((♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
179 | 174, 177,
178 | mp2an 690 |
. . 3
⊢
((♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) ↔ (1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) ≈ {𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) |
180 | 173, 179 | sylibr 236 |
. 2
⊢ (𝜑 →
(♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)})) |
181 | | eluzle 12248 |
. . . . . . 7
⊢ (𝐵 ∈
(ℤ≥‘(𝐴 − 1)) → (𝐴 − 1) ≤ 𝐵) |
182 | 2, 181 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 − 1) ≤ 𝐵) |
183 | | zre 11977 |
. . . . . . . 8
⊢ ((𝐴 − 1) ∈ ℤ
→ (𝐴 − 1) ∈
ℝ) |
184 | | zre 11977 |
. . . . . . . 8
⊢ (𝐵 ∈ ℤ → 𝐵 ∈
ℝ) |
185 | | zre 11977 |
. . . . . . . 8
⊢ (𝐶 ∈ ℤ → 𝐶 ∈
ℝ) |
186 | | lesub1 11126 |
. . . . . . . 8
⊢ (((𝐴 − 1) ∈ ℝ ∧
𝐵 ∈ ℝ ∧
𝐶 ∈ ℝ) →
((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
187 | 183, 184,
185, 186 | syl3an 1155 |
. . . . . . 7
⊢ (((𝐴 − 1) ∈ ℤ ∧
𝐵 ∈ ℤ ∧
𝐶 ∈ ℤ) →
((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
188 | 13, 4, 5, 187 | syl3anc 1366 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 1) ≤ 𝐵 ↔ ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶))) |
189 | 182, 188 | mpbid 234 |
. . . . 5
⊢ (𝜑 → ((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶)) |
190 | | lediv1 11497 |
. . . . . 6
⊢ ((((𝐴 − 1) − 𝐶) ∈ ℝ ∧ (𝐵 − 𝐶) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
191 | 15, 7, 49, 190 | syl3anc 1366 |
. . . . 5
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) ≤ (𝐵 − 𝐶) ↔ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁))) |
192 | 189, 191 | mpbid 234 |
. . . 4
⊢ (𝜑 → (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) |
193 | | flword2 13175 |
. . . 4
⊢
(((((𝐴 − 1)
− 𝐶) / 𝑁) ∈ ℝ ∧ ((𝐵 − 𝐶) / 𝑁) ∈ ℝ ∧ (((𝐴 − 1) − 𝐶) / 𝑁) ≤ ((𝐵 − 𝐶) / 𝑁)) → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
194 | 16, 9, 192, 193 | syl3anc 1366 |
. . 3
⊢ (𝜑 → (⌊‘((𝐵 − 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
195 | | uznn0sub 12269 |
. . 3
⊢
((⌊‘((𝐵
− 𝐶) / 𝑁)) ∈
(ℤ≥‘(⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) → ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))) ∈
ℕ0) |
196 | | hashfz1 13698 |
. . 3
⊢
(((⌊‘((𝐵
− 𝐶) / 𝑁)) −
(⌊‘(((𝐴 −
1) − 𝐶) / 𝑁))) ∈ ℕ0
→ (♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
197 | 194, 195,
196 | 3syl 18 |
. 2
⊢ (𝜑 →
(♯‘(1...((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |
198 | 180, 197 | eqtr3d 2856 |
1
⊢ (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁)))) |