Step | Hyp | Ref
| Expression |
1 | | fzodisj 12502 |
. . . . . 6
⊢
((0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁)))) ∩ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)) = ∅ |
2 | 1 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
((0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁)))) ∩ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)) = ∅) |
3 | | rpvmasum.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | 3 | nnnn0d 11351 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
6 | | nn0re 11301 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ℕ0
→ 𝑈 ∈
ℝ) |
7 | 6 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑈 ∈
ℝ) |
8 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑁 ∈
ℕ) |
9 | 7, 8 | nndivred 11069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 / 𝑁) ∈ ℝ) |
10 | 8 | nnrpd 11870 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑁 ∈
ℝ+) |
11 | | nn0ge0 11318 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ℕ0
→ 0 ≤ 𝑈) |
12 | 11 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 0 ≤
𝑈) |
13 | 7, 10, 12 | divge0d 11912 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 0 ≤
(𝑈 / 𝑁)) |
14 | | flge0nn0 12621 |
. . . . . . . . 9
⊢ (((𝑈 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑈 / 𝑁)) → (⌊‘(𝑈 / 𝑁)) ∈
ℕ0) |
15 | 9, 13, 14 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(⌊‘(𝑈 / 𝑁)) ∈
ℕ0) |
16 | 5, 15 | nn0mulcld 11356 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ∈
ℕ0) |
17 | | flle 12600 |
. . . . . . . . 9
⊢ ((𝑈 / 𝑁) ∈ ℝ →
(⌊‘(𝑈 / 𝑁)) ≤ (𝑈 / 𝑁)) |
18 | 9, 17 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(⌊‘(𝑈 / 𝑁)) ≤ (𝑈 / 𝑁)) |
19 | | reflcl 12597 |
. . . . . . . . . 10
⊢ ((𝑈 / 𝑁) ∈ ℝ →
(⌊‘(𝑈 / 𝑁)) ∈
ℝ) |
20 | 9, 19 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(⌊‘(𝑈 / 𝑁)) ∈
ℝ) |
21 | 20, 7, 10 | lemuldiv2d 11922 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈 ↔ (⌊‘(𝑈 / 𝑁)) ≤ (𝑈 / 𝑁))) |
22 | 18, 21 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈) |
23 | | fznn0 12432 |
. . . . . . . 8
⊢ (𝑈 ∈ ℕ0
→ ((𝑁 ·
(⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈) ↔ ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ ℕ0 ∧ (𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈))) |
24 | 23 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈) ↔ ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ ℕ0 ∧ (𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈))) |
25 | 16, 22, 24 | mpbir2and 957 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈)) |
26 | | fzosplit 12501 |
. . . . . 6
⊢ ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈) → (0..^𝑈) = ((0..^(𝑁 · (⌊‘(𝑈 / 𝑁)))) ∪ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈))) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(0..^𝑈) = ((0..^(𝑁 · (⌊‘(𝑈 / 𝑁)))) ∪ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈))) |
28 | | fzofi 12773 |
. . . . . 6
⊢
(0..^𝑈) ∈
Fin |
29 | 28 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(0..^𝑈) ∈
Fin) |
30 | | rpvmasum.g |
. . . . . 6
⊢ 𝐺 = (DChr‘𝑁) |
31 | | rpvmasum.z |
. . . . . 6
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
32 | | rpvmasum.d |
. . . . . 6
⊢ 𝐷 = (Base‘𝐺) |
33 | | rpvmasum.l |
. . . . . 6
⊢ 𝐿 = (ℤRHom‘𝑍) |
34 | | dchrisum.b |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
35 | 34 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^𝑈)) → 𝑋 ∈ 𝐷) |
36 | | elfzoelz 12470 |
. . . . . . 7
⊢ (𝑛 ∈ (0..^𝑈) → 𝑛 ∈ ℤ) |
37 | 36 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^𝑈)) → 𝑛 ∈ ℤ) |
38 | 30, 31, 32, 33, 35, 37 | dchrzrhcl 24970 |
. . . . 5
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^𝑈)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
39 | 2, 27, 29, 38 | fsumsplit 14471 |
. . . 4
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛)) = (Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛)))) |
40 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑁 · 𝑘) = (𝑁 · 0)) |
41 | 40 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · 0))) |
42 | 41 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛))) |
43 | 42 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = 0)) |
44 | 43 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = 0))) |
45 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝑁 · 𝑘) = (𝑁 · 𝑚)) |
46 | 45 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · 𝑚))) |
47 | 46 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛))) |
48 | 47 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0)) |
49 | 48 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0))) |
50 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑚 + 1) → (𝑁 · 𝑘) = (𝑁 · (𝑚 + 1))) |
51 | 50 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑚 + 1) → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · (𝑚 + 1)))) |
52 | 51 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑚 + 1) → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) |
53 | 52 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑘 = (𝑚 + 1) → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0)) |
54 | 53 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑘 = (𝑚 + 1) → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0))) |
55 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → (𝑁 · 𝑘) = (𝑁 · (⌊‘(𝑈 / 𝑁)))) |
56 | 55 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))) |
57 | 56 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛))) |
58 | 57 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0)) |
59 | 58 | imbi2d 330 |
. . . . . . . 8
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0))) |
60 | 3 | nncnd 11036 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
61 | 60 | mul01d 10235 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 · 0) = 0) |
62 | 61 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝜑 → (0..^(𝑁 · 0)) = (0..^0)) |
63 | | fzo0 12492 |
. . . . . . . . . . 11
⊢ (0..^0) =
∅ |
64 | 62, 63 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝜑 → (0..^(𝑁 · 0)) = ∅) |
65 | 64 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ∅ (𝑋‘(𝐿‘𝑛))) |
66 | | sum0 14452 |
. . . . . . . . 9
⊢
Σ𝑛 ∈
∅ (𝑋‘(𝐿‘𝑛)) = 0 |
67 | 65, 66 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = 0) |
68 | | oveq1 6657 |
. . . . . . . . . . 11
⊢
(Σ𝑛 ∈
(0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0 → (Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) = (0 + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)))) |
69 | | fzodisj 12502 |
. . . . . . . . . . . . . 14
⊢
((0..^(𝑁 ·
𝑚)) ∩ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))) = ∅ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((0..^(𝑁 · 𝑚)) ∩ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))) = ∅) |
71 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℝ) |
73 | 72 | lep1d 10955 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ≤ (𝑚 + 1)) |
74 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℝ → (𝑚 + 1) ∈
ℝ) |
75 | 72, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℝ) |
76 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℕ) |
77 | 76 | nnred 11035 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℝ) |
78 | 76 | nngt0d 11064 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 0 <
𝑁) |
79 | | lemul2 10876 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℝ ∧ (𝑚 + 1) ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → (𝑚 ≤ (𝑚 + 1) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) |
80 | 72, 75, 77, 78, 79 | syl112anc 1330 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑚 ≤ (𝑚 + 1) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) |
81 | 73, 80 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1))) |
82 | | nn0mulcl 11329 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑁 · 𝑚) ∈
ℕ0) |
83 | 4, 82 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈
ℕ0) |
84 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . 17
⊢
ℕ0 = (ℤ≥‘0) |
85 | 83, 84 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈
(ℤ≥‘0)) |
86 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) |
87 | | nnmulcl 11043 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ (𝑚 + 1) ∈ ℕ) →
(𝑁 · (𝑚 + 1)) ∈
ℕ) |
88 | 3, 86, 87 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) ∈ ℕ) |
89 | 88 | nnzd 11481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) ∈ ℤ) |
90 | | elfz5 12334 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 · 𝑚) ∈ (ℤ≥‘0)
∧ (𝑁 · (𝑚 + 1)) ∈ ℤ) →
((𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1))) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) |
91 | 85, 89, 90 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1))) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) |
92 | 81, 91 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1)))) |
93 | | fzosplit 12501 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1))) → (0..^(𝑁 · (𝑚 + 1))) = ((0..^(𝑁 · 𝑚)) ∪ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1))))) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(0..^(𝑁 · (𝑚 + 1))) = ((0..^(𝑁 · 𝑚)) ∪ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1))))) |
95 | | fzofi 12773 |
. . . . . . . . . . . . . 14
⊢
(0..^(𝑁 ·
(𝑚 + 1))) ∈
Fin |
96 | 95 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(0..^(𝑁 · (𝑚 + 1))) ∈
Fin) |
97 | 34 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))) → 𝑋 ∈ 𝐷) |
98 | | elfzoelz 12470 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (0..^(𝑁 · (𝑚 + 1))) → 𝑛 ∈ ℤ) |
99 | 98 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))) → 𝑛 ∈ ℤ) |
100 | 30, 31, 32, 33, 97, 99 | dchrzrhcl 24970 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
101 | 70, 94, 96, 100 | fsumsplit 14471 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = (Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)))) |
102 | 76 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℂ) |
103 | 72 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) |
104 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℂ) |
105 | 102, 103,
104 | adddid 10064 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) = ((𝑁 · 𝑚) + (𝑁 · 1))) |
106 | 102 | mulid1d 10057 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 1) = 𝑁) |
107 | 106 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁 · 𝑚) + (𝑁 · 1)) = ((𝑁 · 𝑚) + 𝑁)) |
108 | 105, 107 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) = ((𝑁 · 𝑚) + 𝑁)) |
109 | 108 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1))) = ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))) |
110 | 109 | sumeq1d 14431 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛))) |
111 | 76 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
112 | 83 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈ ℤ) |
113 | 112 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑁 · 𝑚) ∈
ℤ) |
114 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
115 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 · 𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑚) + 𝑘) ∈ ℤ) |
116 | 112, 114,
115 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚) + 𝑘) ∈ ℤ) |
117 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 · 𝑚) + 𝑘) ∈ ℤ → (((𝑁 · 𝑚) + 𝑘) − 1) ∈ ℤ) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑁 · 𝑚) + 𝑘) − 1) ∈ ℤ) |
119 | 34 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) → 𝑋 ∈ 𝐷) |
120 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1)) → 𝑛 ∈ ℤ) |
121 | 120 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) → 𝑛 ∈ ℤ) |
122 | 30, 31, 32, 33, 119, 121 | dchrzrhcl 24970 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
123 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = (𝑖 + (𝑁 · 𝑚)) → (𝐿‘𝑛) = (𝐿‘(𝑖 + (𝑁 · 𝑚)))) |
124 | 123 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑖 + (𝑁 · 𝑚)) → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) |
125 | 113, 113,
118, 122, 124 | fsumshftm 14513 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))(𝑋‘(𝐿‘𝑛)) = Σ𝑖 ∈ (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)))(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) |
126 | | fzoval 12471 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 · 𝑚) + 𝑘) ∈ ℤ → ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) |
127 | 116, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) |
128 | 127 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))(𝑋‘(𝐿‘𝑛))) |
129 | 114 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℤ) |
130 | | fzoval 12471 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ →
(0..^𝑘) = (0...(𝑘 − 1))) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0..^𝑘) =
(0...(𝑘 −
1))) |
132 | 113 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑁 · 𝑚) ∈
ℂ) |
133 | 132 | subidd 10380 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚) − (𝑁 · 𝑚)) = 0) |
134 | 116 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚) + 𝑘) ∈ ℂ) |
135 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 1 ∈ ℂ) |
136 | 134, 135,
132 | sub32d 10424 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)) = ((((𝑁 · 𝑚) + 𝑘) − (𝑁 · 𝑚)) − 1)) |
137 | | nn0cn 11302 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
138 | 137 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℂ) |
139 | 132, 138 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑁 · 𝑚) + 𝑘) − (𝑁 · 𝑚)) = 𝑘) |
140 | 139 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((((𝑁 · 𝑚) + 𝑘) − (𝑁 · 𝑚)) − 1) = (𝑘 − 1)) |
141 | 136, 140 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)) = (𝑘 − 1)) |
142 | 133, 141 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚))) = (0...(𝑘 − 1))) |
143 | 131, 142 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0..^𝑘) = (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)))) |
144 | 143 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = Σ𝑖 ∈ (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)))(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) |
145 | 125, 128,
144 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑖 ∈ (0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) |
146 | 3 | nnzd 11481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈ ℤ) |
147 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) |
148 | | dvdsmul1 15003 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → 𝑁 ∥ (𝑁 · 𝑚)) |
149 | 146, 147,
148 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∥ (𝑁 · 𝑚)) |
150 | 149 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑁 ∥ (𝑁 · 𝑚)) |
151 | | elfzoelz 12470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℤ) |
152 | 151 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑖 ∈ ℤ) |
153 | 152 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑖 ∈ ℂ) |
154 | 132 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝑁 · 𝑚) ∈ ℂ) |
155 | 153, 154 | pncan2d 10394 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → ((𝑖 + (𝑁 · 𝑚)) − 𝑖) = (𝑁 · 𝑚)) |
156 | 150, 155 | breqtrrd 4681 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑁 ∥ ((𝑖 + (𝑁 · 𝑚)) − 𝑖)) |
157 | 111 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑁 ∈
ℕ0) |
158 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ ℤ ∧ (𝑁 · 𝑚) ∈ ℤ) → (𝑖 + (𝑁 · 𝑚)) ∈ ℤ) |
159 | 151, 113,
158 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 + (𝑁 · 𝑚)) ∈ ℤ) |
160 | 31, 33 | zndvds 19898 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ (𝑖 + (𝑁 · 𝑚)) ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝐿‘(𝑖 + (𝑁 · 𝑚))) = (𝐿‘𝑖) ↔ 𝑁 ∥ ((𝑖 + (𝑁 · 𝑚)) − 𝑖))) |
161 | 157, 159,
152, 160 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → ((𝐿‘(𝑖 + (𝑁 · 𝑚))) = (𝐿‘𝑖) ↔ 𝑁 ∥ ((𝑖 + (𝑁 · 𝑚)) − 𝑖))) |
162 | 156, 161 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝐿‘(𝑖 + (𝑁 · 𝑚))) = (𝐿‘𝑖)) |
163 | 162 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = (𝑋‘(𝐿‘𝑖))) |
164 | 163 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = Σ𝑖 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑖))) |
165 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑛 → (𝐿‘𝑖) = (𝐿‘𝑛)) |
166 | 165 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑛 → (𝑋‘(𝐿‘𝑖)) = (𝑋‘(𝐿‘𝑛))) |
167 | 166 | cbvsumv 14426 |
. . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘𝑖)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) |
168 | 164, 167 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) |
169 | 145, 168 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) |
170 | 169 | ralrimiva 2966 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) |
171 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑁 → ((𝑁 · 𝑚) + 𝑘) = ((𝑁 · 𝑚) + 𝑁)) |
172 | 171 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑁 → ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))) |
173 | 172 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑁 → Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛))) |
174 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑁 → (0..^𝑘) = (0..^𝑁)) |
175 | 174 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑁 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛))) |
176 | 173, 175 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑁 → (Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ↔ Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛)))) |
177 | 176 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (∀𝑘 ∈
ℕ0 Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) → Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛)))) |
178 | 111, 170,
177 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛))) |
179 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝐿‘𝑛) → (𝑋‘𝑘) = (𝑋‘(𝐿‘𝑛))) |
180 | 3 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ≠ 0) |
181 | | ifnefalse 4098 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) |
183 | | fzofi 12773 |
. . . . . . . . . . . . . . . . . . 19
⊢
(0..^𝑁) ∈
Fin |
184 | 182, 183 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝑁 = 0, ℤ, (0..^𝑁)) ∈ Fin) |
185 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝑍) =
(Base‘𝑍) |
186 | 33 | reseq1i 5392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑍) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) |
187 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) = if(𝑁 = 0, ℤ, (0..^𝑁)) |
188 | 31, 185, 186, 187 | znf1o 19900 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ (𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑍)) |
189 | 4, 188 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑍)) |
190 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) → ((𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁)))‘𝑛) = (𝐿‘𝑛)) |
191 | 190 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ if(𝑁 = 0, ℤ, (0..^𝑁))) → ((𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁)))‘𝑛) = (𝐿‘𝑛)) |
192 | 30, 31, 32, 185, 34 | dchrf 24967 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) |
193 | 192 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘𝑍)) → (𝑋‘𝑘) ∈ ℂ) |
194 | 179, 184,
189, 191, 193 | fsumf1o 14454 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (Base‘𝑍)(𝑋‘𝑘) = Σ𝑛 ∈ if (𝑁 = 0, ℤ, (0..^𝑁))(𝑋‘(𝐿‘𝑛))) |
195 | | rpvmasum.1 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 =
(0g‘𝐺) |
196 | 30, 31, 32, 195, 34, 185 | dchrsum 24994 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Σ𝑘 ∈ (Base‘𝑍)(𝑋‘𝑘) = if(𝑋 = 1 , (ϕ‘𝑁), 0)) |
197 | | dchrisum.n1 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ≠ 1 ) |
198 | | ifnefalse 4098 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ≠ 1 → if(𝑋 = 1 , (ϕ‘𝑁), 0) = 0) |
199 | 197, 198 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝑋 = 1 , (ϕ‘𝑁), 0) = 0) |
200 | 196, 199 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (Base‘𝑍)(𝑋‘𝑘) = 0) |
201 | 182 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑛 ∈ if (𝑁 = 0, ℤ, (0..^𝑁))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛))) |
202 | 194, 200,
201 | 3eqtr3rd 2665 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛)) = 0) |
203 | 202 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛)) = 0) |
204 | 110, 178,
203 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0) |
205 | 204 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (0 +
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) = (0 + 0)) |
206 | | 00id 10211 |
. . . . . . . . . . . . 13
⊢ (0 + 0) =
0 |
207 | 205, 206 | syl6req 2673 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 0 = (0 +
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)))) |
208 | 101, 207 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(Σ𝑛 ∈
(0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0 ↔ (Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) = (0 + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))))) |
209 | 68, 208 | syl5ibr 236 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(Σ𝑛 ∈
(0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0)) |
210 | 209 | expcom 451 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
→ (𝜑 →
(Σ𝑛 ∈
(0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0))) |
211 | 210 | a2d 29 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ ((𝜑 →
Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0) → (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0))) |
212 | 44, 49, 54, 59, 67, 211 | nn0ind 11472 |
. . . . . . 7
⊢
((⌊‘(𝑈 /
𝑁)) ∈
ℕ0 → (𝜑
→ Σ𝑛 ∈
(0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0)) |
213 | 212 | impcom 446 |
. . . . . 6
⊢ ((𝜑 ∧ (⌊‘(𝑈 / 𝑁)) ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0) |
214 | 15, 213 | syldan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0) |
215 | | modval 12670 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (𝑈 mod 𝑁) = (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁))))) |
216 | 7, 10, 215 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 mod 𝑁) = (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁))))) |
217 | 216 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)) = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁)))))) |
218 | 16 | nn0cnd 11353 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ ℂ) |
219 | | nn0cn 11302 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ ℕ0
→ 𝑈 ∈
ℂ) |
220 | 219 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑈 ∈
ℂ) |
221 | 218, 220 | pncan3d 10395 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁))))) = 𝑈) |
222 | 217, 221 | eqtr2d 2657 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑈 = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁))) |
223 | 222 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈) = ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))) |
224 | 223 | sumeq1d 14431 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛))) |
225 | | nn0z 11400 |
. . . . . . . 8
⊢ (𝑈 ∈ ℕ0
→ 𝑈 ∈
ℤ) |
226 | | zmodcl 12690 |
. . . . . . . 8
⊢ ((𝑈 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑈 mod 𝑁) ∈
ℕ0) |
227 | 225, 3, 226 | syl2anr 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 mod 𝑁) ∈
ℕ0) |
228 | 170 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑚 ∈ ℕ0 ∀𝑘 ∈ ℕ0
Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) |
229 | 228 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
∀𝑚 ∈
ℕ0 ∀𝑘 ∈ ℕ0 Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) |
230 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → (𝑁 · 𝑚) = (𝑁 · (⌊‘(𝑈 / 𝑁)))) |
231 | 230 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → ((𝑁 · 𝑚) + 𝑘) = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘)) |
232 | 230, 231 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))) |
233 | 232 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛))) |
234 | 233 | eqeq1d 2624 |
. . . . . . . 8
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → (Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ↔ Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)))) |
235 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑈 mod 𝑁) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘) = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁))) |
236 | 235 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑈 mod 𝑁) → ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘)) = ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))) |
237 | 236 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝑘 = (𝑈 mod 𝑁) → Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛))) |
238 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑈 mod 𝑁) → (0..^𝑘) = (0..^(𝑈 mod 𝑁))) |
239 | 238 | sumeq1d 14431 |
. . . . . . . . 9
⊢ (𝑘 = (𝑈 mod 𝑁) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) |
240 | 237, 239 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑘 = (𝑈 mod 𝑁) → (Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ↔ Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) |
241 | 234, 240 | rspc2va 3323 |
. . . . . . 7
⊢
((((⌊‘(𝑈
/ 𝑁)) ∈
ℕ0 ∧ (𝑈 mod 𝑁) ∈ ℕ0) ∧
∀𝑚 ∈
ℕ0 ∀𝑘 ∈ ℕ0 Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) → Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) |
242 | 15, 227, 229, 241 | syl21anc 1325 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) |
243 | 224, 242 | eqtrd 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) |
244 | 214, 243 | oveq12d 6668 |
. . . 4
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(Σ𝑛 ∈
(0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛))) = (0 + Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) |
245 | | fzofi 12773 |
. . . . . . 7
⊢
(0..^(𝑈 mod 𝑁)) ∈ Fin |
246 | 245 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(0..^(𝑈 mod 𝑁)) ∈ Fin) |
247 | 34 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑈 mod 𝑁))) → 𝑋 ∈ 𝐷) |
248 | | elfzoelz 12470 |
. . . . . . . 8
⊢ (𝑛 ∈ (0..^(𝑈 mod 𝑁)) → 𝑛 ∈ ℤ) |
249 | 248 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑈 mod 𝑁))) → 𝑛 ∈ ℤ) |
250 | 30, 31, 32, 33, 247, 249 | dchrzrhcl 24970 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑈 mod 𝑁))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
251 | 246, 250 | fsumcl 14464 |
. . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)) ∈ ℂ) |
252 | 251 | addid2d 10237 |
. . . 4
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (0 +
Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) |
253 | 39, 244, 252 | 3eqtrd 2660 |
. . 3
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) |
254 | 253 | fveq2d 6195 |
. 2
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^𝑈)(𝑋‘(𝐿‘𝑛))) = (abs‘Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) |
255 | | zmodfzo 12693 |
. . . 4
⊢ ((𝑈 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑈 mod 𝑁) ∈ (0..^𝑁)) |
256 | 225, 3, 255 | syl2anr 495 |
. . 3
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 mod 𝑁) ∈ (0..^𝑁)) |
257 | | dchrisum.10 |
. . . 4
⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
258 | 257 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
259 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑢 = (𝑈 mod 𝑁) → (0..^𝑢) = (0..^(𝑈 mod 𝑁))) |
260 | 259 | sumeq1d 14431 |
. . . . . 6
⊢ (𝑢 = (𝑈 mod 𝑁) → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) |
261 | 260 | fveq2d 6195 |
. . . . 5
⊢ (𝑢 = (𝑈 mod 𝑁) → (abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) = (abs‘Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) |
262 | 261 | breq1d 4663 |
. . . 4
⊢ (𝑢 = (𝑈 mod 𝑁) → ((abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅 ↔ (abs‘Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)) |
263 | 262 | rspcv 3305 |
. . 3
⊢ ((𝑈 mod 𝑁) ∈ (0..^𝑁) → (∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅 → (abs‘Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)) |
264 | 256, 258,
263 | sylc 65 |
. 2
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |
265 | 254, 264 | eqbrtrd 4675 |
1
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^𝑈)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |