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

Theorem breprexplemc 30838
 Description: Lemma for breprexp 30839 (induction step) (Contributed by Thierry Arnoux, 6-Dec-2021.)
Hypotheses
Ref Expression
breprexp.n (𝜑𝑁 ∈ ℕ0)
breprexp.s (𝜑𝑆 ∈ ℕ0)
breprexp.z (𝜑𝑍 ∈ ℂ)
breprexp.h (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
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 11760 . . . . 5 0 = (ℤ‘0)
31, 2syl6eleq 2740 . . . 4 (𝜑𝑇 ∈ (ℤ‘0))
4 fzosplitsn 12616 . . . 4 (𝑇 ∈ (ℤ‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
53, 4syl 17 . . 3 (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
65prodeq1d 14695 . 2 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
7 nfv 1883 . . 3 𝑎𝜑
8 nfcv 2793 . . 3 𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))
9 fzofi 12813 . . . 4 (0..^𝑇) ∈ Fin
109a1i 11 . . 3 (𝜑 → (0..^𝑇) ∈ Fin)
11 fzonel 12522 . . . 4 ¬ 𝑇 ∈ (0..^𝑇)
1211a1i 11 . . 3 (𝜑 → ¬ 𝑇 ∈ (0..^𝑇))
13 fzfid 12812 . . . 4 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin)
14 breprexp.n . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
1514ad2antrr 762 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
16 breprexp.s . . . . . . 7 (𝜑𝑆 ∈ ℕ0)
1716ad2antrr 762 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
18 breprexp.z . . . . . . 7 (𝜑𝑍 ∈ ℂ)
1918ad2antrr 762 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
20 breprexp.h . . . . . . . 8 (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
2120adantr 480 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
2221adantr 480 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
231nn0zd 11518 . . . . . . . . . 10 (𝜑𝑇 ∈ ℤ)
2416nn0zd 11518 . . . . . . . . . 10 (𝜑𝑆 ∈ ℤ)
251nn0red 11390 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
26 1red 10093 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
2725, 26readdcld 10107 . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ∈ ℝ)
2816nn0red 11390 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
2925lep1d 10993 . . . . . . . . . . 11 (𝜑𝑇 ≤ (𝑇 + 1))
30 breprexplemc.s . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ≤ 𝑆)
3125, 27, 28, 29, 30letrd 10232 . . . . . . . . . 10 (𝜑𝑇𝑆)
32 eluz1 11729 . . . . . . . . . . 11 (𝑇 ∈ ℤ → (𝑆 ∈ (ℤ𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇𝑆)))
3332biimpar 501 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇𝑆)) → 𝑆 ∈ (ℤ𝑇))
3423, 24, 31, 33syl12anc 1364 . . . . . . . . 9 (𝜑𝑆 ∈ (ℤ𝑇))
35 fzoss2 12535 . . . . . . . . 9 (𝑆 ∈ (ℤ𝑇) → (0..^𝑇) ⊆ (0..^𝑆))
3634, 35syl 17 . . . . . . . 8 (𝜑 → (0..^𝑇) ⊆ (0..^𝑆))
3736sselda 3636 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
3837adantr 480 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆))
39 fz1ssnn 12410 . . . . . . . 8 (1...𝑁) ⊆ ℕ
4039a1i 11 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
4140sselda 3636 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
4215, 17, 19, 22, 38, 41breprexplemb 30837 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) ∈ ℂ)
43 nnssnn0 11333 . . . . . . . . . . 11 ℕ ⊆ ℕ0
4439, 43sstri 3645 . . . . . . . . . 10 (1...𝑁) ⊆ ℕ0
4544a1i 11 . . . . . . . . 9 (𝜑 → (1...𝑁) ⊆ ℕ0)
4645ralrimivw 2996 . . . . . . . 8 (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆ ℕ0)
4746r19.21bi 2961 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ0)
4847sselda 3636 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
4919, 48expcld 13048 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
5042, 49mulcld 10098 . . . 4 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
5113, 50fsumcl 14508 . . 3 ((𝜑𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
52 simpl 472 . . . . . . 7 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇)
5352fveq2d 6233 . . . . . 6 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (𝐿𝑎) = (𝐿𝑇))
5453fveq1d 6231 . . . . 5 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) = ((𝐿𝑇)‘𝑏))
5554oveq1d 6705 . . . 4 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
5655sumeq2dv 14477 . . 3 (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
57 fzfid 12812 . . . 4 (𝜑 → (1...𝑁) ∈ Fin)
5814adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
5916adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
6018adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
6120adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
621nn0ge0d 11392 . . . . . . . 8 (𝜑 → 0 ≤ 𝑇)
63 zltp1le 11465 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6423, 24, 63syl2anc 694 . . . . . . . . 9 (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6530, 64mpbird 247 . . . . . . . 8 (𝜑𝑇 < 𝑆)
66 0zd 11427 . . . . . . . . 9 (𝜑 → 0 ∈ ℤ)
67 elfzo 12511 . . . . . . . . 9 ((𝑇 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6823, 66, 24, 67syl3anc 1366 . . . . . . . 8 (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6962, 65, 68mpbir2and 977 . . . . . . 7 (𝜑𝑇 ∈ (0..^𝑆))
7069adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
7139a1i 11 . . . . . . 7 (𝜑 → (1...𝑁) ⊆ ℕ)
7271sselda 3636 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
7358, 59, 60, 61, 70, 72breprexplemb 30837 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
7445sselda 3636 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
7560, 74expcld 13048 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
7673, 75mulcld 10098 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
7757, 76fsumcl 14508 . . 3 (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
787, 8, 10, 1, 12, 51, 56, 77fprodsplitsn 14764 . 2 (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
79 breprexplemc.1 . . . 4 (𝜑 → ∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
8079oveq1d 6705 . . 3 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
81 fzfid 12812 . . . 4 (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin)
8239a1i 11 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ)
83 fz0ssnn0 12473 . . . . . . . 8 (0...(𝑇 · 𝑁)) ⊆ ℕ0
84 simpr 476 . . . . . . . 8 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁)))
8583, 84sseldi 3634 . . . . . . 7 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0)
8685nn0zd 11518 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ)
871adantr 480 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈ ℕ0)
8857adantr 480 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin)
8982, 86, 87, 88reprfi 30822 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
909a1i 11 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
9114adantr 480 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈ ℕ0)
9291ad2antrr 762 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
9316ad3antrrr 766 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
9418ad3antrrr 766 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
9520ad3antrrr 766 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
9636ad2antrr 762 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
9796sselda 3636 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
9839a1i 11 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
9986ad2antrr 762 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ)
10087ad2antrr 762 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
101 simplr 807 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
10298, 99, 100, 101reprf 30818 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
103 simpr 476 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
104102, 103ffvelrnd 6400 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
10539, 104sseldi 3634 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
10692, 93, 94, 95, 97, 105breprexplemb 30837 . . . . . . 7 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10790, 106fprodcl 14726 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10818ad2antrr 762 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
10985adantr 480 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
110108, 109expcld 13048 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
111107, 110mulcld 10098 . . . . 5 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11289, 111fsumcl 14508 . . . 4 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11381, 57, 112, 76fsum2mul 14565 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
11439a1i 11 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
115 fzssz 12381 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℤ
116 simpr 476 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁)))
117115, 116sseldi 3634 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ)
118117adantr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
119 fzssz 12381 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℤ
120 simpr 476 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
121119, 120sseldi 3634 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
122118, 121zsubcld 11525 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚𝑏) ∈ ℤ)
1231adantr 480 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈ ℕ0)
124123adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
12557adantr 480 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin)
126125adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
127114, 122, 124, 126reprfi 30822 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚𝑏)) ∈ Fin)
12873adantlr 751 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
12918adantr 480 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ)
130 fz0ssnn0 12473 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℕ0
131130, 116sseldi 3634 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0)
132129, 131expcld 13048 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍𝑚) ∈ ℂ)
133132adantr 480 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑚) ∈ ℂ)
134128, 133mulcld 10098 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑚)) ∈ ℂ)
1359a1i 11 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (0..^𝑇) ∈ Fin)
13614adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈ ℕ0)
137136adantr 480 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
138137ad2antrr 762 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
13916ad4antr 769 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
140129ad3antrrr 766 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
14120ad4antr 769 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
14237ad5ant15 1336 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
14339a1i 11 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
144122ad2antrr 762 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚𝑏) ∈ ℤ)
145124ad2antrr 762 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
146 simplr 807 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
147143, 144, 145, 146reprf 30818 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
148 simpr 476 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
149147, 148ffvelrnd 6400 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
15039, 149sseldi 3634 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
151138, 139, 140, 141, 142, 150breprexplemb 30837 . . . . . . . . . 10 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
152135, 151fprodcl 14726 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
153127, 134, 152fsummulc1 14561 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
154153sumeq2dv 14477 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
155 elfzle2 12383 . . . . . . . . . . 11 (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
156155adantl 481 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
157136ad2antrr 762 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ0)
15816ad3antrrr 766 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈ ℕ0)
159129ad2antrr 762 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ)
16020ad3antrrr 766 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
16123peano2zd 11523 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 + 1) ∈ ℤ)
162 eluz 11739 . . . . . . . . . . . . . . . 16 (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈ (ℤ‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆))
163162biimpar 501 . . . . . . . . . . . . . . 15 ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ‘(𝑇 + 1)))
164161, 24, 30, 163syl21anc 1365 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ (ℤ‘(𝑇 + 1)))
165 fzoss2 12535 . . . . . . . . . . . . . 14 (𝑆 ∈ (ℤ‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
166164, 165syl 17 . . . . . . . . . . . . 13 (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
167166ad3antrrr 766 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
168 simplr 807 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1)))
169167, 168sseldd 3637 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆))
170 simpr 476 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
171157, 158, 159, 160, 169, 170breprexplemb 30837 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿𝑥)‘𝑦) ∈ ℂ)
172136, 123, 131, 156, 171breprexplema 30836 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)))
173172oveq1d 6705 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
174128adantr 480 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
175152, 174mulcld 10098 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
176127, 175fsumcl 14508 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
177125, 132, 176fsummulc1 14561 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
178127, 133, 175fsummulc1 14561 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
179133adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (𝑍𝑚) ∈ ℂ)
180152, 174, 179mulassd 10101 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
181180sumeq2dv 14477 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
182178, 181eqtrd 2685 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
183182sumeq2dv 14477 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
184173, 177, 1833eqtrd 2689 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
18539a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ)
186 1nn0 11346 . . . . . . . . . . 11 1 ∈ ℕ0
187186a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈ ℕ0)
188123, 187nn0addcld 11393 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈ ℕ0)
189185, 117, 188, 125reprfi 30822 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin)
190 fzofi 12813 . . . . . . . . . 10 (0..^(𝑇 + 1)) ∈ Fin
191190a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin)
192136ad2antrr 762 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈ ℕ0)
19316ad3antrrr 766 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈ ℕ0)
194129ad2antrr 762 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ)
19520ad3antrrr 766 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
196166ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
197196sselda 3636 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆))
19839a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ)
199117ad2antrr 762 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ)
200188ad2antrr 762 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈ ℕ0)
201 simplr 807 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚))
202198, 199, 200, 201reprf 30818 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁))
203 simpr 476 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1)))
204202, 203ffvelrnd 6400 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ (1...𝑁))
20539, 204sseldi 3634 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ ℕ)
206192, 193, 194, 195, 197, 205breprexplemb 30837 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
207191, 206fprodcl 14726 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
208189, 132, 207fsummulc1 14561 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
209154, 184, 2083eqtr2rd 2692 . . . . . 6 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
210209sumeq2dv 14477 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
211 oveq1 6697 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑛𝑏) = (𝑚𝑏))
212211oveq2d 6706 . . . . . . . . . 10 (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
213212sumeq1d 14475 . . . . . . . . 9 (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
214 oveq2 6698 . . . . . . . . . 10 (𝑛 = 𝑚 → (𝑍𝑛) = (𝑍𝑚))
215214oveq2d 6706 . . . . . . . . 9 (𝑛 = 𝑚 → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
216213, 215oveq12d 6708 . . . . . . . 8 (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
217216adantr 480 . . . . . . 7 ((𝑛 = 𝑚𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
218217sumeq2dv 14477 . . . . . 6 (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
219218cbvsumv 14470 . . . . 5 Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
220210, 219syl6eqr 2703 . . . 4 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
2211, 14nn0mulcld 11394 . . . . . 6 (𝜑 → (𝑇 · 𝑁) ∈ ℕ0)
222 oveq2 6698 . . . . . . . 8 (𝑚 = (𝑛𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛𝑏)))
223222sumeq1d 14475 . . . . . . 7 (𝑚 = (𝑛𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
224 oveq1 6697 . . . . . . . . 9 (𝑚 = (𝑛𝑏) → (𝑚 + 𝑏) = ((𝑛𝑏) + 𝑏))
225224oveq2d 6706 . . . . . . . 8 (𝑚 = (𝑛𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛𝑏) + 𝑏)))
226225oveq2d 6706 . . . . . . 7 (𝑚 = (𝑛𝑏) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
227223, 226oveq12d 6708 . . . . . 6 (𝑚 = (𝑛𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
22839a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
229 uzssz 11745 . . . . . . . . . 10 (ℤ‘-𝑏) ⊆ ℤ
230 simp2 1082 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ‘-𝑏))
231229, 230sseldi 3634 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
23213ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
233573ad2ant1 1102 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
234228, 231, 232, 233reprfi 30822 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
2359a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
236583adant2 1100 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
237236ad2antrr 762 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
238593adant2 1100 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
239238ad2antrr 762 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
240603adant2 1100 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
241240ad2antrr 762 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
242613adant2 1100 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
243242ad2antrr 762 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
244363ad2ant1 1102 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆))
245244adantr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
246245sselda 3636 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
24739a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ)
248231adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ)
249232adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈ ℕ0)
250 simpr 476 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
251247, 248, 249, 250reprf 30818 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
252251adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
253 simpr 476 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
254252, 253ffvelrnd 6400 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
25539, 254sseldi 3634 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
256237, 239, 241, 243, 246, 255breprexplemb 30837 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
257235, 256fprodcl 14726 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
258234, 257fsumcl 14508 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
259703adant2 1100 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
260723adant2 1100 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
261236, 238, 240, 242, 259, 260breprexplemb 30837 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
262231zcnd 11521 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ)
263 simp3 1083 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
264119, 263sseldi 3634 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
265264zcnd 11521 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
266262, 265subnegd 10437 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏))
267264znegcld 11522 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ)
268 eluzle 11738 . . . . . . . . . . . 12 (𝑚 ∈ (ℤ‘-𝑏) → -𝑏𝑚)
269230, 268syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏𝑚)
270 znn0sub 11462 . . . . . . . . . . . 12 ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏𝑚 ↔ (𝑚 − -𝑏) ∈ ℕ0))
271270biimpa 500 . . . . . . . . . . 11 (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏𝑚) → (𝑚 − -𝑏) ∈ ℕ0)
272267, 231, 269, 271syl21anc 1365 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈ ℕ0)
273266, 272eqeltrrd 2731 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
274240, 273expcld 13048 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
275261, 274mulcld 10098 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
276258, 275mulcld 10098 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ)
27758adantr 480 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℕ0)
278 ssid 3657 . . . . . . . . . . . 12 (1...𝑁) ⊆ (1...𝑁)
279278a1i 11 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁))
280 fzssz 12381 . . . . . . . . . . . . 13 ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℤ
281 simpr 476 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)))
282280, 281sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ)
283 simplr 807 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁))
284119, 283sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ)
285282, 284zsubcld 11525 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛𝑏) ∈ ℤ)
2861ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℕ0)
28725ad2antrr 762 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ)
288277nn0red 11390 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ)
289287, 288remulcld 10108 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ)
290284zred 11520 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ)
291221adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈ ℕ0)
292291, 74nn0addcld 11393 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈ ℕ0)
293186a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → 1 ∈ ℕ0)
294292, 293nn0addcld 11393 . . . . . . . . . . . . . . 15 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0)
295 fz2ssnn0 29675 . . . . . . . . . . . . . . 15 ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
296294, 295syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
297296sselda 3636 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0)
298297nn0red 11390 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ)
29923ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ)
300277nn0zd 11518 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ)
301299, 300zmulcld 11526 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ)
302301, 284zaddcld 11524 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ)
303 elfzle1 12382 . . . . . . . . . . . . . 14 (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
304281, 303syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
305 zltp1le 11465 . . . . . . . . . . . . . 14 ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛))
306305biimpar 501 . . . . . . . . . . . . 13 (((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
307302, 282, 304, 306syl21anc 1365 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
308 ltaddsub 10540 . . . . . . . . . . . . 13 (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛𝑏)))
309308biimpa 500 . . . . . . . . . . . 12 ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛𝑏))
310289, 290, 298, 307, 309syl31anc 1369 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛𝑏))
311277, 279, 285, 286, 310reprgt 30827 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
312311sumeq1d 14475 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
313 sum0 14496 . . . . . . . . 9 Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0
314312, 313syl6eq 2701 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
315314oveq1d 6705 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
31673adantr 480 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
31760adantr 480 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ)
318282zcnd 11521 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ)
319284zcnd 11521 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ)
320318, 319npcand 10434 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) = 𝑛)
321320, 297eqeltrd 2730 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
322317, 321expcld 13048 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
323316, 322mulcld 10098 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
324323mul02d 10272 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
325315, 324eqtrd 2685 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
32639a1i 11 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ)
327 fzossfz 12527 . . . . . . . . . . . . . 14 (0..^𝑏) ⊆ (0...𝑏)
328 fzssz 12381 . . . . . . . . . . . . . 14 (0...𝑏) ⊆ ℤ
329327, 328sstri 3645 . . . . . . . . . . . . 13 (0..^𝑏) ⊆ ℤ
330 simpr 476 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏))
331329, 330sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ)
332 simplr 807 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁))
333119, 332sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ)
334331, 333zsubcld 11525 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℤ)
3351ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℕ0)
336334zred 11520 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℝ)
337 0red 10079 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ)
33825ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ)
339 elfzolt2 12518 . . . . . . . . . . . . . 14 (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏)
340339adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏)
341331zred 11520 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ)
342333zred 11520 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ)
343341, 342sublt0d 10691 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) < 0 ↔ 𝑛 < 𝑏))
344340, 343mpbird 247 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 0)
34562ad2antrr 762 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇)
346336, 337, 338, 344, 345ltletrd 10235 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 𝑇)
347326, 334, 335, 346reprlt 30825 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
348347sumeq1d 14475 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
349348, 313syl6eq 2701 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
350349oveq1d 6705 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
35173adantr 480 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
35260adantr 480 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ)
353341recnd 10106 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ)
354342recnd 10106 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ)
355353, 354npcand 10434 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) = 𝑛)
356 fzo0ssnn0 12588 . . . . . . . . . . . 12 (0..^𝑏) ⊆ ℕ0
357356, 330sseldi 3634 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0)
358355, 357eqeltrd 2730 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
359352, 358expcld 13048 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
360351, 359mulcld 10098 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
361360mul02d 10272 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
362350, 361eqtrd 2685 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
363221, 14, 227, 276, 325, 362fsum2dsub 30813 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
364 nn0sscn 11335 . . . . . . . . 9 0 ⊆ ℂ
365364, 1sseldi 3634 . . . . . . . 8 (𝜑𝑇 ∈ ℂ)
366364, 14sseldi 3634 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
367365, 366adddirp1d 10104 . . . . . . 7 (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁))
368367oveq2d 6706 . . . . . 6 (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁)))
369130, 364sstri 3645 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℂ
370 simplr 807 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁)))
371369, 370sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
37244, 364sstri 3645 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℂ
373 simpr 476 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
374372, 373sseldi 3634 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
375371, 374npcand 10434 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛𝑏) + 𝑏) = 𝑛)
376375eqcomd 2657 . . . . . . . . . 10 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛𝑏) + 𝑏))
377376oveq2d 6706 . . . . . . . . 9 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑛) = (𝑍↑((𝑛𝑏) + 𝑏)))
378377oveq2d 6706 . . . . . . . 8 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
379378oveq2d 6706 . . . . . . 7 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
380379sumeq2dv 14477 . . . . . 6 ((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
381368, 380sumeq12dv 14481 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
382363, 381eqtr4d 2688 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
383107adantlr 751 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
384110adantlr 751 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
38576adantlr 751 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
386385adantr 480 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
387383, 384, 386mulassd 10101 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))))
38873ad4ant13 1315 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
38975ad4ant13 1315 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑏) ∈ ℂ)
390384, 388, 389mulassd 10101 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
391388, 384, 389mulassd 10101 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
392384, 388mulcomd 10099 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
393392oveq1d 6705 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)))
394108adantlr 751 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
39574ad4ant13 1315 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0)
396109adantlr 751 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
397394, 395, 396expaddd 13050 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍𝑚) · (𝑍𝑏)))
398397oveq2d 6706 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
399391, 393, 3983eqtr4d 2695 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
400390, 399eqtr3d 2687 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
401400oveq2d 6706 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
402387, 401eqtrd 2685 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
403402sumeq2dv 14477 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
40489adantr 480 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
405111adantlr 751 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
406404, 385, 405fsummulc1 14561 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
40773adantlr 751 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
40860adantlr 751 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
40985adantr 480 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0)
41074adantlr 751 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
411409, 410nn0addcld 11393 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
412408, 411expcld 13048 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
413407, 412mulcld 10098 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
414404, 413, 383fsummulc1 14561 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
415403, 406, 4143eqtr4rd 2696 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
416415sumeq2dv 14477 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
417416sumeq2dv 14477 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
418220, 382, 4173eqtr2rd 2692 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
41980, 113, 4183eqtr2d 2691 . 2 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
4206, 78, 4193eqtrd 2689 1 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ∪ cun 3605   ⊆ wss 3607  ∅c0 3948  {csn 4210   class class class wbr 4685  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↑𝑚 cmap 7899  Fincfn 7997  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  ..^cfzo 12504  ↑cexp 12900  Σcsu 14460  ∏cprod 14679  reprcrepr 30814 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-prod 14680  df-repr 30815 This theorem is referenced by:  breprexp  30839
 Copyright terms: Public domain W3C validator