| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzodisj 13734 | . . . . . 6
⊢
((0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁)))) ∩ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)) = ∅ | 
| 2 | 1 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
((0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁)))) ∩ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)) = ∅) | 
| 3 |  | rpvmasum.a | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 4 | 3 | nnnn0d 12589 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 5 | 4 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑁 ∈
ℕ0) | 
| 6 |  | nn0re 12537 | . . . . . . . . . . 11
⊢ (𝑈 ∈ ℕ0
→ 𝑈 ∈
ℝ) | 
| 7 | 6 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑈 ∈
ℝ) | 
| 8 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑁 ∈
ℕ) | 
| 9 | 7, 8 | nndivred 12321 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 / 𝑁) ∈ ℝ) | 
| 10 | 8 | nnrpd 13076 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑁 ∈
ℝ+) | 
| 11 |  | nn0ge0 12553 | . . . . . . . . . . 11
⊢ (𝑈 ∈ ℕ0
→ 0 ≤ 𝑈) | 
| 12 | 11 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 0 ≤
𝑈) | 
| 13 | 7, 10, 12 | divge0d 13118 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 0 ≤
(𝑈 / 𝑁)) | 
| 14 |  | flge0nn0 13861 | . . . . . . . . 9
⊢ (((𝑈 / 𝑁) ∈ ℝ ∧ 0 ≤ (𝑈 / 𝑁)) → (⌊‘(𝑈 / 𝑁)) ∈
ℕ0) | 
| 15 | 9, 13, 14 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(⌊‘(𝑈 / 𝑁)) ∈
ℕ0) | 
| 16 | 5, 15 | nn0mulcld 12594 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ∈
ℕ0) | 
| 17 |  | flle 13840 | . . . . . . . . 9
⊢ ((𝑈 / 𝑁) ∈ ℝ →
(⌊‘(𝑈 / 𝑁)) ≤ (𝑈 / 𝑁)) | 
| 18 | 9, 17 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(⌊‘(𝑈 / 𝑁)) ≤ (𝑈 / 𝑁)) | 
| 19 |  | reflcl 13837 | . . . . . . . . . 10
⊢ ((𝑈 / 𝑁) ∈ ℝ →
(⌊‘(𝑈 / 𝑁)) ∈
ℝ) | 
| 20 | 9, 19 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(⌊‘(𝑈 / 𝑁)) ∈
ℝ) | 
| 21 | 20, 7, 10 | lemuldiv2d 13128 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈 ↔ (⌊‘(𝑈 / 𝑁)) ≤ (𝑈 / 𝑁))) | 
| 22 | 18, 21 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈) | 
| 23 |  | fznn0 13660 | . . . . . . . 8
⊢ (𝑈 ∈ ℕ0
→ ((𝑁 ·
(⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈) ↔ ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ ℕ0 ∧ (𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈))) | 
| 24 | 23 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈) ↔ ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ ℕ0 ∧ (𝑁 · (⌊‘(𝑈 / 𝑁))) ≤ 𝑈))) | 
| 25 | 16, 22, 24 | mpbir2and 713 | . . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈)) | 
| 26 |  | fzosplit 13733 | . . . . . 6
⊢ ((𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ (0...𝑈) → (0..^𝑈) = ((0..^(𝑁 · (⌊‘(𝑈 / 𝑁)))) ∪ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈))) | 
| 27 | 25, 26 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(0..^𝑈) = ((0..^(𝑁 · (⌊‘(𝑈 / 𝑁)))) ∪ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈))) | 
| 28 |  | fzofi 14016 | . . . . . 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 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^𝑈)) → 𝑋 ∈ 𝐷) | 
| 36 |  | elfzoelz 13700 | . . . . . . 7
⊢ (𝑛 ∈ (0..^𝑈) → 𝑛 ∈ ℤ) | 
| 37 | 36 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^𝑈)) → 𝑛 ∈ ℤ) | 
| 38 | 30, 31, 32, 33, 35, 37 | dchrzrhcl 27290 | . . . . 5
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^𝑈)) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) | 
| 39 | 2, 27, 29, 38 | fsumsplit 15778 | . . . 4
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛)) = (Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛)))) | 
| 40 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑁 · 𝑘) = (𝑁 · 0)) | 
| 41 | 40 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 = 0 → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · 0))) | 
| 42 | 41 | sumeq1d 15737 | . . . . . . . . . 10
⊢ (𝑘 = 0 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛))) | 
| 43 | 42 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑘 = 0 → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = 0)) | 
| 44 | 43 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = 0 → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = 0))) | 
| 45 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝑁 · 𝑘) = (𝑁 · 𝑚)) | 
| 46 | 45 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · 𝑚))) | 
| 47 | 46 | sumeq1d 15737 | . . . . . . . . . 10
⊢ (𝑘 = 𝑚 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛))) | 
| 48 | 47 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑘 = 𝑚 → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0)) | 
| 49 | 48 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0))) | 
| 50 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑚 + 1) → (𝑁 · 𝑘) = (𝑁 · (𝑚 + 1))) | 
| 51 | 50 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 = (𝑚 + 1) → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · (𝑚 + 1)))) | 
| 52 | 51 | sumeq1d 15737 | . . . . . . . . . 10
⊢ (𝑘 = (𝑚 + 1) → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) | 
| 53 | 52 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑘 = (𝑚 + 1) → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0)) | 
| 54 | 53 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = (𝑚 + 1) → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0))) | 
| 55 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → (𝑁 · 𝑘) = (𝑁 · (⌊‘(𝑈 / 𝑁)))) | 
| 56 | 55 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → (0..^(𝑁 · 𝑘)) = (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))) | 
| 57 | 56 | sumeq1d 15737 | . . . . . . . . . 10
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛))) | 
| 58 | 57 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → (Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0 ↔ Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0)) | 
| 59 | 58 | imbi2d 340 | . . . . . . . 8
⊢ (𝑘 = (⌊‘(𝑈 / 𝑁)) → ((𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 𝑘))(𝑋‘(𝐿‘𝑛)) = 0) ↔ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0))) | 
| 60 | 3 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 61 | 60 | mul01d 11461 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 · 0) = 0) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → (0..^(𝑁 · 0)) = (0..^0)) | 
| 63 |  | fzo0 13724 | . . . . . . . . . . 11
⊢ (0..^0) =
∅ | 
| 64 | 62, 63 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝜑 → (0..^(𝑁 · 0)) = ∅) | 
| 65 | 64 | sumeq1d 15737 | . . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ∅ (𝑋‘(𝐿‘𝑛))) | 
| 66 |  | sum0 15758 | . . . . . . . . 9
⊢
Σ𝑛 ∈
∅ (𝑋‘(𝐿‘𝑛)) = 0 | 
| 67 | 65, 66 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · 0))(𝑋‘(𝐿‘𝑛)) = 0) | 
| 68 |  | oveq1 7439 | . . . . . . . . . . 11
⊢
(Σ𝑛 ∈
(0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0 → (Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) = (0 + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)))) | 
| 69 |  | fzodisj 13734 | . . . . . . . . . . . . . 14
⊢
((0..^(𝑁 ·
𝑚)) ∩ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))) = ∅ | 
| 70 | 69 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
((0..^(𝑁 · 𝑚)) ∩ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))) = ∅) | 
| 71 |  | nn0re 12537 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) | 
| 72 | 71 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℝ) | 
| 73 | 72 | lep1d 12200 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ≤ (𝑚 + 1)) | 
| 74 |  | peano2re 11435 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℝ → (𝑚 + 1) ∈
ℝ) | 
| 75 | 72, 74 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℝ) | 
| 76 | 3 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℕ) | 
| 77 | 76 | nnred 12282 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℝ) | 
| 78 | 76 | nngt0d 12316 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 0 <
𝑁) | 
| 79 |  | lemul2 12121 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℝ ∧ (𝑚 + 1) ∈ ℝ ∧
(𝑁 ∈ ℝ ∧ 0
< 𝑁)) → (𝑚 ≤ (𝑚 + 1) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) | 
| 80 | 72, 75, 77, 78, 79 | syl112anc 1375 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑚 ≤ (𝑚 + 1) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) | 
| 81 | 73, 80 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1))) | 
| 82 |  | nn0mulcl 12564 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0
∧ 𝑚 ∈
ℕ0) → (𝑁 · 𝑚) ∈
ℕ0) | 
| 83 | 4, 82 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈
ℕ0) | 
| 84 |  | nn0uz 12921 | . . . . . . . . . . . . . . . . 17
⊢
ℕ0 = (ℤ≥‘0) | 
| 85 | 83, 84 | eleqtrdi 2850 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈
(ℤ≥‘0)) | 
| 86 |  | nn0p1nn 12567 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ) | 
| 87 |  | nnmulcl 12291 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ ∧ (𝑚 + 1) ∈ ℕ) →
(𝑁 · (𝑚 + 1)) ∈
ℕ) | 
| 88 | 3, 86, 87 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) ∈ ℕ) | 
| 89 | 88 | nnzd 12642 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) ∈ ℤ) | 
| 90 |  | elfz5 13557 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 · 𝑚) ∈ (ℤ≥‘0)
∧ (𝑁 · (𝑚 + 1)) ∈ ℤ) →
((𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1))) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) | 
| 91 | 85, 89, 90 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1))) ↔ (𝑁 · 𝑚) ≤ (𝑁 · (𝑚 + 1)))) | 
| 92 | 81, 91 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1)))) | 
| 93 |  | fzosplit 13733 | . . . . . . . . . . . . . 14
⊢ ((𝑁 · 𝑚) ∈ (0...(𝑁 · (𝑚 + 1))) → (0..^(𝑁 · (𝑚 + 1))) = ((0..^(𝑁 · 𝑚)) ∪ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1))))) | 
| 94 | 92, 93 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(0..^(𝑁 · (𝑚 + 1))) = ((0..^(𝑁 · 𝑚)) ∪ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1))))) | 
| 95 |  | fzofi 14016 | . . . . . . . . . . . . . 14
⊢
(0..^(𝑁 ·
(𝑚 + 1))) ∈
Fin | 
| 96 | 95 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(0..^(𝑁 · (𝑚 + 1))) ∈
Fin) | 
| 97 | 34 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))) → 𝑋 ∈ 𝐷) | 
| 98 |  | elfzoelz 13700 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ (0..^(𝑁 · (𝑚 + 1))) → 𝑛 ∈ ℤ) | 
| 99 | 98 | adantl 481 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))) → 𝑛 ∈ ℤ) | 
| 100 | 30, 31, 32, 33, 97, 99 | dchrzrhcl 27290 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) | 
| 101 | 70, 94, 96, 100 | fsumsplit 15778 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = (Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)))) | 
| 102 | 76 | nncnd 12283 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℂ) | 
| 103 | 72 | recnd 11290 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) | 
| 104 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℂ) | 
| 105 | 102, 103,
104 | adddid 11286 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) = ((𝑁 · 𝑚) + (𝑁 · 1))) | 
| 106 | 102 | mulridd 11279 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 1) = 𝑁) | 
| 107 | 106 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁 · 𝑚) + (𝑁 · 1)) = ((𝑁 · 𝑚) + 𝑁)) | 
| 108 | 105, 107 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · (𝑚 + 1)) = ((𝑁 · 𝑚) + 𝑁)) | 
| 109 | 108 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1))) = ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))) | 
| 110 | 109 | sumeq1d 15737 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 111 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑁 → ((𝑁 · 𝑚) + 𝑘) = ((𝑁 · 𝑚) + 𝑁)) | 
| 112 | 111 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑁 → ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))) | 
| 113 | 112 | sumeq1d 15737 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑁 → Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 114 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑁 → (0..^𝑘) = (0..^𝑁)) | 
| 115 | 114 | sumeq1d 15737 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑁 → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛))) | 
| 116 | 113, 115 | eqeq12d 2752 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑁 → (Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ↔ Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛)))) | 
| 117 | 83 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑁 · 𝑚) ∈ ℤ) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑁 · 𝑚) ∈
ℤ) | 
| 119 |  | nn0z 12640 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) | 
| 120 |  | zaddcl 12659 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 · 𝑚) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑁 · 𝑚) + 𝑘) ∈ ℤ) | 
| 121 | 117, 119,
120 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚) + 𝑘) ∈ ℤ) | 
| 122 |  | peano2zm 12662 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 · 𝑚) + 𝑘) ∈ ℤ → (((𝑁 · 𝑚) + 𝑘) − 1) ∈ ℤ) | 
| 123 | 121, 122 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑁 · 𝑚) + 𝑘) − 1) ∈ ℤ) | 
| 124 | 34 | ad3antrrr 730 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) → 𝑋 ∈ 𝐷) | 
| 125 |  | elfzelz 13565 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1)) → 𝑛 ∈ ℤ) | 
| 126 | 125 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) → 𝑛 ∈ ℤ) | 
| 127 | 30, 31, 32, 33, 124, 126 | dchrzrhcl 27290 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) | 
| 128 |  | 2fveq3 6910 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = (𝑖 + (𝑁 · 𝑚)) → (𝑋‘(𝐿‘𝑛)) = (𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) | 
| 129 | 118, 118,
123, 127, 128 | fsumshftm 15818 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))(𝑋‘(𝐿‘𝑛)) = Σ𝑖 ∈ (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)))(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) | 
| 130 |  | fzoval 13701 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 · 𝑚) + 𝑘) ∈ ℤ → ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) | 
| 131 | 121, 130 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))) | 
| 132 | 131 | sumeq1d 15737 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · 𝑚)...(((𝑁 · 𝑚) + 𝑘) − 1))(𝑋‘(𝐿‘𝑛))) | 
| 133 | 119 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℤ) | 
| 134 |  | fzoval 13701 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℤ →
(0..^𝑘) = (0...(𝑘 − 1))) | 
| 135 | 133, 134 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0..^𝑘) =
(0...(𝑘 −
1))) | 
| 136 | 118 | zcnd 12725 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (𝑁 · 𝑚) ∈
ℂ) | 
| 137 | 136 | subidd 11609 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚) − (𝑁 · 𝑚)) = 0) | 
| 138 | 121 | zcnd 12725 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑁 · 𝑚) + 𝑘) ∈ ℂ) | 
| 139 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 1 ∈ ℂ) | 
| 140 | 138, 139,
136 | sub32d 11653 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)) = ((((𝑁 · 𝑚) + 𝑘) − (𝑁 · 𝑚)) − 1)) | 
| 141 |  | nn0cn 12538 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) | 
| 142 | 141 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℂ) | 
| 143 | 136, 142 | pncan2d 11623 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑁 · 𝑚) + 𝑘) − (𝑁 · 𝑚)) = 𝑘) | 
| 144 | 143 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((((𝑁 · 𝑚) + 𝑘) − (𝑁 · 𝑚)) − 1) = (𝑘 − 1)) | 
| 145 | 140, 144 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ ((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)) = (𝑘 − 1)) | 
| 146 | 137, 145 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚))) = (0...(𝑘 − 1))) | 
| 147 | 135, 146 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ (0..^𝑘) = (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)))) | 
| 148 | 147 | sumeq1d 15737 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = Σ𝑖 ∈ (((𝑁 · 𝑚) − (𝑁 · 𝑚))...((((𝑁 · 𝑚) + 𝑘) − 1) − (𝑁 · 𝑚)))(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) | 
| 149 | 129, 132,
148 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑖 ∈ (0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚))))) | 
| 150 | 3 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 151 |  | nn0z 12640 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℤ) | 
| 152 |  | dvdsmul1 16316 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ) → 𝑁 ∥ (𝑁 · 𝑚)) | 
| 153 | 150, 151,
152 | syl2an 596 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∥ (𝑁 · 𝑚)) | 
| 154 | 153 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑁 ∥ (𝑁 · 𝑚)) | 
| 155 |  | elfzoelz 13700 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑘) → 𝑖 ∈ ℤ) | 
| 156 | 155 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑖 ∈ ℤ) | 
| 157 | 156 | zcnd 12725 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑖 ∈ ℂ) | 
| 158 | 136 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝑁 · 𝑚) ∈ ℂ) | 
| 159 | 157, 158 | pncan2d 11623 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → ((𝑖 + (𝑁 · 𝑚)) − 𝑖) = (𝑁 · 𝑚)) | 
| 160 | 154, 159 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑁 ∥ ((𝑖 + (𝑁 · 𝑚)) − 𝑖)) | 
| 161 | 76 | nnnn0d 12589 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑁 ∈
ℕ0) | 
| 162 | 161 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → 𝑁 ∈
ℕ0) | 
| 163 |  | zaddcl 12659 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑖 ∈ ℤ ∧ (𝑁 · 𝑚) ∈ ℤ) → (𝑖 + (𝑁 · 𝑚)) ∈ ℤ) | 
| 164 | 155, 118,
163 | syl2anr 597 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝑖 + (𝑁 · 𝑚)) ∈ ℤ) | 
| 165 | 31, 33 | zndvds 21569 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 ∈ ℕ0
∧ (𝑖 + (𝑁 · 𝑚)) ∈ ℤ ∧ 𝑖 ∈ ℤ) → ((𝐿‘(𝑖 + (𝑁 · 𝑚))) = (𝐿‘𝑖) ↔ 𝑁 ∥ ((𝑖 + (𝑁 · 𝑚)) − 𝑖))) | 
| 166 | 162, 164,
156, 165 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → ((𝐿‘(𝑖 + (𝑁 · 𝑚))) = (𝐿‘𝑖) ↔ 𝑁 ∥ ((𝑖 + (𝑁 · 𝑚)) − 𝑖))) | 
| 167 | 160, 166 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝐿‘(𝑖 + (𝑁 · 𝑚))) = (𝐿‘𝑖)) | 
| 168 | 167 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
∧ 𝑖 ∈ (0..^𝑘)) → (𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = (𝑋‘(𝐿‘𝑖))) | 
| 169 | 168 | sumeq2dv 15739 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = Σ𝑖 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑖))) | 
| 170 |  | 2fveq3 6910 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑛 → (𝑋‘(𝐿‘𝑖)) = (𝑋‘(𝐿‘𝑛))) | 
| 171 | 170 | cbvsumv 15733 | . . . . . . . . . . . . . . . . . . 19
⊢
Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘𝑖)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) | 
| 172 | 169, 171 | eqtrdi 2792 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑖 ∈
(0..^𝑘)(𝑋‘(𝐿‘(𝑖 + (𝑁 · 𝑚)))) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) | 
| 173 | 149, 172 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑘 ∈ ℕ0)
→ Σ𝑛 ∈
((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) | 
| 174 | 173 | ralrimiva 3145 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
∀𝑘 ∈
ℕ0 Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) | 
| 175 | 116, 174,
161 | rspcdva 3622 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑁))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛))) | 
| 176 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝐿‘𝑛) → (𝑋‘𝑘) = (𝑋‘(𝐿‘𝑛))) | 
| 177 | 3 | nnne0d 12317 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 178 |  | ifnefalse 4536 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ≠ 0 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) | 
| 179 | 177, 178 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → if(𝑁 = 0, ℤ, (0..^𝑁)) = (0..^𝑁)) | 
| 180 |  | fzofi 14016 | . . . . . . . . . . . . . . . . . . 19
⊢
(0..^𝑁) ∈
Fin | 
| 181 | 179, 180 | eqeltrdi 2848 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝑁 = 0, ℤ, (0..^𝑁)) ∈ Fin) | 
| 182 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(Base‘𝑍) =
(Base‘𝑍) | 
| 183 | 33 | reseq1i 5992 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) = ((ℤRHom‘𝑍) ↾ if(𝑁 = 0, ℤ, (0..^𝑁))) | 
| 184 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢ if(𝑁 = 0, ℤ, (0..^𝑁)) = if(𝑁 = 0, ℤ, (0..^𝑁)) | 
| 185 | 31, 182, 183, 184 | znf1o 21571 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ (𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑍)) | 
| 186 | 4, 185 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁))):if(𝑁 = 0, ℤ, (0..^𝑁))–1-1-onto→(Base‘𝑍)) | 
| 187 |  | fvres 6924 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ if(𝑁 = 0, ℤ, (0..^𝑁)) → ((𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁)))‘𝑛) = (𝐿‘𝑛)) | 
| 188 | 187 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑛 ∈ if(𝑁 = 0, ℤ, (0..^𝑁))) → ((𝐿 ↾ if(𝑁 = 0, ℤ, (0..^𝑁)))‘𝑛) = (𝐿‘𝑛)) | 
| 189 | 30, 31, 32, 182, 34 | dchrf 27287 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ) | 
| 190 | 189 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (Base‘𝑍)) → (𝑋‘𝑘) ∈ ℂ) | 
| 191 | 176, 181,
186, 188, 190 | fsumf1o 15760 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (Base‘𝑍)(𝑋‘𝑘) = Σ𝑛 ∈ if (𝑁 = 0, ℤ, (0..^𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 192 |  | rpvmasum.1 | . . . . . . . . . . . . . . . . . . 19
⊢  1 =
(0g‘𝐺) | 
| 193 | 30, 31, 32, 192, 34, 182 | dchrsum 27314 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Σ𝑘 ∈ (Base‘𝑍)(𝑋‘𝑘) = if(𝑋 = 1 , (ϕ‘𝑁), 0)) | 
| 194 |  | dchrisum.n1 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 ≠ 1 ) | 
| 195 |  | ifnefalse 4536 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ≠ 1 → if(𝑋 = 1 , (ϕ‘𝑁), 0) = 0) | 
| 196 | 194, 195 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → if(𝑋 = 1 , (ϕ‘𝑁), 0) = 0) | 
| 197 | 193, 196 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑘 ∈ (Base‘𝑍)(𝑋‘𝑘) = 0) | 
| 198 | 179 | sumeq1d 15737 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Σ𝑛 ∈ if (𝑁 = 0, ℤ, (0..^𝑁))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛))) | 
| 199 | 191, 197,
198 | 3eqtr3rd 2785 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛)) = 0) | 
| 200 | 199 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ (0..^𝑁)(𝑋‘(𝐿‘𝑛)) = 0) | 
| 201 | 110, 175,
200 | 3eqtrd 2780 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0) | 
| 202 | 201 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (0 +
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) = (0 + 0)) | 
| 203 |  | 00id 11437 | . . . . . . . . . . . . 13
⊢ (0 + 0) =
0 | 
| 204 | 202, 203 | eqtr2di 2793 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 0 = (0 +
Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)))) | 
| 205 | 101, 204 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(Σ𝑛 ∈
(0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0 ↔ (Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))) = (0 + Σ𝑛 ∈ ((𝑁 · 𝑚)..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛))))) | 
| 206 | 68, 205 | imbitrrid 246 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(Σ𝑛 ∈
(0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0)) | 
| 207 | 206 | expcom 413 | . . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
→ (𝜑 →
(Σ𝑛 ∈
(0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0))) | 
| 208 | 207 | a2d 29 | . . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ ((𝜑 →
Σ𝑛 ∈ (0..^(𝑁 · 𝑚))(𝑋‘(𝐿‘𝑛)) = 0) → (𝜑 → Σ𝑛 ∈ (0..^(𝑁 · (𝑚 + 1)))(𝑋‘(𝐿‘𝑛)) = 0))) | 
| 209 | 44, 49, 54, 59, 67, 208 | nn0ind 12715 | . . . . . . 7
⊢
((⌊‘(𝑈 /
𝑁)) ∈
ℕ0 → (𝜑
→ Σ𝑛 ∈
(0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0)) | 
| 210 | 209 | impcom 407 | . . . . . 6
⊢ ((𝜑 ∧ (⌊‘(𝑈 / 𝑁)) ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0) | 
| 211 | 15, 210 | syldan 591 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑁 · (⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) = 0) | 
| 212 |  | modval 13912 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ ℝ ∧ 𝑁 ∈ ℝ+)
→ (𝑈 mod 𝑁) = (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁))))) | 
| 213 | 7, 10, 212 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 mod 𝑁) = (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁))))) | 
| 214 | 213 | oveq2d 7448 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)) = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁)))))) | 
| 215 | 16 | nn0cnd 12591 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑁 · (⌊‘(𝑈 / 𝑁))) ∈ ℂ) | 
| 216 |  | nn0cn 12538 | . . . . . . . . . . 11
⊢ (𝑈 ∈ ℕ0
→ 𝑈 ∈
ℂ) | 
| 217 | 216 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑈 ∈
ℂ) | 
| 218 | 215, 217 | pncan3d 11624 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 − (𝑁 · (⌊‘(𝑈 / 𝑁))))) = 𝑈) | 
| 219 | 214, 218 | eqtr2d 2777 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → 𝑈 = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁))) | 
| 220 | 219 | oveq2d 7448 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈) = ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))) | 
| 221 | 220 | sumeq1d 15737 | . . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛))) | 
| 222 |  | nn0z 12640 | . . . . . . . 8
⊢ (𝑈 ∈ ℕ0
→ 𝑈 ∈
ℤ) | 
| 223 |  | zmodcl 13932 | . . . . . . . 8
⊢ ((𝑈 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑈 mod 𝑁) ∈
ℕ0) | 
| 224 | 222, 3, 223 | syl2anr 597 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 mod 𝑁) ∈
ℕ0) | 
| 225 | 174 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝜑 → ∀𝑚 ∈ ℕ0 ∀𝑘 ∈ ℕ0
Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) | 
| 226 | 225 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
∀𝑚 ∈
ℕ0 ∀𝑘 ∈ ℕ0 Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) | 
| 227 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → (𝑁 · 𝑚) = (𝑁 · (⌊‘(𝑈 / 𝑁)))) | 
| 228 | 227 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → ((𝑁 · 𝑚) + 𝑘) = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘)) | 
| 229 | 227, 228 | oveq12d 7450 | . . . . . . . . . 10
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘)) = ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))) | 
| 230 | 229 | sumeq1d 15737 | . . . . . . . . 9
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛))) | 
| 231 | 230 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑚 = (⌊‘(𝑈 / 𝑁)) → (Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ↔ Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)))) | 
| 232 |  | oveq2 7440 | . . . . . . . . . . 11
⊢ (𝑘 = (𝑈 mod 𝑁) → ((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘) = ((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁))) | 
| 233 | 232 | oveq2d 7448 | . . . . . . . . . 10
⊢ (𝑘 = (𝑈 mod 𝑁) → ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘)) = ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))) | 
| 234 | 233 | sumeq1d 15737 | . . . . . . . . 9
⊢ (𝑘 = (𝑈 mod 𝑁) → Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛))) | 
| 235 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑘 = (𝑈 mod 𝑁) → (0..^𝑘) = (0..^(𝑈 mod 𝑁))) | 
| 236 | 235 | sumeq1d 15737 | . . . . . . . . 9
⊢ (𝑘 = (𝑈 mod 𝑁) → Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 237 | 234, 236 | eqeq12d 2752 | . . . . . . . 8
⊢ (𝑘 = (𝑈 mod 𝑁) → (Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛)) ↔ Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) | 
| 238 | 231, 237 | rspc2va 3633 | . . . . . . 7
⊢
((((⌊‘(𝑈
/ 𝑁)) ∈
ℕ0 ∧ (𝑈 mod 𝑁) ∈ ℕ0) ∧
∀𝑚 ∈
ℕ0 ∀𝑘 ∈ ℕ0 Σ𝑛 ∈ ((𝑁 · 𝑚)..^((𝑁 · 𝑚) + 𝑘))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^𝑘)(𝑋‘(𝐿‘𝑛))) → Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 239 | 15, 224, 226, 238 | syl21anc 837 | . . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^((𝑁 · (⌊‘(𝑈 / 𝑁))) + (𝑈 mod 𝑁)))(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 240 | 221, 239 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 241 | 211, 240 | oveq12d 7450 | . . . 4
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(Σ𝑛 ∈
(0..^(𝑁 ·
(⌊‘(𝑈 / 𝑁))))(𝑋‘(𝐿‘𝑛)) + Σ𝑛 ∈ ((𝑁 · (⌊‘(𝑈 / 𝑁)))..^𝑈)(𝑋‘(𝐿‘𝑛))) = (0 + Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) | 
| 242 |  | fzofi 14016 | . . . . . . 7
⊢
(0..^(𝑈 mod 𝑁)) ∈ Fin | 
| 243 | 242 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(0..^(𝑈 mod 𝑁)) ∈ Fin) | 
| 244 | 34 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑈 mod 𝑁))) → 𝑋 ∈ 𝐷) | 
| 245 |  | elfzoelz 13700 | . . . . . . . 8
⊢ (𝑛 ∈ (0..^(𝑈 mod 𝑁)) → 𝑛 ∈ ℤ) | 
| 246 | 245 | adantl 481 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑈 mod 𝑁))) → 𝑛 ∈ ℤ) | 
| 247 | 30, 31, 32, 33, 244, 246 | dchrzrhcl 27290 | . . . . . 6
⊢ (((𝜑 ∧ 𝑈 ∈ ℕ0) ∧ 𝑛 ∈ (0..^(𝑈 mod 𝑁))) → (𝑋‘(𝐿‘𝑛)) ∈ ℂ) | 
| 248 | 243, 247 | fsumcl 15770 | . . . . 5
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)) ∈ ℂ) | 
| 249 | 248 | addlidd 11463 | . . . 4
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (0 +
Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 250 | 39, 241, 249 | 3eqtrd 2780 | . . 3
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 251 | 250 | fveq2d 6909 | . 2
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^𝑈)(𝑋‘(𝐿‘𝑛))) = (abs‘Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) | 
| 252 |  | oveq2 7440 | . . . . . 6
⊢ (𝑢 = (𝑈 mod 𝑁) → (0..^𝑢) = (0..^(𝑈 mod 𝑁))) | 
| 253 | 252 | sumeq1d 15737 | . . . . 5
⊢ (𝑢 = (𝑈 mod 𝑁) → Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛)) = Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) | 
| 254 | 253 | fveq2d 6909 | . . . 4
⊢ (𝑢 = (𝑈 mod 𝑁) → (abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) = (abs‘Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛)))) | 
| 255 | 254 | breq1d 5152 | . . 3
⊢ (𝑢 = (𝑈 mod 𝑁) → ((abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅 ↔ (abs‘Σ𝑛 ∈ (0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)) | 
| 256 |  | dchrisum.10 | . . . 4
⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) | 
| 257 | 256 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) | 
| 258 |  | zmodfzo 13935 | . . . 4
⊢ ((𝑈 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑈 mod 𝑁) ∈ (0..^𝑁)) | 
| 259 | 222, 3, 258 | syl2anr 597 | . . 3
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (𝑈 mod 𝑁) ∈ (0..^𝑁)) | 
| 260 | 255, 257,
259 | rspcdva 3622 | . 2
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^(𝑈 mod 𝑁))(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) | 
| 261 | 251, 260 | eqbrtrd 5164 | 1
⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) →
(abs‘Σ𝑛 ∈
(0..^𝑈)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅) |