Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  breprexplemc Structured version   Visualization version   GIF version

Theorem breprexplemc 34625
Description: Lemma for breprexp 34626 (induction step). (Contributed by Thierry Arnoux, 6-Dec-2021.)
Hypotheses
Ref Expression
breprexp.n (𝜑𝑁 ∈ ℕ0)
breprexp.s (𝜑𝑆 ∈ ℕ0)
breprexp.z (𝜑𝑍 ∈ ℂ)
breprexp.h (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
breprexplemc.t (𝜑𝑇 ∈ ℕ0)
breprexplemc.s (𝜑 → (𝑇 + 1) ≤ 𝑆)
breprexplemc.1 (𝜑 → ∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
Assertion
Ref Expression
breprexplemc (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
Distinct variable groups:   𝑚,𝑁   𝑆,𝑎,𝑚   𝑚,𝑍   𝑚,𝐿   𝑇,𝑎,𝑏,𝑑,𝑚   𝑍,𝑎,𝑏,𝑑   𝐿,𝑎,𝑏,𝑑   𝜑,𝑎,𝑏,𝑑,𝑚   𝑁,𝑎,𝑏,𝑑
Allowed substitution hints:   𝑆(𝑏,𝑑)

Proof of Theorem breprexplemc
Dummy variables 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breprexplemc.t . . . . 5 (𝜑𝑇 ∈ ℕ0)
2 nn0uz 12917 . . . . 5 0 = (ℤ‘0)
31, 2eleqtrdi 2848 . . . 4 (𝜑𝑇 ∈ (ℤ‘0))
4 fzosplitsn 13810 . . . 4 (𝑇 ∈ (ℤ‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
53, 4syl 17 . . 3 (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
65prodeq1d 15952 . 2 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
7 nfv 1911 . . 3 𝑎𝜑
8 nfcv 2902 . . 3 𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))
9 fzofi 14011 . . . 4 (0..^𝑇) ∈ Fin
109a1i 11 . . 3 (𝜑 → (0..^𝑇) ∈ Fin)
11 fzonel 13709 . . . 4 ¬ 𝑇 ∈ (0..^𝑇)
1211a1i 11 . . 3 (𝜑 → ¬ 𝑇 ∈ (0..^𝑇))
13 fzfid 14010 . . . 4 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin)
14 breprexp.n . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
1514ad2antrr 726 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
16 breprexp.s . . . . . . 7 (𝜑𝑆 ∈ ℕ0)
1716ad2antrr 726 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
18 breprexp.z . . . . . . 7 (𝜑𝑍 ∈ ℂ)
1918ad2antrr 726 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
20 breprexp.h . . . . . . . 8 (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
2120adantr 480 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
2221adantr 480 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
231nn0zd 12636 . . . . . . . . . 10 (𝜑𝑇 ∈ ℤ)
2416nn0zd 12636 . . . . . . . . . 10 (𝜑𝑆 ∈ ℤ)
251nn0red 12585 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
26 1red 11259 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
2725, 26readdcld 11287 . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ∈ ℝ)
2816nn0red 12585 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
2925lep1d 12196 . . . . . . . . . . 11 (𝜑𝑇 ≤ (𝑇 + 1))
30 breprexplemc.s . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ≤ 𝑆)
3125, 27, 28, 29, 30letrd 11415 . . . . . . . . . 10 (𝜑𝑇𝑆)
32 eluz1 12879 . . . . . . . . . . 11 (𝑇 ∈ ℤ → (𝑆 ∈ (ℤ𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇𝑆)))
3332biimpar 477 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇𝑆)) → 𝑆 ∈ (ℤ𝑇))
3423, 24, 31, 33syl12anc 837 . . . . . . . . 9 (𝜑𝑆 ∈ (ℤ𝑇))
35 fzoss2 13723 . . . . . . . . 9 (𝑆 ∈ (ℤ𝑇) → (0..^𝑇) ⊆ (0..^𝑆))
3634, 35syl 17 . . . . . . . 8 (𝜑 → (0..^𝑇) ⊆ (0..^𝑆))
3736sselda 3994 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
3837adantr 480 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆))
39 fz1ssnn 13591 . . . . . . . 8 (1...𝑁) ⊆ ℕ
4039a1i 11 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
4140sselda 3994 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
4215, 17, 19, 22, 38, 41breprexplemb 34624 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) ∈ ℂ)
43 nnssnn0 12526 . . . . . . . . . . 11 ℕ ⊆ ℕ0
4439, 43sstri 4004 . . . . . . . . . 10 (1...𝑁) ⊆ ℕ0
4544a1i 11 . . . . . . . . 9 (𝜑 → (1...𝑁) ⊆ ℕ0)
4645ralrimivw 3147 . . . . . . . 8 (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆ ℕ0)
4746r19.21bi 3248 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ0)
4847sselda 3994 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
4919, 48expcld 14182 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
5042, 49mulcld 11278 . . . 4 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
5113, 50fsumcl 15765 . . 3 ((𝜑𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
52 simpl 482 . . . . . . 7 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇)
5352fveq2d 6910 . . . . . 6 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (𝐿𝑎) = (𝐿𝑇))
5453fveq1d 6908 . . . . 5 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) = ((𝐿𝑇)‘𝑏))
5554oveq1d 7445 . . . 4 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
5655sumeq2dv 15734 . . 3 (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
57 fzfid 14010 . . . 4 (𝜑 → (1...𝑁) ∈ Fin)
5814adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
5916adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
6018adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
6120adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
621nn0ge0d 12587 . . . . . . . 8 (𝜑 → 0 ≤ 𝑇)
63 zltp1le 12664 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6423, 24, 63syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6530, 64mpbird 257 . . . . . . . 8 (𝜑𝑇 < 𝑆)
66 0zd 12622 . . . . . . . . 9 (𝜑 → 0 ∈ ℤ)
67 elfzo 13697 . . . . . . . . 9 ((𝑇 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6823, 66, 24, 67syl3anc 1370 . . . . . . . 8 (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6962, 65, 68mpbir2and 713 . . . . . . 7 (𝜑𝑇 ∈ (0..^𝑆))
7069adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
7139a1i 11 . . . . . . 7 (𝜑 → (1...𝑁) ⊆ ℕ)
7271sselda 3994 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
7358, 59, 60, 61, 70, 72breprexplemb 34624 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
7445sselda 3994 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
7560, 74expcld 14182 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
7673, 75mulcld 11278 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
7757, 76fsumcl 15765 . . 3 (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
787, 8, 10, 1, 12, 51, 56, 77fprodsplitsn 16021 . 2 (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
79 breprexplemc.1 . . . 4 (𝜑 → ∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
8079oveq1d 7445 . . 3 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
81 fzfid 14010 . . . 4 (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin)
8239a1i 11 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ)
83 simpr 484 . . . . . . 7 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁)))
8483elfzelzd 13561 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ)
851adantr 480 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈ ℕ0)
8657adantr 480 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin)
8782, 84, 85, 86reprfi 34609 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
889a1i 11 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
8914adantr 480 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈ ℕ0)
9089ad2antrr 726 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
9116ad3antrrr 730 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
9218ad3antrrr 730 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
9320ad3antrrr 730 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
9436ad2antrr 726 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
9594sselda 3994 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
9639a1i 11 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
9784ad2antrr 726 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ)
9885ad2antrr 726 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
99 simplr 769 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
10096, 97, 98, 99reprf 34605 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
101 simpr 484 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
102100, 101ffvelcdmd 7104 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
10339, 102sselid 3992 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
10490, 91, 92, 93, 95, 103breprexplemb 34624 . . . . . . 7 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10588, 104fprodcl 15984 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10618ad2antrr 726 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
107 fz0ssnn0 13658 . . . . . . . . 9 (0...(𝑇 · 𝑁)) ⊆ ℕ0
108107, 83sselid 3992 . . . . . . . 8 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0)
109108adantr 480 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
110106, 109expcld 14182 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
111105, 110mulcld 11278 . . . . 5 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11287, 111fsumcl 15765 . . . 4 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11381, 57, 112, 76fsum2mul 15821 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
11439a1i 11 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
115 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁)))
116115elfzelzd 13561 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ)
117116adantr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
118 simpr 484 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
119118elfzelzd 13561 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
120117, 119zsubcld 12724 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚𝑏) ∈ ℤ)
1211adantr 480 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈ ℕ0)
122121adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
12357adantr 480 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin)
124123adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
125114, 120, 122, 124reprfi 34609 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚𝑏)) ∈ Fin)
12673adantlr 715 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
12718adantr 480 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ)
128 fz0ssnn0 13658 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℕ0
129128, 115sselid 3992 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0)
130127, 129expcld 14182 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍𝑚) ∈ ℂ)
131130adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑚) ∈ ℂ)
132126, 131mulcld 11278 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑚)) ∈ ℂ)
1339a1i 11 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (0..^𝑇) ∈ Fin)
13414adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈ ℕ0)
135134adantr 480 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
136135ad2antrr 726 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
13716ad4antr 732 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
138127ad3antrrr 730 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
13920ad4antr 732 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
14037ad5ant15 759 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
14139a1i 11 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
142120ad2antrr 726 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚𝑏) ∈ ℤ)
143122ad2antrr 726 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
144 simplr 769 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
145141, 142, 143, 144reprf 34605 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
146 simpr 484 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
147145, 146ffvelcdmd 7104 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
14839, 147sselid 3992 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
149136, 137, 138, 139, 140, 148breprexplemb 34624 . . . . . . . . . 10 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
150133, 149fprodcl 15984 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
151125, 132, 150fsummulc1 15817 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
152151sumeq2dv 15734 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
153 elfzle2 13564 . . . . . . . . . . 11 (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
154153adantl 481 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
155134ad2antrr 726 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ0)
15616ad3antrrr 730 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈ ℕ0)
157127ad2antrr 726 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ)
15820ad3antrrr 730 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
15923peano2zd 12722 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 + 1) ∈ ℤ)
160 eluz 12889 . . . . . . . . . . . . . . . 16 (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈ (ℤ‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆))
161160biimpar 477 . . . . . . . . . . . . . . 15 ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ‘(𝑇 + 1)))
162159, 24, 30, 161syl21anc 838 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ (ℤ‘(𝑇 + 1)))
163 fzoss2 13723 . . . . . . . . . . . . . 14 (𝑆 ∈ (ℤ‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
164162, 163syl 17 . . . . . . . . . . . . 13 (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
165164ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
166 simplr 769 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1)))
167165, 166sseldd 3995 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆))
168 simpr 484 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
169155, 156, 157, 158, 167, 168breprexplemb 34624 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿𝑥)‘𝑦) ∈ ℂ)
170134, 121, 129, 154, 169breprexplema 34623 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)))
171170oveq1d 7445 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
172126adantr 480 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
173150, 172mulcld 11278 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
174125, 173fsumcl 15765 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
175123, 130, 174fsummulc1 15817 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
176125, 131, 173fsummulc1 15817 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
177131adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (𝑍𝑚) ∈ ℂ)
178150, 172, 177mulassd 11281 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
179178sumeq2dv 15734 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
180176, 179eqtrd 2774 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
181180sumeq2dv 15734 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
182171, 175, 1813eqtrd 2778 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
18339a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ)
184 1nn0 12539 . . . . . . . . . . 11 1 ∈ ℕ0
185184a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈ ℕ0)
186121, 185nn0addcld 12588 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈ ℕ0)
187183, 116, 186, 123reprfi 34609 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin)
188 fzofi 14011 . . . . . . . . . 10 (0..^(𝑇 + 1)) ∈ Fin
189188a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin)
190134ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈ ℕ0)
19116ad3antrrr 730 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈ ℕ0)
192127ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ)
19320ad3antrrr 730 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
194164ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
195194sselda 3994 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆))
19639a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ)
197116ad2antrr 726 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ)
198186ad2antrr 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))𝑚))
200196, 197, 198, 199reprf 34605 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁))
201 simpr 484 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1)))
202200, 201ffvelcdmd 7104 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ (1...𝑁))
20339, 202sselid 3992 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ ℕ)
204190, 191, 192, 193, 195, 203breprexplemb 34624 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
205189, 204fprodcl 15984 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
206187, 130, 205fsummulc1 15817 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
207152, 182, 2063eqtr2rd 2781 . . . . . 6 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
208207sumeq2dv 15734 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
209 oveq1 7437 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑛𝑏) = (𝑚𝑏))
210209oveq2d 7446 . . . . . . . . . 10 (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
211210sumeq1d 15732 . . . . . . . . 9 (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
212 oveq2 7438 . . . . . . . . . 10 (𝑛 = 𝑚 → (𝑍𝑛) = (𝑍𝑚))
213212oveq2d 7446 . . . . . . . . 9 (𝑛 = 𝑚 → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
214211, 213oveq12d 7448 . . . . . . . 8 (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
215214adantr 480 . . . . . . 7 ((𝑛 = 𝑚𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
216215sumeq2dv 15734 . . . . . 6 (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
217216cbvsumv 15728 . . . . 5 Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
218208, 217eqtr4di 2792 . . . 4 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
2191, 14nn0mulcld 12589 . . . . . 6 (𝜑 → (𝑇 · 𝑁) ∈ ℕ0)
220 oveq2 7438 . . . . . . . 8 (𝑚 = (𝑛𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛𝑏)))
221220sumeq1d 15732 . . . . . . 7 (𝑚 = (𝑛𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
222 oveq1 7437 . . . . . . . . 9 (𝑚 = (𝑛𝑏) → (𝑚 + 𝑏) = ((𝑛𝑏) + 𝑏))
223222oveq2d 7446 . . . . . . . 8 (𝑚 = (𝑛𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛𝑏) + 𝑏)))
224223oveq2d 7446 . . . . . . 7 (𝑚 = (𝑛𝑏) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
225221, 224oveq12d 7448 . . . . . 6 (𝑚 = (𝑛𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
22639a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
227 uzssz 12896 . . . . . . . . . 10 (ℤ‘-𝑏) ⊆ ℤ
228 simp2 1136 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ‘-𝑏))
229227, 228sselid 3992 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
23013ad2ant1 1132 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
231573ad2ant1 1132 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
232226, 229, 230, 231reprfi 34609 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
2339a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
234583adant2 1130 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
235234ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
236593adant2 1130 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
237236ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
238603adant2 1130 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
239238ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
240613adant2 1130 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
241240ad2antrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
242363ad2ant1 1132 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆))
243242adantr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
244243sselda 3994 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
24539a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ)
246229adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ)
247230adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈ ℕ0)
248 simpr 484 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
249245, 246, 247, 248reprf 34605 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
250249adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
251 simpr 484 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
252250, 251ffvelcdmd 7104 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
25339, 252sselid 3992 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
254235, 237, 239, 241, 244, 253breprexplemb 34624 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
255233, 254fprodcl 15984 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
256232, 255fsumcl 15765 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
257703adant2 1130 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
258723adant2 1130 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
259234, 236, 238, 240, 257, 258breprexplemb 34624 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
260229zcnd 12720 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ)
261 simp3 1137 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
262261elfzelzd 13561 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
263262zcnd 12720 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
264260, 263subnegd 11624 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏))
265262znegcld 12721 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ)
266 eluzle 12888 . . . . . . . . . . . 12 (𝑚 ∈ (ℤ‘-𝑏) → -𝑏𝑚)
267228, 266syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏𝑚)
268 znn0sub 12661 . . . . . . . . . . . 12 ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏𝑚 ↔ (𝑚 − -𝑏) ∈ ℕ0))
269268biimpa 476 . . . . . . . . . . 11 (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏𝑚) → (𝑚 − -𝑏) ∈ ℕ0)
270265, 229, 267, 269syl21anc 838 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈ ℕ0)
271264, 270eqeltrrd 2839 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
272238, 271expcld 14182 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
273259, 272mulcld 11278 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
274256, 273mulcld 11278 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ)
27558adantr 480 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℕ0)
276 ssidd 4018 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁))
277 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)))
278277elfzelzd 13561 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ)
279 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁))
280279elfzelzd 13561 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ)
281278, 280zsubcld 12724 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛𝑏) ∈ ℤ)
2821ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℕ0)
28325ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ)
284275nn0red 12585 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ)
285283, 284remulcld 11288 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ)
286280zred 12719 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ)
287219adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈ ℕ0)
288287, 74nn0addcld 12588 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈ ℕ0)
289184a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → 1 ∈ ℕ0)
290288, 289nn0addcld 12588 . . . . . . . . . . . . . . 15 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0)
291 fz2ssnn0 32793 . . . . . . . . . . . . . . 15 ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
292290, 291syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
293292sselda 3994 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0)
294293nn0red 12585 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ)
29523ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ)
296275nn0zd 12636 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ)
297295, 296zmulcld 12725 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ)
298297, 280zaddcld 12723 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ)
299 elfzle1 13563 . . . . . . . . . . . . . 14 (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
300277, 299syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
301 zltp1le 12664 . . . . . . . . . . . . . 14 ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛))
302301biimpar 477 . . . . . . . . . . . . 13 (((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
303298, 278, 300, 302syl21anc 838 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
304 ltaddsub 11734 . . . . . . . . . . . . 13 (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛𝑏)))
305304biimpa 476 . . . . . . . . . . . 12 ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛𝑏))
306285, 286, 294, 303, 305syl31anc 1372 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛𝑏))
307275, 276, 281, 282, 306reprgt 34614 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
308307sumeq1d 15732 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
309 sum0 15753 . . . . . . . . 9 Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0
310308, 309eqtrdi 2790 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
311310oveq1d 7445 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
31273adantr 480 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
31360adantr 480 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ)
314278zcnd 12720 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ)
315280zcnd 12720 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ)
316314, 315npcand 11621 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) = 𝑛)
317316, 293eqeltrd 2838 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
318313, 317expcld 14182 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
319312, 318mulcld 11278 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
320319mul02d 11456 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
321311, 320eqtrd 2774 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
32239a1i 11 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ)
323 fzossfz 13714 . . . . . . . . . . . . . 14 (0..^𝑏) ⊆ (0...𝑏)
324 fzssz 13562 . . . . . . . . . . . . . 14 (0...𝑏) ⊆ ℤ
325323, 324sstri 4004 . . . . . . . . . . . . 13 (0..^𝑏) ⊆ ℤ
326 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏))
327325, 326sselid 3992 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ)
328 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁))
329328elfzelzd 13561 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ)
330327, 329zsubcld 12724 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℤ)
3311ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℕ0)
332330zred 12719 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℝ)
333 0red 11261 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ)
33425ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ)
335 elfzolt2 13704 . . . . . . . . . . . . . 14 (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏)
336335adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏)
337327zred 12719 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ)
338329zred 12719 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ)
339337, 338sublt0d 11886 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) < 0 ↔ 𝑛 < 𝑏))
340336, 339mpbird 257 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 0)
34162ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇)
342332, 333, 334, 340, 341ltletrd 11418 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 𝑇)
343322, 330, 331, 342reprlt 34612 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
344343sumeq1d 15732 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
345344, 309eqtrdi 2790 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
346345oveq1d 7445 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
34773adantr 480 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
34860adantr 480 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ)
349337recnd 11286 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ)
350338recnd 11286 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ)
351349, 350npcand 11621 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) = 𝑛)
352 fzo0ssnn0 13781 . . . . . . . . . . . 12 (0..^𝑏) ⊆ ℕ0
353352, 326sselid 3992 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0)
354351, 353eqeltrd 2838 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
355348, 354expcld 14182 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
356347, 355mulcld 11278 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
357356mul02d 11456 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
358346, 357eqtrd 2774 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
359219, 14, 225, 274, 321, 358fsum2dsub 34600 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
360 nn0sscn 12528 . . . . . . . . 9 0 ⊆ ℂ
361360, 1sselid 3992 . . . . . . . 8 (𝜑𝑇 ∈ ℂ)
362360, 14sselid 3992 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
363361, 362adddirp1d 11284 . . . . . . 7 (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁))
364363oveq2d 7446 . . . . . 6 (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁)))
365128, 360sstri 4004 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℂ
366 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁)))
367365, 366sselid 3992 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
36844, 360sstri 4004 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℂ
369 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
370368, 369sselid 3992 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
371367, 370npcand 11621 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛𝑏) + 𝑏) = 𝑛)
372371eqcomd 2740 . . . . . . . . . 10 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛𝑏) + 𝑏))
373372oveq2d 7446 . . . . . . . . 9 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑛) = (𝑍↑((𝑛𝑏) + 𝑏)))
374373oveq2d 7446 . . . . . . . 8 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
375374oveq2d 7446 . . . . . . 7 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
376375sumeq2dv 15734 . . . . . 6 ((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
377364, 376sumeq12dv 15738 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
378359, 377eqtr4d 2777 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
379105adantlr 715 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
380110adantlr 715 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
38176adantlr 715 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
382381adantr 480 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
383379, 380, 382mulassd 11281 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))))
38473ad4ant13 751 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
38575ad4ant13 751 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑏) ∈ ℂ)
386380, 384, 385mulassd 11281 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
387384, 380, 385mulassd 11281 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
388380, 384mulcomd 11279 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
389388oveq1d 7445 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)))
390106adantlr 715 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
39174ad4ant13 751 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0)
392109adantlr 715 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
393390, 391, 392expaddd 14184 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍𝑚) · (𝑍𝑏)))
394393oveq2d 7446 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
395387, 389, 3943eqtr4d 2784 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
396386, 395eqtr3d 2776 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
397396oveq2d 7446 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
398383, 397eqtrd 2774 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
399398sumeq2dv 15734 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
40087adantr 480 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
401111adantlr 715 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
402400, 381, 401fsummulc1 15817 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
40373adantlr 715 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
40460adantlr 715 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
405108adantr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0)
40674adantlr 715 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
407405, 406nn0addcld 12588 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
408404, 407expcld 14182 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
409403, 408mulcld 11278 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
410400, 409, 379fsummulc1 15817 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
411399, 402, 4103eqtr4rd 2785 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
412411sumeq2dv 15734 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
413412sumeq2dv 15734 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
414218, 378, 4133eqtr2rd 2781 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
41580, 113, 4143eqtr2d 2780 . 2 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
4166, 78, 4153eqtrd 2778 1 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  cun 3960  wss 3962  c0 4338  {csn 4630   class class class wbr 5147  wf 6558  cfv 6562  (class class class)co 7430  m cmap 8864  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   < clt 11292  cle 11293  cmin 11489  -cneg 11490  cn 12263  0cn0 12523  cz 12610  cuz 12875  ...cfz 13543  ..^cfzo 13690  cexp 14098  Σcsu 15718  cprod 15935  reprcrepr 34601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-disj 5115  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-pm 8867  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-ico 13389  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719  df-prod 15936  df-repr 34602
This theorem is referenced by:  breprexp  34626
  Copyright terms: Public domain W3C validator