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 31789
Description: Lemma for breprexp 31790 (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 12272 . . . . 5 0 = (ℤ‘0)
31, 2syl6eleq 2927 . . . 4 (𝜑𝑇 ∈ (ℤ‘0))
4 fzosplitsn 13138 . . . 4 (𝑇 ∈ (ℤ‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
53, 4syl 17 . . 3 (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
65prodeq1d 15267 . 2 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
7 nfv 1908 . . 3 𝑎𝜑
8 nfcv 2981 . . 3 𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))
9 fzofi 13335 . . . 4 (0..^𝑇) ∈ Fin
109a1i 11 . . 3 (𝜑 → (0..^𝑇) ∈ Fin)
11 fzonel 13044 . . . 4 ¬ 𝑇 ∈ (0..^𝑇)
1211a1i 11 . . 3 (𝜑 → ¬ 𝑇 ∈ (0..^𝑇))
13 fzfid 13334 . . . 4 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin)
14 breprexp.n . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
1514ad2antrr 722 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
16 breprexp.s . . . . . . 7 (𝜑𝑆 ∈ ℕ0)
1716ad2antrr 722 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
18 breprexp.z . . . . . . 7 (𝜑𝑍 ∈ ℂ)
1918ad2antrr 722 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
20 breprexp.h . . . . . . . 8 (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
2120adantr 481 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
2221adantr 481 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
231nn0zd 12077 . . . . . . . . . 10 (𝜑𝑇 ∈ ℤ)
2416nn0zd 12077 . . . . . . . . . 10 (𝜑𝑆 ∈ ℤ)
251nn0red 11948 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
26 1red 10634 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
2725, 26readdcld 10662 . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ∈ ℝ)
2816nn0red 11948 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
2925lep1d 11563 . . . . . . . . . . 11 (𝜑𝑇 ≤ (𝑇 + 1))
30 breprexplemc.s . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ≤ 𝑆)
3125, 27, 28, 29, 30letrd 10789 . . . . . . . . . 10 (𝜑𝑇𝑆)
32 eluz1 12239 . . . . . . . . . . 11 (𝑇 ∈ ℤ → (𝑆 ∈ (ℤ𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇𝑆)))
3332biimpar 478 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇𝑆)) → 𝑆 ∈ (ℤ𝑇))
3423, 24, 31, 33syl12anc 834 . . . . . . . . 9 (𝜑𝑆 ∈ (ℤ𝑇))
35 fzoss2 13058 . . . . . . . . 9 (𝑆 ∈ (ℤ𝑇) → (0..^𝑇) ⊆ (0..^𝑆))
3634, 35syl 17 . . . . . . . 8 (𝜑 → (0..^𝑇) ⊆ (0..^𝑆))
3736sselda 3970 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
3837adantr 481 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆))
39 fz1ssnn 12931 . . . . . . . 8 (1...𝑁) ⊆ ℕ
4039a1i 11 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
4140sselda 3970 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
4215, 17, 19, 22, 38, 41breprexplemb 31788 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) ∈ ℂ)
43 nnssnn0 11892 . . . . . . . . . . 11 ℕ ⊆ ℕ0
4439, 43sstri 3979 . . . . . . . . . 10 (1...𝑁) ⊆ ℕ0
4544a1i 11 . . . . . . . . 9 (𝜑 → (1...𝑁) ⊆ ℕ0)
4645ralrimivw 3187 . . . . . . . 8 (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆ ℕ0)
4746r19.21bi 3212 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ0)
4847sselda 3970 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
4919, 48expcld 13503 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
5042, 49mulcld 10653 . . . 4 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
5113, 50fsumcl 15082 . . 3 ((𝜑𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
52 simpl 483 . . . . . . 7 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇)
5352fveq2d 6670 . . . . . 6 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (𝐿𝑎) = (𝐿𝑇))
5453fveq1d 6668 . . . . 5 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) = ((𝐿𝑇)‘𝑏))
5554oveq1d 7166 . . . 4 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
5655sumeq2dv 15052 . . 3 (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
57 fzfid 13334 . . . 4 (𝜑 → (1...𝑁) ∈ Fin)
5814adantr 481 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
5916adantr 481 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
6018adantr 481 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
6120adantr 481 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
621nn0ge0d 11950 . . . . . . . 8 (𝜑 → 0 ≤ 𝑇)
63 zltp1le 12024 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6423, 24, 63syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6530, 64mpbird 258 . . . . . . . 8 (𝜑𝑇 < 𝑆)
66 0zd 11985 . . . . . . . . 9 (𝜑 → 0 ∈ ℤ)
67 elfzo 13033 . . . . . . . . 9 ((𝑇 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6823, 66, 24, 67syl3anc 1365 . . . . . . . 8 (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6962, 65, 68mpbir2and 709 . . . . . . 7 (𝜑𝑇 ∈ (0..^𝑆))
7069adantr 481 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
7139a1i 11 . . . . . . 7 (𝜑 → (1...𝑁) ⊆ ℕ)
7271sselda 3970 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
7358, 59, 60, 61, 70, 72breprexplemb 31788 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
7445sselda 3970 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
7560, 74expcld 13503 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
7673, 75mulcld 10653 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
7757, 76fsumcl 15082 . . 3 (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
787, 8, 10, 1, 12, 51, 56, 77fprodsplitsn 15335 . 2 (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
79 breprexplemc.1 . . . 4 (𝜑 → ∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
8079oveq1d 7166 . . 3 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
81 fzfid 13334 . . . 4 (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin)
8239a1i 11 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ)
83 fz0ssnn0 12995 . . . . . . . 8 (0...(𝑇 · 𝑁)) ⊆ ℕ0
84 simpr 485 . . . . . . . 8 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁)))
8583, 84sseldi 3968 . . . . . . 7 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0)
8685nn0zd 12077 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ)
871adantr 481 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈ ℕ0)
8857adantr 481 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin)
8982, 86, 87, 88reprfi 31773 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
909a1i 11 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
9114adantr 481 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈ ℕ0)
9291ad2antrr 722 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
9316ad3antrrr 726 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
9418ad3antrrr 726 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
9520ad3antrrr 726 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
9636ad2antrr 722 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
9796sselda 3970 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
9839a1i 11 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
9986ad2antrr 722 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ)
10087ad2antrr 722 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
101 simplr 765 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
10298, 99, 100, 101reprf 31769 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
103 simpr 485 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
104102, 103ffvelrnd 6847 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
10539, 104sseldi 3968 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
10692, 93, 94, 95, 97, 105breprexplemb 31788 . . . . . . 7 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10790, 106fprodcl 15298 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10818ad2antrr 722 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
10985adantr 481 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
110108, 109expcld 13503 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
111107, 110mulcld 10653 . . . . 5 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11289, 111fsumcl 15082 . . . 4 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11381, 57, 112, 76fsum2mul 15136 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
11439a1i 11 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
115 fzssz 12902 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℤ
116 simpr 485 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁)))
117115, 116sseldi 3968 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ)
118117adantr 481 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
119 fzssz 12902 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℤ
120 simpr 485 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
121119, 120sseldi 3968 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
122118, 121zsubcld 12084 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚𝑏) ∈ ℤ)
1231adantr 481 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈ ℕ0)
124123adantr 481 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
12557adantr 481 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin)
126125adantr 481 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
127114, 122, 124, 126reprfi 31773 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚𝑏)) ∈ Fin)
12873adantlr 711 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
12918adantr 481 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ)
130 fz0ssnn0 12995 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℕ0
131130, 116sseldi 3968 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0)
132129, 131expcld 13503 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍𝑚) ∈ ℂ)
133132adantr 481 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑚) ∈ ℂ)
134128, 133mulcld 10653 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑚)) ∈ ℂ)
1359a1i 11 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (0..^𝑇) ∈ Fin)
13614adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈ ℕ0)
137136adantr 481 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
138137ad2antrr 722 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
13916ad4antr 728 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
140129ad3antrrr 726 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
14120ad4antr 728 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
14237ad5ant15 755 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
14339a1i 11 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
144122ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚𝑏) ∈ ℤ)
145124ad2antrr 722 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
146 simplr 765 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
147143, 144, 145, 146reprf 31769 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
148 simpr 485 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
149147, 148ffvelrnd 6847 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
15039, 149sseldi 3968 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
151138, 139, 140, 141, 142, 150breprexplemb 31788 . . . . . . . . . 10 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
152135, 151fprodcl 15298 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
153127, 134, 152fsummulc1 15132 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
154153sumeq2dv 15052 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
155 elfzle2 12904 . . . . . . . . . . 11 (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
156155adantl 482 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
157136ad2antrr 722 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ0)
15816ad3antrrr 726 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈ ℕ0)
159129ad2antrr 722 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ)
16020ad3antrrr 726 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
16123peano2zd 12082 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 + 1) ∈ ℤ)
162 eluz 12249 . . . . . . . . . . . . . . . 16 (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈ (ℤ‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆))
163162biimpar 478 . . . . . . . . . . . . . . 15 ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ‘(𝑇 + 1)))
164161, 24, 30, 163syl21anc 835 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ (ℤ‘(𝑇 + 1)))
165 fzoss2 13058 . . . . . . . . . . . . . 14 (𝑆 ∈ (ℤ‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
166164, 165syl 17 . . . . . . . . . . . . 13 (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
167166ad3antrrr 726 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
168 simplr 765 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1)))
169167, 168sseldd 3971 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆))
170 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
171157, 158, 159, 160, 169, 170breprexplemb 31788 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿𝑥)‘𝑦) ∈ ℂ)
172136, 123, 131, 156, 171breprexplema 31787 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)))
173172oveq1d 7166 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
174128adantr 481 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
175152, 174mulcld 10653 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
176127, 175fsumcl 15082 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
177125, 132, 176fsummulc1 15132 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
178127, 133, 175fsummulc1 15132 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
179133adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (𝑍𝑚) ∈ ℂ)
180152, 174, 179mulassd 10656 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
181180sumeq2dv 15052 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
182178, 181eqtrd 2860 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
183182sumeq2dv 15052 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
184173, 177, 1833eqtrd 2864 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
18539a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ)
186 1nn0 11905 . . . . . . . . . . 11 1 ∈ ℕ0
187186a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈ ℕ0)
188123, 187nn0addcld 11951 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈ ℕ0)
189185, 117, 188, 125reprfi 31773 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin)
190 fzofi 13335 . . . . . . . . . 10 (0..^(𝑇 + 1)) ∈ Fin
191190a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin)
192136ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈ ℕ0)
19316ad3antrrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈ ℕ0)
194129ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ)
19520ad3antrrr 726 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
196166ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
197196sselda 3970 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆))
19839a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ)
199117ad2antrr 722 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ)
200188ad2antrr 722 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈ ℕ0)
201 simplr 765 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚))
202198, 199, 200, 201reprf 31769 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁))
203 simpr 485 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1)))
204202, 203ffvelrnd 6847 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ (1...𝑁))
20539, 204sseldi 3968 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ ℕ)
206192, 193, 194, 195, 197, 205breprexplemb 31788 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
207191, 206fprodcl 15298 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
208189, 132, 207fsummulc1 15132 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
209154, 184, 2083eqtr2rd 2867 . . . . . 6 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
210209sumeq2dv 15052 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
211 oveq1 7158 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑛𝑏) = (𝑚𝑏))
212211oveq2d 7167 . . . . . . . . . 10 (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
213212sumeq1d 15050 . . . . . . . . 9 (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
214 oveq2 7159 . . . . . . . . . 10 (𝑛 = 𝑚 → (𝑍𝑛) = (𝑍𝑚))
215214oveq2d 7167 . . . . . . . . 9 (𝑛 = 𝑚 → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
216213, 215oveq12d 7169 . . . . . . . 8 (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
217216adantr 481 . . . . . . 7 ((𝑛 = 𝑚𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
218217sumeq2dv 15052 . . . . . 6 (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
219218cbvsumv 15045 . . . . 5 Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
220210, 219syl6eqr 2878 . . . 4 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
2211, 14nn0mulcld 11952 . . . . . 6 (𝜑 → (𝑇 · 𝑁) ∈ ℕ0)
222 oveq2 7159 . . . . . . . 8 (𝑚 = (𝑛𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛𝑏)))
223222sumeq1d 15050 . . . . . . 7 (𝑚 = (𝑛𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
224 oveq1 7158 . . . . . . . . 9 (𝑚 = (𝑛𝑏) → (𝑚 + 𝑏) = ((𝑛𝑏) + 𝑏))
225224oveq2d 7167 . . . . . . . 8 (𝑚 = (𝑛𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛𝑏) + 𝑏)))
226225oveq2d 7167 . . . . . . 7 (𝑚 = (𝑛𝑏) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
227223, 226oveq12d 7169 . . . . . 6 (𝑚 = (𝑛𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
22839a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
229 uzssz 12256 . . . . . . . . . 10 (ℤ‘-𝑏) ⊆ ℤ
230 simp2 1131 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ‘-𝑏))
231229, 230sseldi 3968 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
23213ad2ant1 1127 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
233573ad2ant1 1127 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
234228, 231, 232, 233reprfi 31773 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
2359a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
236583adant2 1125 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
237236ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
238593adant2 1125 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
239238ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
240603adant2 1125 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
241240ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
242613adant2 1125 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
243242ad2antrr 722 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
244363ad2ant1 1127 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆))
245244adantr 481 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
246245sselda 3970 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
24739a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ)
248231adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ)
249232adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈ ℕ0)
250 simpr 485 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
251247, 248, 249, 250reprf 31769 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
252251adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
253 simpr 485 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
254252, 253ffvelrnd 6847 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
25539, 254sseldi 3968 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
256237, 239, 241, 243, 246, 255breprexplemb 31788 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
257235, 256fprodcl 15298 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
258234, 257fsumcl 15082 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
259703adant2 1125 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
260723adant2 1125 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
261236, 238, 240, 242, 259, 260breprexplemb 31788 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
262231zcnd 12080 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ)
263 simp3 1132 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
264119, 263sseldi 3968 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
265264zcnd 12080 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
266262, 265subnegd 10996 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏))
267264znegcld 12081 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ)
268 eluzle 12248 . . . . . . . . . . . 12 (𝑚 ∈ (ℤ‘-𝑏) → -𝑏𝑚)
269230, 268syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏𝑚)
270 znn0sub 12021 . . . . . . . . . . . 12 ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏𝑚 ↔ (𝑚 − -𝑏) ∈ ℕ0))
271270biimpa 477 . . . . . . . . . . 11 (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏𝑚) → (𝑚 − -𝑏) ∈ ℕ0)
272267, 231, 269, 271syl21anc 835 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈ ℕ0)
273266, 272eqeltrrd 2918 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
274240, 273expcld 13503 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
275261, 274mulcld 10653 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
276258, 275mulcld 10653 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ)
27758adantr 481 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℕ0)
278 ssidd 3993 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁))
279 fzssz 12902 . . . . . . . . . . . . 13 ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℤ
280 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)))
281279, 280sseldi 3968 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ)
282 simplr 765 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁))
283119, 282sseldi 3968 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ)
284281, 283zsubcld 12084 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛𝑏) ∈ ℤ)
2851ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℕ0)
28625ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ)
287277nn0red 11948 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ)
288286, 287remulcld 10663 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ)
289283zred 12079 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ)
290221adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈ ℕ0)
291290, 74nn0addcld 11951 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈ ℕ0)
292186a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → 1 ∈ ℕ0)
293291, 292nn0addcld 11951 . . . . . . . . . . . . . . 15 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0)
294 fz2ssnn0 30421 . . . . . . . . . . . . . . 15 ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
295293, 294syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
296295sselda 3970 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0)
297296nn0red 11948 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ)
29823ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ)
299277nn0zd 12077 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ)
300298, 299zmulcld 12085 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ)
301300, 283zaddcld 12083 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ)
302 elfzle1 12903 . . . . . . . . . . . . . 14 (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
303280, 302syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
304 zltp1le 12024 . . . . . . . . . . . . . 14 ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛))
305304biimpar 478 . . . . . . . . . . . . 13 (((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
306301, 281, 303, 305syl21anc 835 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
307 ltaddsub 11106 . . . . . . . . . . . . 13 (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛𝑏)))
308307biimpa 477 . . . . . . . . . . . 12 ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛𝑏))
309288, 289, 297, 306, 308syl31anc 1367 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛𝑏))
310277, 278, 284, 285, 309reprgt 31778 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
311310sumeq1d 15050 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
312 sum0 15070 . . . . . . . . 9 Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0
313311, 312syl6eq 2876 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
314313oveq1d 7166 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
31573adantr 481 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
31660adantr 481 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ)
317281zcnd 12080 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ)
318283zcnd 12080 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ)
319317, 318npcand 10993 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) = 𝑛)
320319, 296eqeltrd 2917 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
321316, 320expcld 13503 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
322315, 321mulcld 10653 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
323322mul02d 10830 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
324314, 323eqtrd 2860 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
32539a1i 11 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ)
326 fzossfz 13049 . . . . . . . . . . . . . 14 (0..^𝑏) ⊆ (0...𝑏)
327 fzssz 12902 . . . . . . . . . . . . . 14 (0...𝑏) ⊆ ℤ
328326, 327sstri 3979 . . . . . . . . . . . . 13 (0..^𝑏) ⊆ ℤ
329 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏))
330328, 329sseldi 3968 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ)
331 simplr 765 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁))
332119, 331sseldi 3968 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ)
333330, 332zsubcld 12084 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℤ)
3341ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℕ0)
335333zred 12079 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℝ)
336 0red 10636 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ)
33725ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ)
338 elfzolt2 13040 . . . . . . . . . . . . . 14 (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏)
339338adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏)
340330zred 12079 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ)
341332zred 12079 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ)
342340, 341sublt0d 11258 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) < 0 ↔ 𝑛 < 𝑏))
343339, 342mpbird 258 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 0)
34462ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇)
345335, 336, 337, 343, 344ltletrd 10792 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 𝑇)
346325, 333, 334, 345reprlt 31776 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
347346sumeq1d 15050 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
348347, 312syl6eq 2876 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
349348oveq1d 7166 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
35073adantr 481 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
35160adantr 481 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ)
352340recnd 10661 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ)
353341recnd 10661 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ)
354352, 353npcand 10993 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) = 𝑛)
355 fzo0ssnn0 13111 . . . . . . . . . . . 12 (0..^𝑏) ⊆ ℕ0
356355, 329sseldi 3968 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0)
357354, 356eqeltrd 2917 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
358351, 357expcld 13503 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
359350, 358mulcld 10653 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
360359mul02d 10830 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
361349, 360eqtrd 2860 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
362221, 14, 227, 276, 324, 361fsum2dsub 31764 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
363 nn0sscn 11894 . . . . . . . . 9 0 ⊆ ℂ
364363, 1sseldi 3968 . . . . . . . 8 (𝜑𝑇 ∈ ℂ)
365363, 14sseldi 3968 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
366364, 365adddirp1d 10659 . . . . . . 7 (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁))
367366oveq2d 7167 . . . . . 6 (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁)))
368130, 363sstri 3979 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℂ
369 simplr 765 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁)))
370368, 369sseldi 3968 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
37144, 363sstri 3979 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℂ
372 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
373371, 372sseldi 3968 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
374370, 373npcand 10993 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛𝑏) + 𝑏) = 𝑛)
375374eqcomd 2831 . . . . . . . . . 10 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛𝑏) + 𝑏))
376375oveq2d 7167 . . . . . . . . 9 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑛) = (𝑍↑((𝑛𝑏) + 𝑏)))
377376oveq2d 7167 . . . . . . . 8 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
378377oveq2d 7167 . . . . . . 7 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
379378sumeq2dv 15052 . . . . . 6 ((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
380367, 379sumeq12dv 15055 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
381362, 380eqtr4d 2863 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
382107adantlr 711 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
383110adantlr 711 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
38476adantlr 711 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
385384adantr 481 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
386382, 383, 385mulassd 10656 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))))
38773ad4ant13 747 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
38875ad4ant13 747 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑏) ∈ ℂ)
389383, 387, 388mulassd 10656 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
390387, 383, 388mulassd 10656 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
391383, 387mulcomd 10654 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
392391oveq1d 7166 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)))
393108adantlr 711 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
39474ad4ant13 747 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0)
395109adantlr 711 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
396393, 394, 395expaddd 13505 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍𝑚) · (𝑍𝑏)))
397396oveq2d 7167 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
398390, 392, 3973eqtr4d 2870 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
399389, 398eqtr3d 2862 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
400399oveq2d 7167 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
401386, 400eqtrd 2860 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
402401sumeq2dv 15052 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
40389adantr 481 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
404111adantlr 711 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
405403, 384, 404fsummulc1 15132 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
40673adantlr 711 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
40760adantlr 711 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
40885adantr 481 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0)
40974adantlr 711 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
410408, 409nn0addcld 11951 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
411407, 410expcld 13503 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
412406, 411mulcld 10653 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
413403, 412, 382fsummulc1 15132 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
414402, 405, 4133eqtr4rd 2871 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
415414sumeq2dv 15052 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
416415sumeq2dv 15052 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
417220, 381, 4163eqtr2rd 2867 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
41880, 113, 4173eqtr2d 2866 . 2 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
4196, 78, 4183eqtrd 2864 1 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1081   = wceq 1530  wcel 2107  cun 3937  wss 3939  c0 4294  {csn 4563   class class class wbr 5062  wf 6347  cfv 6351  (class class class)co 7151  m cmap 8399  Fincfn 8501  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667  cle 10668  cmin 10862  -cneg 10863  cn 11630  0cn0 11889  cz 11973  cuz 12235  ...cfz 12885  ..^cfzo 13026  cexp 13422  Σcsu 15035  cprod 15251  reprcrepr 31765
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-disj 5028  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-sup 8898  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-n0 11890  df-z 11974  df-uz 12236  df-rp 12383  df-ico 12737  df-fz 12886  df-fzo 13027  df-seq 13363  df-exp 13423  df-hash 13684  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-clim 14838  df-sum 15036  df-prod 15252  df-repr 31766
This theorem is referenced by:  breprexp  31790
  Copyright terms: Public domain W3C validator