| Step | Hyp | Ref
| Expression |
| 1 | | breprexplemc.t |
. . . . 5
⊢ (𝜑 → 𝑇 ∈
ℕ0) |
| 2 | | nn0uz 12920 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
| 3 | 1, 2 | eleqtrdi 2851 |
. . . 4
⊢ (𝜑 → 𝑇 ∈
(ℤ≥‘0)) |
| 4 | | fzosplitsn 13814 |
. . . 4
⊢ (𝑇 ∈
(ℤ≥‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇})) |
| 5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇})) |
| 6 | 5 | prodeq1d 15956 |
. 2
⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏))) |
| 7 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑎𝜑 |
| 8 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) |
| 9 | | fzofi 14015 |
. . . 4
⊢
(0..^𝑇) ∈
Fin |
| 10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → (0..^𝑇) ∈ Fin) |
| 11 | | fzonel 13713 |
. . . 4
⊢ ¬
𝑇 ∈ (0..^𝑇) |
| 12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → ¬ 𝑇 ∈ (0..^𝑇)) |
| 13 | | fzfid 14014 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin) |
| 14 | | breprexp.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 15 | 14 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
| 16 | | breprexp.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
| 17 | 16 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) |
| 18 | | breprexp.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ ℂ) |
| 19 | 18 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
| 20 | | breprexp.h |
. . . . . . . 8
⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 21 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 23 | 1 | nn0zd 12639 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ ℤ) |
| 24 | 16 | nn0zd 12639 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℤ) |
| 25 | 1 | nn0red 12588 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 26 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
| 27 | 25, 26 | readdcld 11290 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 + 1) ∈ ℝ) |
| 28 | 16 | nn0red 12588 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℝ) |
| 29 | 25 | lep1d 12199 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ≤ (𝑇 + 1)) |
| 30 | | breprexplemc.s |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 + 1) ≤ 𝑆) |
| 31 | 25, 27, 28, 29, 30 | letrd 11418 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ≤ 𝑆) |
| 32 | | eluz1 12882 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ℤ → (𝑆 ∈
(ℤ≥‘𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆))) |
| 33 | 32 | biimpar 477 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)) → 𝑆 ∈ (ℤ≥‘𝑇)) |
| 34 | 23, 24, 31, 33 | syl12anc 837 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘𝑇)) |
| 35 | | fzoss2 13727 |
. . . . . . . . 9
⊢ (𝑆 ∈
(ℤ≥‘𝑇) → (0..^𝑇) ⊆ (0..^𝑆)) |
| 36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0..^𝑇) ⊆ (0..^𝑆)) |
| 37 | 36 | sselda 3983 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
| 38 | 37 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆)) |
| 39 | | fz1ssnn 13595 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
| 40 | 39 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ) |
| 41 | 40 | sselda 3983 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ) |
| 42 | 15, 17, 19, 22, 38, 41 | breprexplemb 34646 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) ∈ ℂ) |
| 43 | | nnssnn0 12529 |
. . . . . . . . . . 11
⊢ ℕ
⊆ ℕ0 |
| 44 | 39, 43 | sstri 3993 |
. . . . . . . . . 10
⊢
(1...𝑁) ⊆
ℕ0 |
| 45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ⊆
ℕ0) |
| 46 | 45 | ralrimivw 3150 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆
ℕ0) |
| 47 | 46 | r19.21bi 3251 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆
ℕ0) |
| 48 | 47 | sselda 3983 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
| 49 | 19, 48 | expcld 14186 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ) |
| 50 | 42, 49 | mulcld 11281 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
| 51 | 13, 50 | fsumcl 15769 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
| 52 | | simpl 482 |
. . . . . . 7
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇) |
| 53 | 52 | fveq2d 6910 |
. . . . . 6
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (𝐿‘𝑎) = (𝐿‘𝑇)) |
| 54 | 53 | fveq1d 6908 |
. . . . 5
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) = ((𝐿‘𝑇)‘𝑏)) |
| 55 | 54 | oveq1d 7446 |
. . . 4
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) |
| 56 | 55 | sumeq2dv 15738 |
. . 3
⊢ (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) |
| 57 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
| 58 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
| 59 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) |
| 60 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
| 61 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 62 | 1 | nn0ge0d 12590 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑇) |
| 63 | | zltp1le 12667 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆)) |
| 64 | 23, 24, 63 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆)) |
| 65 | 30, 64 | mpbird 257 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 < 𝑆) |
| 66 | | 0zd 12625 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℤ) |
| 67 | | elfzo 13701 |
. . . . . . . . 9
⊢ ((𝑇 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑆 ∈
ℤ) → (𝑇 ∈
(0..^𝑆) ↔ (0 ≤
𝑇 ∧ 𝑇 < 𝑆))) |
| 68 | 23, 66, 24, 67 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆))) |
| 69 | 62, 65, 68 | mpbir2and 713 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (0..^𝑆)) |
| 70 | 69 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆)) |
| 71 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
| 72 | 71 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ) |
| 73 | 58, 59, 60, 61, 70, 72 | breprexplemb 34646 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 74 | 45 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
| 75 | 60, 74 | expcld 14186 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ) |
| 76 | 73, 75 | mulcld 11281 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
| 77 | 57, 76 | fsumcl 15769 |
. . 3
⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
| 78 | 7, 8, 10, 1, 12, 51, 56, 77 | fprodsplitsn 16025 |
. 2
⊢ (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 79 | | breprexplemc.1 |
. . . 4
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
| 80 | 79 | oveq1d 7446 |
. . 3
⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 81 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin) |
| 82 | 39 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
| 83 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁))) |
| 84 | 83 | elfzelzd 13565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ) |
| 85 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈
ℕ0) |
| 86 | 57 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin) |
| 87 | 82, 84, 85, 86 | reprfi 34631 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin) |
| 88 | 9 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin) |
| 89 | 14 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈
ℕ0) |
| 90 | 89 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈
ℕ0) |
| 91 | 16 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈
ℕ0) |
| 92 | 18 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ) |
| 93 | 20 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 94 | 36 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆)) |
| 95 | 94 | sselda 3983 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
| 96 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ) |
| 97 | 84 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ) |
| 98 | 85 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈
ℕ0) |
| 99 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) |
| 100 | 96, 97, 98, 99 | reprf 34627 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
| 101 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇)) |
| 102 | 100, 101 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁)) |
| 103 | 39, 102 | sselid 3981 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ) |
| 104 | 90, 91, 92, 93, 95, 103 | breprexplemb 34646 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 105 | 88, 104 | fprodcl 15988 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 106 | 18 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ) |
| 107 | | fz0ssnn0 13662 |
. . . . . . . . 9
⊢
(0...(𝑇 ·
𝑁)) ⊆
ℕ0 |
| 108 | 107, 83 | sselid 3981 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0) |
| 109 | 108 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0) |
| 110 | 106, 109 | expcld 14186 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ) |
| 111 | 105, 110 | mulcld 11281 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ) |
| 112 | 87, 111 | fsumcl 15769 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ) |
| 113 | 81, 57, 112, 76 | fsum2mul 15825 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 114 | 39 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ) |
| 115 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) |
| 116 | 115 | elfzelzd 13565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ) |
| 117 | 116 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ) |
| 118 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
| 119 | 118 | elfzelzd 13565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ) |
| 120 | 117, 119 | zsubcld 12727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − 𝑏) ∈ ℤ) |
| 121 | 1 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈
ℕ0) |
| 122 | 121 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈
ℕ0) |
| 123 | 57 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin) |
| 124 | 123 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin) |
| 125 | 114, 120,
122, 124 | reprfi 34631 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)) ∈ Fin) |
| 126 | 73 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 127 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ) |
| 128 | | fz0ssnn0 13662 |
. . . . . . . . . . . . 13
⊢
(0...((𝑇 + 1)
· 𝑁)) ⊆
ℕ0 |
| 129 | 128, 115 | sselid 3981 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0) |
| 130 | 127, 129 | expcld 14186 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍↑𝑚) ∈ ℂ) |
| 131 | 130 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑚) ∈ ℂ) |
| 132 | 126, 131 | mulcld 11281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) ∈ ℂ) |
| 133 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (0..^𝑇) ∈ Fin) |
| 134 | 14 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈
ℕ0) |
| 135 | 134 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
| 136 | 135 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈
ℕ0) |
| 137 | 16 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈
ℕ0) |
| 138 | 127 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ) |
| 139 | 20 | ad4antr 732 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 140 | 37 | ad5ant15 759 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
| 141 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ) |
| 142 | 120 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚 − 𝑏) ∈ ℤ) |
| 143 | 122 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈
ℕ0) |
| 144 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) |
| 145 | 141, 142,
143, 144 | reprf 34627 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
| 146 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇)) |
| 147 | 145, 146 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁)) |
| 148 | 39, 147 | sselid 3981 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ) |
| 149 | 136, 137,
138, 139, 140, 148 | breprexplemb 34646 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 150 | 133, 149 | fprodcl 15988 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 151 | 125, 132,
150 | fsummulc1 15821 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 152 | 151 | sumeq2dv 15738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 153 | | elfzle2 13568 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁)) |
| 154 | 153 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁)) |
| 155 | 134 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℕ0) |
| 156 | 16 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈
ℕ0) |
| 157 | 127 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ) |
| 158 | 20 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 159 | 23 | peano2zd 12725 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 + 1) ∈ ℤ) |
| 160 | | eluz 12892 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈
(ℤ≥‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆)) |
| 161 | 160 | biimpar 477 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ≥‘(𝑇 + 1))) |
| 162 | 159, 24, 30, 161 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘(𝑇 + 1))) |
| 163 | | fzoss2 13727 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(ℤ≥‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
| 164 | 162, 163 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
| 165 | 164 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
| 166 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1))) |
| 167 | 165, 166 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆)) |
| 168 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ) |
| 169 | 155, 156,
157, 158, 167, 168 | breprexplemb 34646 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿‘𝑥)‘𝑦) ∈ ℂ) |
| 170 | 134, 121,
129, 154, 169 | breprexplema 34645 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏))) |
| 171 | 170 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚))) |
| 172 | 126 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 173 | 150, 172 | mulcld 11281 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ) |
| 174 | 125, 173 | fsumcl 15769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ) |
| 175 | 123, 130,
174 | fsummulc1 15821 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚))) |
| 176 | 125, 131,
173 | fsummulc1 15821 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚))) |
| 177 | 131 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (𝑍↑𝑚) ∈ ℂ) |
| 178 | 150, 172,
177 | mulassd 11284 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 179 | 178 | sumeq2dv 15738 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 180 | 176, 179 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 181 | 180 | sumeq2dv 15738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 182 | 171, 175,
181 | 3eqtrd 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 183 | 39 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ) |
| 184 | | 1nn0 12542 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
| 185 | 184 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈
ℕ0) |
| 186 | 121, 185 | nn0addcld 12591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈
ℕ0) |
| 187 | 183, 116,
186, 123 | reprfi 34631 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin) |
| 188 | | fzofi 14015 |
. . . . . . . . . 10
⊢
(0..^(𝑇 + 1)) ∈
Fin |
| 189 | 188 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin) |
| 190 | 134 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈
ℕ0) |
| 191 | 16 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈
ℕ0) |
| 192 | 127 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ) |
| 193 | 20 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 194 | 164 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
| 195 | 194 | sselda 3983 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆)) |
| 196 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ) |
| 197 | 116 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ) |
| 198 | 186 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈
ℕ0) |
| 199 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) |
| 200 | 196, 197,
198, 199 | reprf 34627 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁)) |
| 201 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1))) |
| 202 | 200, 201 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁)) |
| 203 | 39, 202 | sselid 3981 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ ℕ) |
| 204 | 190, 191,
192, 193, 195, 203 | breprexplemb 34646 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 205 | 189, 204 | fprodcl 15988 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 206 | 187, 130,
205 | fsummulc1 15821 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
| 207 | 152, 182,
206 | 3eqtr2rd 2784 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 208 | 207 | sumeq2dv 15738 |
. . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 209 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑛 − 𝑏) = (𝑚 − 𝑏)) |
| 210 | 209 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) |
| 211 | 210 | sumeq1d 15736 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
| 212 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝑍↑𝑛) = (𝑍↑𝑚)) |
| 213 | 212 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) |
| 214 | 211, 213 | oveq12d 7449 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 215 | 214 | adantr 480 |
. . . . . . 7
⊢ ((𝑛 = 𝑚 ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 216 | 215 | sumeq2dv 15738 |
. . . . . 6
⊢ (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
| 217 | 216 | cbvsumv 15732 |
. . . . 5
⊢
Σ𝑛 ∈
(0...((𝑇 + 1) ·
𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) |
| 218 | 208, 217 | eqtr4di 2795 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)))) |
| 219 | 1, 14 | nn0mulcld 12592 |
. . . . . 6
⊢ (𝜑 → (𝑇 · 𝑁) ∈
ℕ0) |
| 220 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 − 𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))) |
| 221 | 220 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑚 = (𝑛 − 𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
| 222 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 − 𝑏) → (𝑚 + 𝑏) = ((𝑛 − 𝑏) + 𝑏)) |
| 223 | 222 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 − 𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛 − 𝑏) + 𝑏))) |
| 224 | 223 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑚 = (𝑛 − 𝑏) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) |
| 225 | 221, 224 | oveq12d 7449 |
. . . . . 6
⊢ (𝑚 = (𝑛 − 𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
| 226 | 39 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ) |
| 227 | | uzssz 12899 |
. . . . . . . . . 10
⊢
(ℤ≥‘-𝑏) ⊆ ℤ |
| 228 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ≥‘-𝑏)) |
| 229 | 227, 228 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ) |
| 230 | 1 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈
ℕ0) |
| 231 | 57 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin) |
| 232 | 226, 229,
230, 231 | reprfi 34631 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin) |
| 233 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin) |
| 234 | 58 | 3adant2 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
| 235 | 234 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈
ℕ0) |
| 236 | 59 | 3adant2 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) |
| 237 | 236 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈
ℕ0) |
| 238 | 60 | 3adant2 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
| 239 | 238 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ) |
| 240 | 61 | 3adant2 1132 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 241 | 240 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
| 242 | 36 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆)) |
| 243 | 242 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆)) |
| 244 | 243 | sselda 3983 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
| 245 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ) |
| 246 | 229 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ) |
| 247 | 230 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈
ℕ0) |
| 248 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) |
| 249 | 245, 246,
247, 248 | reprf 34627 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
| 250 | 249 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
| 251 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇)) |
| 252 | 250, 251 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁)) |
| 253 | 39, 252 | sselid 3981 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ) |
| 254 | 235, 237,
239, 241, 244, 253 | breprexplemb 34646 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 255 | 233, 254 | fprodcl 15988 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 256 | 232, 255 | fsumcl 15769 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 257 | 70 | 3adant2 1132 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆)) |
| 258 | 72 | 3adant2 1132 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ) |
| 259 | 234, 236,
238, 240, 257, 258 | breprexplemb 34646 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 260 | 229 | zcnd 12723 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ) |
| 261 | | simp3 1139 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
| 262 | 261 | elfzelzd 13565 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ) |
| 263 | 262 | zcnd 12723 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ) |
| 264 | 260, 263 | subnegd 11627 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏)) |
| 265 | 262 | znegcld 12724 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ) |
| 266 | | eluzle 12891 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(ℤ≥‘-𝑏) → -𝑏 ≤ 𝑚) |
| 267 | 228, 266 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ≤ 𝑚) |
| 268 | | znn0sub 12664 |
. . . . . . . . . . . 12
⊢ ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏 ≤ 𝑚 ↔ (𝑚 − -𝑏) ∈
ℕ0)) |
| 269 | 268 | biimpa 476 |
. . . . . . . . . . 11
⊢ (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏 ≤ 𝑚) → (𝑚 − -𝑏) ∈
ℕ0) |
| 270 | 265, 229,
267, 269 | syl21anc 838 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈
ℕ0) |
| 271 | 264, 270 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈
ℕ0) |
| 272 | 238, 271 | expcld 14186 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ) |
| 273 | 259, 272 | mulcld 11281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ) |
| 274 | 256, 273 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ) |
| 275 | 58 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈
ℕ0) |
| 276 | | ssidd 4007 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁)) |
| 277 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) |
| 278 | 277 | elfzelzd 13565 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ) |
| 279 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁)) |
| 280 | 279 | elfzelzd 13565 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ) |
| 281 | 278, 280 | zsubcld 12727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛 − 𝑏) ∈ ℤ) |
| 282 | 1 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈
ℕ0) |
| 283 | 25 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ) |
| 284 | 275 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ) |
| 285 | 283, 284 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ) |
| 286 | 280 | zred 12722 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ) |
| 287 | 219 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈
ℕ0) |
| 288 | 287, 74 | nn0addcld 12591 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈
ℕ0) |
| 289 | 184 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 1 ∈
ℕ0) |
| 290 | 288, 289 | nn0addcld 12591 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈
ℕ0) |
| 291 | | fz2ssnn0 32787 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 →
((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆
ℕ0) |
| 292 | 290, 291 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆
ℕ0) |
| 293 | 292 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0) |
| 294 | 293 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ) |
| 295 | 23 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ) |
| 296 | 275 | nn0zd 12639 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ) |
| 297 | 295, 296 | zmulcld 12728 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ) |
| 298 | 297, 280 | zaddcld 12726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ) |
| 299 | | elfzle1 13567 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) |
| 300 | 277, 299 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) |
| 301 | | zltp1le 12667 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)) |
| 302 | 301 | biimpar 477 |
. . . . . . . . . . . . 13
⊢
(((((𝑇 ·
𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛) |
| 303 | 298, 278,
300, 302 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛) |
| 304 | | ltaddsub 11737 |
. . . . . . . . . . . . 13
⊢ (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛 − 𝑏))) |
| 305 | 304 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛 − 𝑏)) |
| 306 | 285, 286,
294, 303, 305 | syl31anc 1375 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛 − 𝑏)) |
| 307 | 275, 276,
281, 282, 306 | reprgt 34636 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅) |
| 308 | 307 | sumeq1d 15736 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
| 309 | | sum0 15757 |
. . . . . . . . 9
⊢
Σ𝑑 ∈
∅ ∏𝑎 ∈
(0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0 |
| 310 | 308, 309 | eqtrdi 2793 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0) |
| 311 | 310 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
| 312 | 73 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 313 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ) |
| 314 | 278 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ) |
| 315 | 280 | zcnd 12723 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ) |
| 316 | 314, 315 | npcand 11624 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) = 𝑛) |
| 317 | 316, 293 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) ∈
ℕ0) |
| 318 | 313, 317 | expcld 14186 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ) |
| 319 | 312, 318 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ) |
| 320 | 319 | mul02d 11459 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
| 321 | 311, 320 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
| 322 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ) |
| 323 | | fzossfz 13718 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑏) ⊆
(0...𝑏) |
| 324 | | fzssz 13566 |
. . . . . . . . . . . . . 14
⊢
(0...𝑏) ⊆
ℤ |
| 325 | 323, 324 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(0..^𝑏) ⊆
ℤ |
| 326 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏)) |
| 327 | 325, 326 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ) |
| 328 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁)) |
| 329 | 328 | elfzelzd 13565 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ) |
| 330 | 327, 329 | zsubcld 12727 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℤ) |
| 331 | 1 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈
ℕ0) |
| 332 | 330 | zred 12722 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℝ) |
| 333 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ) |
| 334 | 25 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ) |
| 335 | | elfzolt2 13708 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏) |
| 336 | 335 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏) |
| 337 | 327 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ) |
| 338 | 329 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ) |
| 339 | 337, 338 | sublt0d 11889 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) < 0 ↔ 𝑛 < 𝑏)) |
| 340 | 336, 339 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 0) |
| 341 | 62 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇) |
| 342 | 332, 333,
334, 340, 341 | ltletrd 11421 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 𝑇) |
| 343 | 322, 330,
331, 342 | reprlt 34634 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅) |
| 344 | 343 | sumeq1d 15736 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
| 345 | 344, 309 | eqtrdi 2793 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0) |
| 346 | 345 | oveq1d 7446 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
| 347 | 73 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 348 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ) |
| 349 | 337 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ) |
| 350 | 338 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ) |
| 351 | 349, 350 | npcand 11624 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛) |
| 352 | | fzo0ssnn0 13785 |
. . . . . . . . . . . 12
⊢
(0..^𝑏) ⊆
ℕ0 |
| 353 | 352, 326 | sselid 3981 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0) |
| 354 | 351, 353 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) ∈
ℕ0) |
| 355 | 348, 354 | expcld 14186 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ) |
| 356 | 347, 355 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ) |
| 357 | 356 | mul02d 11459 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
| 358 | 346, 357 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
| 359 | 219, 14, 225, 274, 321, 358 | fsum2dsub 34622 |
. . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
| 360 | | nn0sscn 12531 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℂ |
| 361 | 360, 1 | sselid 3981 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℂ) |
| 362 | 360, 14 | sselid 3981 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 363 | 361, 362 | adddirp1d 11287 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁)) |
| 364 | 363 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁))) |
| 365 | 128, 360 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(0...((𝑇 + 1)
· 𝑁)) ⊆
ℂ |
| 366 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) |
| 367 | 365, 366 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ) |
| 368 | 44, 360 | sstri 3993 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
ℂ |
| 369 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
| 370 | 368, 369 | sselid 3981 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ) |
| 371 | 367, 370 | npcand 11624 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛) |
| 372 | 371 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛 − 𝑏) + 𝑏)) |
| 373 | 372 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑛) = (𝑍↑((𝑛 − 𝑏) + 𝑏))) |
| 374 | 373 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) |
| 375 | 374 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
| 376 | 375 | sumeq2dv 15738 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
| 377 | 364, 376 | sumeq12dv 15742 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
| 378 | 359, 377 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)))) |
| 379 | 105 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
| 380 | 110 | adantlr 715 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ) |
| 381 | 76 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
| 382 | 381 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
| 383 | 379, 380,
382 | mulassd 11284 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))) |
| 384 | 73 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 385 | 75 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑏) ∈ ℂ) |
| 386 | 380, 384,
385 | mulassd 11284 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 387 | 384, 380,
385 | mulassd 11284 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏)))) |
| 388 | 380, 384 | mulcomd 11282 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) |
| 389 | 388 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏))) |
| 390 | 106 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ) |
| 391 | 74 | ad4ant13 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0) |
| 392 | 109 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0) |
| 393 | 390, 391,
392 | expaddd 14188 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍↑𝑚) · (𝑍↑𝑏))) |
| 394 | 393 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏)))) |
| 395 | 387, 389,
394 | 3eqtr4d 2787 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) |
| 396 | 386, 395 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) |
| 397 | 396 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
| 398 | 383, 397 | eqtrd 2777 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
| 399 | 398 | sumeq2dv 15738 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
| 400 | 87 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin) |
| 401 | 111 | adantlr 715 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ) |
| 402 | 400, 381,
401 | fsummulc1 15821 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 403 | 73 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
| 404 | 60 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
| 405 | 108 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0) |
| 406 | 74 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
| 407 | 405, 406 | nn0addcld 12591 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈
ℕ0) |
| 408 | 404, 407 | expcld 14186 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ) |
| 409 | 403, 408 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ) |
| 410 | 400, 409,
379 | fsummulc1 15821 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
| 411 | 399, 402,
410 | 3eqtr4rd 2788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 412 | 411 | sumeq2dv 15738 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 413 | 412 | sumeq2dv 15738 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
| 414 | 218, 378,
413 | 3eqtr2rd 2784 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
| 415 | 80, 113, 414 | 3eqtr2d 2783 |
. 2
⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
| 416 | 6, 78, 415 | 3eqtrd 2781 |
1
⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |