Step | Hyp | Ref
| Expression |
1 | | breprexplemc.t |
. . . . 5
⊢ (𝜑 → 𝑇 ∈
ℕ0) |
2 | | nn0uz 12279 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
3 | 1, 2 | eleqtrdi 2923 |
. . . 4
⊢ (𝜑 → 𝑇 ∈
(ℤ≥‘0)) |
4 | | fzosplitsn 13144 |
. . . 4
⊢ (𝑇 ∈
(ℤ≥‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇})) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇})) |
6 | 5 | prodeq1d 15274 |
. 2
⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏))) |
7 | | nfv 1911 |
. . 3
⊢
Ⅎ𝑎𝜑 |
8 | | nfcv 2977 |
. . 3
⊢
Ⅎ𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) |
9 | | fzofi 13341 |
. . . 4
⊢
(0..^𝑇) ∈
Fin |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → (0..^𝑇) ∈ Fin) |
11 | | fzonel 13050 |
. . . 4
⊢ ¬
𝑇 ∈ (0..^𝑇) |
12 | 11 | a1i 11 |
. . 3
⊢ (𝜑 → ¬ 𝑇 ∈ (0..^𝑇)) |
13 | | fzfid 13340 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin) |
14 | | breprexp.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
15 | 14 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
16 | | breprexp.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
17 | 16 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) |
18 | | breprexp.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ ℂ) |
19 | 18 | ad2antrr 724 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
20 | | breprexp.h |
. . . . . . . 8
⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
21 | 20 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
22 | 21 | adantr 483 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
23 | 1 | nn0zd 12084 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ∈ ℤ) |
24 | 16 | nn0zd 12084 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ∈ ℤ) |
25 | 1 | nn0red 11955 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℝ) |
26 | | 1red 10641 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
27 | 25, 26 | readdcld 10669 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 + 1) ∈ ℝ) |
28 | 16 | nn0red 11955 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℝ) |
29 | 25 | lep1d 11570 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ≤ (𝑇 + 1)) |
30 | | breprexplemc.s |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 + 1) ≤ 𝑆) |
31 | 25, 27, 28, 29, 30 | letrd 10796 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑇 ≤ 𝑆) |
32 | | eluz1 12246 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ ℤ → (𝑆 ∈
(ℤ≥‘𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆))) |
33 | 32 | biimpar 480 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)) → 𝑆 ∈ (ℤ≥‘𝑇)) |
34 | 23, 24, 31, 33 | syl12anc 834 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘𝑇)) |
35 | | fzoss2 13064 |
. . . . . . . . 9
⊢ (𝑆 ∈
(ℤ≥‘𝑇) → (0..^𝑇) ⊆ (0..^𝑆)) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0..^𝑇) ⊆ (0..^𝑆)) |
37 | 36 | sselda 3966 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
38 | 37 | adantr 483 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆)) |
39 | | fz1ssnn 12937 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
40 | 39 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ) |
41 | 40 | sselda 3966 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ) |
42 | 15, 17, 19, 22, 38, 41 | breprexplemb 31902 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) ∈ ℂ) |
43 | | nnssnn0 11899 |
. . . . . . . . . . 11
⊢ ℕ
⊆ ℕ0 |
44 | 39, 43 | sstri 3975 |
. . . . . . . . . 10
⊢
(1...𝑁) ⊆
ℕ0 |
45 | 44 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1...𝑁) ⊆
ℕ0) |
46 | 45 | ralrimivw 3183 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆
ℕ0) |
47 | 46 | r19.21bi 3208 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆
ℕ0) |
48 | 47 | sselda 3966 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
49 | 19, 48 | expcld 13509 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ) |
50 | 42, 49 | mulcld 10660 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
51 | 13, 50 | fsumcl 15089 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
52 | | simpl 485 |
. . . . . . 7
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇) |
53 | 52 | fveq2d 6673 |
. . . . . 6
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (𝐿‘𝑎) = (𝐿‘𝑇)) |
54 | 53 | fveq1d 6671 |
. . . . 5
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) = ((𝐿‘𝑇)‘𝑏)) |
55 | 54 | oveq1d 7170 |
. . . 4
⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) |
56 | 55 | sumeq2dv 15059 |
. . 3
⊢ (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) |
57 | | fzfid 13340 |
. . . 4
⊢ (𝜑 → (1...𝑁) ∈ Fin) |
58 | 14 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
59 | 16 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) |
60 | 18 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
61 | 20 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
62 | 1 | nn0ge0d 11957 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝑇) |
63 | | zltp1le 12031 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆)) |
64 | 23, 24, 63 | syl2anc 586 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆)) |
65 | 30, 64 | mpbird 259 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 < 𝑆) |
66 | | 0zd 11992 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℤ) |
67 | | elfzo 13039 |
. . . . . . . . 9
⊢ ((𝑇 ∈ ℤ ∧ 0 ∈
ℤ ∧ 𝑆 ∈
ℤ) → (𝑇 ∈
(0..^𝑆) ↔ (0 ≤
𝑇 ∧ 𝑇 < 𝑆))) |
68 | 23, 66, 24, 67 | syl3anc 1367 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆))) |
69 | 62, 65, 68 | mpbir2and 711 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ (0..^𝑆)) |
70 | 69 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆)) |
71 | 39 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
72 | 71 | sselda 3966 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ) |
73 | 58, 59, 60, 61, 70, 72 | breprexplemb 31902 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
74 | 45 | sselda 3966 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
75 | 60, 74 | expcld 13509 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ) |
76 | 73, 75 | mulcld 10660 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
77 | 57, 76 | fsumcl 15089 |
. . 3
⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
78 | 7, 8, 10, 1, 12, 51, 56, 77 | fprodsplitsn 15342 |
. 2
⊢ (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
79 | | breprexplemc.1 |
. . . 4
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
80 | 79 | oveq1d 7170 |
. . 3
⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
81 | | fzfid 13340 |
. . . 4
⊢ (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin) |
82 | 39 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
83 | | fz0ssnn0 13001 |
. . . . . . . 8
⊢
(0...(𝑇 ·
𝑁)) ⊆
ℕ0 |
84 | | simpr 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁))) |
85 | 83, 84 | sseldi 3964 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0) |
86 | 85 | nn0zd 12084 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ) |
87 | 1 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈
ℕ0) |
88 | 57 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin) |
89 | 82, 86, 87, 88 | reprfi 31887 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin) |
90 | 9 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin) |
91 | 14 | adantr 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈
ℕ0) |
92 | 91 | ad2antrr 724 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈
ℕ0) |
93 | 16 | ad3antrrr 728 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈
ℕ0) |
94 | 18 | ad3antrrr 728 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ) |
95 | 20 | ad3antrrr 728 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
96 | 36 | ad2antrr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆)) |
97 | 96 | sselda 3966 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
98 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ) |
99 | 86 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ) |
100 | 87 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈
ℕ0) |
101 | | simplr 767 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) |
102 | 98, 99, 100, 101 | reprf 31883 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
103 | | simpr 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇)) |
104 | 102, 103 | ffvelrnd 6851 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁)) |
105 | 39, 104 | sseldi 3964 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ) |
106 | 92, 93, 94, 95, 97, 105 | breprexplemb 31902 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
107 | 90, 106 | fprodcl 15305 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
108 | 18 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ) |
109 | 85 | adantr 483 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0) |
110 | 108, 109 | expcld 13509 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ) |
111 | 107, 110 | mulcld 10660 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ) |
112 | 89, 111 | fsumcl 15089 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ) |
113 | 81, 57, 112, 76 | fsum2mul 15143 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
114 | 39 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ) |
115 | | fzssz 12908 |
. . . . . . . . . . . . 13
⊢
(0...((𝑇 + 1)
· 𝑁)) ⊆
ℤ |
116 | | simpr 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) |
117 | 115, 116 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ) |
118 | 117 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ) |
119 | | fzssz 12908 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
ℤ |
120 | | simpr 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
121 | 119, 120 | sseldi 3964 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ) |
122 | 118, 121 | zsubcld 12091 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − 𝑏) ∈ ℤ) |
123 | 1 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈
ℕ0) |
124 | 123 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈
ℕ0) |
125 | 57 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin) |
126 | 125 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin) |
127 | 114, 122,
124, 126 | reprfi 31887 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)) ∈ Fin) |
128 | 73 | adantlr 713 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
129 | 18 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ) |
130 | | fz0ssnn0 13001 |
. . . . . . . . . . . . 13
⊢
(0...((𝑇 + 1)
· 𝑁)) ⊆
ℕ0 |
131 | 130, 116 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0) |
132 | 129, 131 | expcld 13509 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍↑𝑚) ∈ ℂ) |
133 | 132 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑚) ∈ ℂ) |
134 | 128, 133 | mulcld 10660 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) ∈ ℂ) |
135 | 9 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (0..^𝑇) ∈ Fin) |
136 | 14 | adantr 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈
ℕ0) |
137 | 136 | adantr 483 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
138 | 137 | ad2antrr 724 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈
ℕ0) |
139 | 16 | ad4antr 730 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈
ℕ0) |
140 | 129 | ad3antrrr 728 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ) |
141 | 20 | ad4antr 730 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
142 | 37 | ad5ant15 757 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
143 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ) |
144 | 122 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚 − 𝑏) ∈ ℤ) |
145 | 124 | ad2antrr 724 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈
ℕ0) |
146 | | simplr 767 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) |
147 | 143, 144,
145, 146 | reprf 31883 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
148 | | simpr 487 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇)) |
149 | 147, 148 | ffvelrnd 6851 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁)) |
150 | 39, 149 | sseldi 3964 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ) |
151 | 138, 139,
140, 141, 142, 150 | breprexplemb 31902 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
152 | 135, 151 | fprodcl 15305 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
153 | 127, 134,
152 | fsummulc1 15139 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
154 | 153 | sumeq2dv 15059 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
155 | | elfzle2 12910 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁)) |
156 | 155 | adantl 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁)) |
157 | 136 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈
ℕ0) |
158 | 16 | ad3antrrr 728 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈
ℕ0) |
159 | 129 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ) |
160 | 20 | ad3antrrr 728 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
161 | 23 | peano2zd 12089 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 + 1) ∈ ℤ) |
162 | | eluz 12256 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈
(ℤ≥‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆)) |
163 | 162 | biimpar 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ≥‘(𝑇 + 1))) |
164 | 161, 24, 30, 163 | syl21anc 835 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘(𝑇 + 1))) |
165 | | fzoss2 13064 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈
(ℤ≥‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
166 | 164, 165 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
167 | 166 | ad3antrrr 728 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
168 | | simplr 767 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1))) |
169 | 167, 168 | sseldd 3967 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆)) |
170 | | simpr 487 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ) |
171 | 157, 158,
159, 160, 169, 170 | breprexplemb 31902 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿‘𝑥)‘𝑦) ∈ ℂ) |
172 | 136, 123,
131, 156, 171 | breprexplema 31901 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏))) |
173 | 172 | oveq1d 7170 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚))) |
174 | 128 | adantr 483 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
175 | 152, 174 | mulcld 10660 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ) |
176 | 127, 175 | fsumcl 15089 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ) |
177 | 125, 132,
176 | fsummulc1 15139 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚))) |
178 | 127, 133,
175 | fsummulc1 15139 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚))) |
179 | 133 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (𝑍↑𝑚) ∈ ℂ) |
180 | 152, 174,
179 | mulassd 10663 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
181 | 180 | sumeq2dv 15059 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
182 | 178, 181 | eqtrd 2856 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
183 | 182 | sumeq2dv 15059 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
184 | 173, 177,
183 | 3eqtrd 2860 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
185 | 39 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ) |
186 | | 1nn0 11912 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
187 | 186 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈
ℕ0) |
188 | 123, 187 | nn0addcld 11958 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈
ℕ0) |
189 | 185, 117,
188, 125 | reprfi 31887 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin) |
190 | | fzofi 13341 |
. . . . . . . . . 10
⊢
(0..^(𝑇 + 1)) ∈
Fin |
191 | 190 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin) |
192 | 136 | ad2antrr 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈
ℕ0) |
193 | 16 | ad3antrrr 728 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈
ℕ0) |
194 | 129 | ad2antrr 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ) |
195 | 20 | ad3antrrr 728 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
196 | 166 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆)) |
197 | 196 | sselda 3966 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆)) |
198 | 39 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ) |
199 | 117 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ) |
200 | 188 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈
ℕ0) |
201 | | simplr 767 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) |
202 | 198, 199,
200, 201 | reprf 31883 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁)) |
203 | | simpr 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1))) |
204 | 202, 203 | ffvelrnd 6851 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁)) |
205 | 39, 204 | sseldi 3964 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ ℕ) |
206 | 192, 193,
194, 195, 197, 205 | breprexplemb 31902 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
207 | 191, 206 | fprodcl 15305 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
208 | 189, 132,
207 | fsummulc1 15139 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
209 | 154, 184,
208 | 3eqtr2rd 2863 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
210 | 209 | sumeq2dv 15059 |
. . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
211 | | oveq1 7162 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝑛 − 𝑏) = (𝑚 − 𝑏)) |
212 | 211 | oveq2d 7171 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) |
213 | 212 | sumeq1d 15057 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
214 | | oveq2 7163 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝑍↑𝑛) = (𝑍↑𝑚)) |
215 | 214 | oveq2d 7171 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) |
216 | 213, 215 | oveq12d 7173 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
217 | 216 | adantr 483 |
. . . . . . 7
⊢ ((𝑛 = 𝑚 ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
218 | 217 | sumeq2dv 15059 |
. . . . . 6
⊢ (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))) |
219 | 218 | cbvsumv 15052 |
. . . . 5
⊢
Σ𝑛 ∈
(0...((𝑇 + 1) ·
𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) |
220 | 210, 219 | syl6eqr 2874 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)))) |
221 | 1, 14 | nn0mulcld 11959 |
. . . . . 6
⊢ (𝜑 → (𝑇 · 𝑁) ∈
ℕ0) |
222 | | oveq2 7163 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 − 𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))) |
223 | 222 | sumeq1d 15057 |
. . . . . . 7
⊢ (𝑚 = (𝑛 − 𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
224 | | oveq1 7162 |
. . . . . . . . 9
⊢ (𝑚 = (𝑛 − 𝑏) → (𝑚 + 𝑏) = ((𝑛 − 𝑏) + 𝑏)) |
225 | 224 | oveq2d 7171 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 − 𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛 − 𝑏) + 𝑏))) |
226 | 225 | oveq2d 7171 |
. . . . . . 7
⊢ (𝑚 = (𝑛 − 𝑏) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) |
227 | 223, 226 | oveq12d 7173 |
. . . . . 6
⊢ (𝑚 = (𝑛 − 𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
228 | 39 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ) |
229 | | uzssz 12263 |
. . . . . . . . . 10
⊢
(ℤ≥‘-𝑏) ⊆ ℤ |
230 | | simp2 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ≥‘-𝑏)) |
231 | 229, 230 | sseldi 3964 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ) |
232 | 1 | 3ad2ant1 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈
ℕ0) |
233 | 57 | 3ad2ant1 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin) |
234 | 228, 231,
232, 233 | reprfi 31887 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin) |
235 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin) |
236 | 58 | 3adant2 1127 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈
ℕ0) |
237 | 236 | ad2antrr 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈
ℕ0) |
238 | 59 | 3adant2 1127 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈
ℕ0) |
239 | 238 | ad2antrr 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈
ℕ0) |
240 | 60 | 3adant2 1127 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
241 | 240 | ad2antrr 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ) |
242 | 61 | 3adant2 1127 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
243 | 242 | ad2antrr 724 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
244 | 36 | 3ad2ant1 1129 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆)) |
245 | 244 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆)) |
246 | 245 | sselda 3966 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆)) |
247 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ) |
248 | 231 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ) |
249 | 232 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈
ℕ0) |
250 | | simpr 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) |
251 | 247, 248,
249, 250 | reprf 31883 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
252 | 251 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁)) |
253 | | simpr 487 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇)) |
254 | 252, 253 | ffvelrnd 6851 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁)) |
255 | 39, 254 | sseldi 3964 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ) |
256 | 237, 239,
241, 243, 246, 255 | breprexplemb 31902 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
257 | 235, 256 | fprodcl 15305 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
258 | 234, 257 | fsumcl 15089 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
259 | 70 | 3adant2 1127 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆)) |
260 | 72 | 3adant2 1127 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ) |
261 | 236, 238,
240, 242, 259, 260 | breprexplemb 31902 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
262 | 231 | zcnd 12087 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ) |
263 | | simp3 1134 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
264 | 119, 263 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ) |
265 | 264 | zcnd 12087 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ) |
266 | 262, 265 | subnegd 11003 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏)) |
267 | 264 | znegcld 12088 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ) |
268 | | eluzle 12255 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(ℤ≥‘-𝑏) → -𝑏 ≤ 𝑚) |
269 | 230, 268 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ≤ 𝑚) |
270 | | znn0sub 12028 |
. . . . . . . . . . . 12
⊢ ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏 ≤ 𝑚 ↔ (𝑚 − -𝑏) ∈
ℕ0)) |
271 | 270 | biimpa 479 |
. . . . . . . . . . 11
⊢ (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏 ≤ 𝑚) → (𝑚 − -𝑏) ∈
ℕ0) |
272 | 267, 231,
269, 271 | syl21anc 835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈
ℕ0) |
273 | 266, 272 | eqeltrrd 2914 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈
ℕ0) |
274 | 240, 273 | expcld 13509 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ) |
275 | 261, 274 | mulcld 10660 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ) |
276 | 258, 275 | mulcld 10660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ) |
277 | 58 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈
ℕ0) |
278 | | ssidd 3989 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁)) |
279 | | fzssz 12908 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℤ |
280 | | simpr 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) |
281 | 279, 280 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ) |
282 | | simplr 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁)) |
283 | 119, 282 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ) |
284 | 281, 283 | zsubcld 12091 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛 − 𝑏) ∈ ℤ) |
285 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈
ℕ0) |
286 | 25 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ) |
287 | 277 | nn0red 11955 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ) |
288 | 286, 287 | remulcld 10670 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ) |
289 | 283 | zred 12086 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ) |
290 | 221 | adantr 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈
ℕ0) |
291 | 290, 74 | nn0addcld 11958 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈
ℕ0) |
292 | 186 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 1 ∈
ℕ0) |
293 | 291, 292 | nn0addcld 11958 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈
ℕ0) |
294 | | fz2ssnn0 30507 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 →
((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆
ℕ0) |
295 | 293, 294 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆
ℕ0) |
296 | 295 | sselda 3966 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0) |
297 | 296 | nn0red 11955 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ) |
298 | 23 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ) |
299 | 277 | nn0zd 12084 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ) |
300 | 298, 299 | zmulcld 12092 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ) |
301 | 300, 283 | zaddcld 12090 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ) |
302 | | elfzle1 12909 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) |
303 | 280, 302 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) |
304 | | zltp1le 12031 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)) |
305 | 304 | biimpar 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑇 ·
𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛) |
306 | 301, 281,
303, 305 | syl21anc 835 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛) |
307 | | ltaddsub 11113 |
. . . . . . . . . . . . 13
⊢ (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛 − 𝑏))) |
308 | 307 | biimpa 479 |
. . . . . . . . . . . 12
⊢ ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛 − 𝑏)) |
309 | 288, 289,
297, 306, 308 | syl31anc 1369 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛 − 𝑏)) |
310 | 277, 278,
284, 285, 309 | reprgt 31892 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅) |
311 | 310 | sumeq1d 15057 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
312 | | sum0 15077 |
. . . . . . . . 9
⊢
Σ𝑑 ∈
∅ ∏𝑎 ∈
(0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0 |
313 | 311, 312 | syl6eq 2872 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0) |
314 | 313 | oveq1d 7170 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
315 | 73 | adantr 483 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
316 | 60 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ) |
317 | 281 | zcnd 12087 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ) |
318 | 283 | zcnd 12087 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ) |
319 | 317, 318 | npcand 11000 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) = 𝑛) |
320 | 319, 296 | eqeltrd 2913 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) ∈
ℕ0) |
321 | 316, 320 | expcld 13509 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ) |
322 | 315, 321 | mulcld 10660 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ) |
323 | 322 | mul02d 10837 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
324 | 314, 323 | eqtrd 2856 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
325 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ) |
326 | | fzossfz 13055 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑏) ⊆
(0...𝑏) |
327 | | fzssz 12908 |
. . . . . . . . . . . . . 14
⊢
(0...𝑏) ⊆
ℤ |
328 | 326, 327 | sstri 3975 |
. . . . . . . . . . . . 13
⊢
(0..^𝑏) ⊆
ℤ |
329 | | simpr 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏)) |
330 | 328, 329 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ) |
331 | | simplr 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁)) |
332 | 119, 331 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ) |
333 | 330, 332 | zsubcld 12091 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℤ) |
334 | 1 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈
ℕ0) |
335 | 333 | zred 12086 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℝ) |
336 | | 0red 10643 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ) |
337 | 25 | ad2antrr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ) |
338 | | elfzolt2 13046 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏) |
339 | 338 | adantl 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏) |
340 | 330 | zred 12086 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ) |
341 | 332 | zred 12086 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ) |
342 | 340, 341 | sublt0d 11265 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) < 0 ↔ 𝑛 < 𝑏)) |
343 | 339, 342 | mpbird 259 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 0) |
344 | 62 | ad2antrr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇) |
345 | 335, 336,
337, 343, 344 | ltletrd 10799 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 𝑇) |
346 | 325, 333,
334, 345 | reprlt 31890 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅) |
347 | 346 | sumeq1d 15057 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎))) |
348 | 347, 312 | syl6eq 2872 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0) |
349 | 348 | oveq1d 7170 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
350 | 73 | adantr 483 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
351 | 60 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ) |
352 | 340 | recnd 10668 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ) |
353 | 341 | recnd 10668 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ) |
354 | 352, 353 | npcand 11000 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛) |
355 | | fzo0ssnn0 13117 |
. . . . . . . . . . . 12
⊢
(0..^𝑏) ⊆
ℕ0 |
356 | 355, 329 | sseldi 3964 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0) |
357 | 354, 356 | eqeltrd 2913 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) ∈
ℕ0) |
358 | 351, 357 | expcld 13509 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ) |
359 | 350, 358 | mulcld 10660 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ) |
360 | 359 | mul02d 10837 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
361 | 349, 360 | eqtrd 2856 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0) |
362 | 221, 14, 227, 276, 324, 361 | fsum2dsub 31878 |
. . . . 5
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
363 | | nn0sscn 11901 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℂ |
364 | 363, 1 | sseldi 3964 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ ℂ) |
365 | 363, 14 | sseldi 3964 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℂ) |
366 | 364, 365 | adddirp1d 10666 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁)) |
367 | 366 | oveq2d 7171 |
. . . . . 6
⊢ (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁))) |
368 | 130, 363 | sstri 3975 |
. . . . . . . . . . . . 13
⊢
(0...((𝑇 + 1)
· 𝑁)) ⊆
ℂ |
369 | | simplr 767 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) |
370 | 368, 369 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ) |
371 | 44, 363 | sstri 3975 |
. . . . . . . . . . . . 13
⊢
(1...𝑁) ⊆
ℂ |
372 | | simpr 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
373 | 371, 372 | sseldi 3964 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ) |
374 | 370, 373 | npcand 11000 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛) |
375 | 374 | eqcomd 2827 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛 − 𝑏) + 𝑏)) |
376 | 375 | oveq2d 7171 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑛) = (𝑍↑((𝑛 − 𝑏) + 𝑏))) |
377 | 376 | oveq2d 7171 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) |
378 | 377 | oveq2d 7171 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
379 | 378 | sumeq2dv 15059 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
380 | 367, 379 | sumeq12dv 15062 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))) |
381 | 362, 380 | eqtr4d 2859 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)))) |
382 | 107 | adantlr 713 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ) |
383 | 110 | adantlr 713 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ) |
384 | 76 | adantlr 713 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
385 | 384 | adantr 483 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ) |
386 | 382, 383,
385 | mulassd 10663 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))) |
387 | 73 | ad4ant13 749 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
388 | 75 | ad4ant13 749 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑏) ∈ ℂ) |
389 | 383, 387,
388 | mulassd 10663 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
390 | 387, 383,
388 | mulassd 10663 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏)))) |
391 | 383, 387 | mulcomd 10661 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) |
392 | 391 | oveq1d 7170 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏))) |
393 | 108 | adantlr 713 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ) |
394 | 74 | ad4ant13 749 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0) |
395 | 109 | adantlr 713 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0) |
396 | 393, 394,
395 | expaddd 13511 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍↑𝑚) · (𝑍↑𝑏))) |
397 | 396 | oveq2d 7171 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏)))) |
398 | 390, 392,
397 | 3eqtr4d 2866 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) |
399 | 389, 398 | eqtr3d 2858 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) |
400 | 399 | oveq2d 7171 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
401 | 386, 400 | eqtrd 2856 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
402 | 401 | sumeq2dv 15059 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
403 | 89 | adantr 483 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin) |
404 | 111 | adantlr 713 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ) |
405 | 403, 384,
404 | fsummulc1 15139 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
406 | 73 | adantlr 713 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ) |
407 | 60 | adantlr 713 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
408 | 85 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0) |
409 | 74 | adantlr 713 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
410 | 408, 409 | nn0addcld 11958 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈
ℕ0) |
411 | 407, 410 | expcld 13509 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ) |
412 | 406, 411 | mulcld 10660 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ) |
413 | 403, 412,
382 | fsummulc1 15139 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))) |
414 | 402, 405,
413 | 3eqtr4rd 2867 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
415 | 414 | sumeq2dv 15059 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
416 | 415 | sumeq2dv 15059 |
. . . 4
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) |
417 | 220, 381,
416 | 3eqtr2rd 2863 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
418 | 80, 113, 417 | 3eqtr2d 2862 |
. 2
⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |
419 | 6, 78, 418 | 3eqtrd 2860 |
1
⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚))) |