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 31045
Description: Lemma for breprexp 31046 (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 11947 . . . . 5 0 = (ℤ‘0)
31, 2syl6eleq 2906 . . . 4 (𝜑𝑇 ∈ (ℤ‘0))
4 fzosplitsn 12807 . . . 4 (𝑇 ∈ (ℤ‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
53, 4syl 17 . . 3 (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
65prodeq1d 14879 . 2 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
7 nfv 2005 . . 3 𝑎𝜑
8 nfcv 2959 . . 3 𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))
9 fzofi 13004 . . . 4 (0..^𝑇) ∈ Fin
109a1i 11 . . 3 (𝜑 → (0..^𝑇) ∈ Fin)
11 fzonel 12714 . . . 4 ¬ 𝑇 ∈ (0..^𝑇)
1211a1i 11 . . 3 (𝜑 → ¬ 𝑇 ∈ (0..^𝑇))
13 fzfid 13003 . . . 4 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin)
14 breprexp.n . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
1514ad2antrr 708 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
16 breprexp.s . . . . . . 7 (𝜑𝑆 ∈ ℕ0)
1716ad2antrr 708 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
18 breprexp.z . . . . . . 7 (𝜑𝑍 ∈ ℂ)
1918ad2antrr 708 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
20 breprexp.h . . . . . . . 8 (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
2120adantr 468 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
2221adantr 468 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
231nn0zd 11753 . . . . . . . . . 10 (𝜑𝑇 ∈ ℤ)
2416nn0zd 11753 . . . . . . . . . 10 (𝜑𝑆 ∈ ℤ)
251nn0red 11625 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℝ)
26 1red 10333 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
2725, 26readdcld 10361 . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ∈ ℝ)
2816nn0red 11625 . . . . . . . . . . 11 (𝜑𝑆 ∈ ℝ)
2925lep1d 11247 . . . . . . . . . . 11 (𝜑𝑇 ≤ (𝑇 + 1))
30 breprexplemc.s . . . . . . . . . . 11 (𝜑 → (𝑇 + 1) ≤ 𝑆)
3125, 27, 28, 29, 30letrd 10486 . . . . . . . . . 10 (𝜑𝑇𝑆)
32 eluz1 11915 . . . . . . . . . . 11 (𝑇 ∈ ℤ → (𝑆 ∈ (ℤ𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇𝑆)))
3332biimpar 465 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇𝑆)) → 𝑆 ∈ (ℤ𝑇))
3423, 24, 31, 33syl12anc 856 . . . . . . . . 9 (𝜑𝑆 ∈ (ℤ𝑇))
35 fzoss2 12727 . . . . . . . . 9 (𝑆 ∈ (ℤ𝑇) → (0..^𝑇) ⊆ (0..^𝑆))
3634, 35syl 17 . . . . . . . 8 (𝜑 → (0..^𝑇) ⊆ (0..^𝑆))
3736sselda 3809 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
3837adantr 468 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆))
39 fz1ssnn 12602 . . . . . . . 8 (1...𝑁) ⊆ ℕ
4039a1i 11 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
4140sselda 3809 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
4215, 17, 19, 22, 38, 41breprexplemb 31044 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) ∈ ℂ)
43 nnssnn0 11569 . . . . . . . . . . 11 ℕ ⊆ ℕ0
4439, 43sstri 3818 . . . . . . . . . 10 (1...𝑁) ⊆ ℕ0
4544a1i 11 . . . . . . . . 9 (𝜑 → (1...𝑁) ⊆ ℕ0)
4645ralrimivw 3166 . . . . . . . 8 (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆ ℕ0)
4746r19.21bi 3131 . . . . . . 7 ((𝜑𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ0)
4847sselda 3809 . . . . . 6 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
4919, 48expcld 13238 . . . . 5 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
5042, 49mulcld 10352 . . . 4 (((𝜑𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
5113, 50fsumcl 14694 . . 3 ((𝜑𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
52 simpl 470 . . . . . . 7 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇)
5352fveq2d 6419 . . . . . 6 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (𝐿𝑎) = (𝐿𝑇))
5453fveq1d 6417 . . . . 5 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) = ((𝐿𝑇)‘𝑏))
5554oveq1d 6896 . . . 4 ((𝑎 = 𝑇𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
5655sumeq2dv 14663 . . 3 (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)))
57 fzfid 13003 . . . 4 (𝜑 → (1...𝑁) ∈ Fin)
5814adantr 468 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
5916adantr 468 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
6018adantr 468 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
6120adantr 468 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
621nn0ge0d 11627 . . . . . . . 8 (𝜑 → 0 ≤ 𝑇)
63 zltp1le 11700 . . . . . . . . . 10 ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6423, 24, 63syl2anc 575 . . . . . . . . 9 (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
6530, 64mpbird 248 . . . . . . . 8 (𝜑𝑇 < 𝑆)
66 0zd 11662 . . . . . . . . 9 (𝜑 → 0 ∈ ℤ)
67 elfzo 12703 . . . . . . . . 9 ((𝑇 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6823, 66, 24, 67syl3anc 1483 . . . . . . . 8 (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇𝑇 < 𝑆)))
6962, 65, 68mpbir2and 695 . . . . . . 7 (𝜑𝑇 ∈ (0..^𝑆))
7069adantr 468 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
7139a1i 11 . . . . . . 7 (𝜑 → (1...𝑁) ⊆ ℕ)
7271sselda 3809 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
7358, 59, 60, 61, 70, 72breprexplemb 31044 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
7445sselda 3809 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
7560, 74expcld 13238 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑍𝑏) ∈ ℂ)
7673, 75mulcld 10352 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
7757, 76fsumcl 14694 . . 3 (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
787, 8, 10, 1, 12, 51, 56, 77fprodsplitsn 14947 . 2 (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
79 breprexplemc.1 . . . 4 (𝜑 → ∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
8079oveq1d 6896 . . 3 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
81 fzfid 13003 . . . 4 (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin)
8239a1i 11 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ)
83 fz0ssnn0 12665 . . . . . . . 8 (0...(𝑇 · 𝑁)) ⊆ ℕ0
84 simpr 473 . . . . . . . 8 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁)))
8583, 84sseldi 3807 . . . . . . 7 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0)
8685nn0zd 11753 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ)
871adantr 468 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈ ℕ0)
8857adantr 468 . . . . . 6 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin)
8982, 86, 87, 88reprfi 31029 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
909a1i 11 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
9114adantr 468 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈ ℕ0)
9291ad2antrr 708 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
9316ad3antrrr 712 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
9418ad3antrrr 712 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
9520ad3antrrr 712 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
9636ad2antrr 708 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
9796sselda 3809 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
9839a1i 11 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
9986ad2antrr 708 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ)
10087ad2antrr 708 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
101 simplr 776 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
10298, 99, 100, 101reprf 31025 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
103 simpr 473 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
104102, 103ffvelrnd 6589 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
10539, 104sseldi 3807 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
10692, 93, 94, 95, 97, 105breprexplemb 31044 . . . . . . 7 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10790, 106fprodcl 14910 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
10818ad2antrr 708 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
10985adantr 468 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
110108, 109expcld 13238 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
111107, 110mulcld 10352 . . . . 5 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11289, 111fsumcl 14694 . . . 4 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
11381, 57, 112, 76fsum2mul 14750 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
11439a1i 11 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
115 fzssz 12573 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℤ
116 simpr 473 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁)))
117115, 116sseldi 3807 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ)
118117adantr 468 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
119 fzssz 12573 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℤ
120 simpr 473 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
121119, 120sseldi 3807 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
122118, 121zsubcld 11760 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚𝑏) ∈ ℤ)
1231adantr 468 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈ ℕ0)
124123adantr 468 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
12557adantr 468 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin)
126125adantr 468 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
127114, 122, 124, 126reprfi 31029 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚𝑏)) ∈ Fin)
12873adantlr 697 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
12918adantr 468 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ)
130 fz0ssnn0 12665 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℕ0
131130, 116sseldi 3807 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0)
132129, 131expcld 13238 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍𝑚) ∈ ℂ)
133132adantr 468 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑚) ∈ ℂ)
134128, 133mulcld 10352 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑚)) ∈ ℂ)
1359a1i 11 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (0..^𝑇) ∈ Fin)
13614adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈ ℕ0)
137136adantr 468 . . . . . . . . . . . 12 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
138137ad2antrr 708 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
13916ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
140129ad3antrrr 712 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
14120ad4antr 715 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
14237ad5ant15 762 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
14339a1i 11 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
144122ad2antrr 708 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚𝑏) ∈ ℤ)
145124ad2antrr 708 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
146 simplr 776 . . . . . . . . . . . . . 14 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
147143, 144, 145, 146reprf 31025 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
148 simpr 473 . . . . . . . . . . . . 13 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
149147, 148ffvelrnd 6589 . . . . . . . . . . . 12 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
15039, 149sseldi 3807 . . . . . . . . . . 11 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
151138, 139, 140, 141, 142, 150breprexplemb 31044 . . . . . . . . . 10 (((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
152135, 151fprodcl 14910 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
153127, 134, 152fsummulc1 14746 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
154153sumeq2dv 14663 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
155 elfzle2 12575 . . . . . . . . . . 11 (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
156155adantl 469 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
157136ad2antrr 708 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ0)
15816ad3antrrr 712 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈ ℕ0)
159129ad2antrr 708 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ)
16020ad3antrrr 712 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
16123peano2zd 11758 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇 + 1) ∈ ℤ)
162 eluz 11925 . . . . . . . . . . . . . . . 16 (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈ (ℤ‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆))
163162biimpar 465 . . . . . . . . . . . . . . 15 ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ‘(𝑇 + 1)))
164161, 24, 30, 163syl21anc 857 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ (ℤ‘(𝑇 + 1)))
165 fzoss2 12727 . . . . . . . . . . . . . 14 (𝑆 ∈ (ℤ‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
166164, 165syl 17 . . . . . . . . . . . . 13 (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
167166ad3antrrr 712 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
168 simplr 776 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1)))
169167, 168sseldd 3810 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆))
170 simpr 473 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
171157, 158, 159, 160, 169, 170breprexplemb 31044 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿𝑥)‘𝑦) ∈ ℂ)
172136, 123, 131, 156, 171breprexplema 31043 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)))
173172oveq1d 6896 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
174128adantr 468 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
175152, 174mulcld 10352 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
176127, 175fsumcl 14694 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) ∈ ℂ)
177125, 132, 176fsummulc1 14746 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
178127, 133, 175fsummulc1 14746 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)))
179133adantr 468 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → (𝑍𝑚) ∈ ℂ)
180152, 174, 179mulassd 10355 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
181180sumeq2dv 14663 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
182178, 181eqtrd 2851 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
183182sumeq2dv 14663 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
184173, 177, 1833eqtrd 2855 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
18539a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ)
186 1nn0 11582 . . . . . . . . . . 11 1 ∈ ℕ0
187186a1i 11 . . . . . . . . . 10 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈ ℕ0)
188123, 187nn0addcld 11628 . . . . . . . . 9 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈ ℕ0)
189185, 117, 188, 125reprfi 31029 . . . . . . . 8 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin)
190 fzofi 13004 . . . . . . . . . 10 (0..^(𝑇 + 1)) ∈ Fin
191190a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin)
192136ad2antrr 708 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈ ℕ0)
19316ad3antrrr 712 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈ ℕ0)
194129ad2antrr 708 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ)
19520ad3antrrr 712 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
196166ad2antrr 708 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
197196sselda 3809 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆))
19839a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ)
199117ad2antrr 708 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ)
200188ad2antrr 708 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈ ℕ0)
201 simplr 776 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚))
202198, 199, 200, 201reprf 31025 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁))
203 simpr 473 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1)))
204202, 203ffvelrnd 6589 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ (1...𝑁))
20539, 204sseldi 3807 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑𝑎) ∈ ℕ)
206192, 193, 194, 195, 197, 205breprexplemb 31044 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
207191, 206fprodcl 14910 . . . . . . . 8 (((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
208189, 132, 207fsummulc1 14746 . . . . . . 7 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
209154, 184, 2083eqtr2rd 2858 . . . . . 6 ((𝜑𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
210209sumeq2dv 14663 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
211 oveq1 6888 . . . . . . . . . . 11 (𝑛 = 𝑚 → (𝑛𝑏) = (𝑚𝑏))
212211oveq2d 6897 . . . . . . . . . 10 (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚𝑏)))
213212sumeq1d 14661 . . . . . . . . 9 (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
214 oveq2 6889 . . . . . . . . . 10 (𝑛 = 𝑚 → (𝑍𝑛) = (𝑍𝑚))
215214oveq2d 6897 . . . . . . . . 9 (𝑛 = 𝑚 → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
216213, 215oveq12d 6899 . . . . . . . 8 (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
217216adantr 468 . . . . . . 7 ((𝑛 = 𝑚𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
218217sumeq2dv 14663 . . . . . 6 (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚))))
219218cbvsumv 14656 . . . . 5 Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
220210, 219syl6eqr 2869 . . . 4 (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
2211, 14nn0mulcld 11629 . . . . . 6 (𝜑 → (𝑇 · 𝑁) ∈ ℕ0)
222 oveq2 6889 . . . . . . . 8 (𝑚 = (𝑛𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛𝑏)))
223222sumeq1d 14661 . . . . . . 7 (𝑚 = (𝑛𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
224 oveq1 6888 . . . . . . . . 9 (𝑚 = (𝑛𝑏) → (𝑚 + 𝑏) = ((𝑛𝑏) + 𝑏))
225224oveq2d 6897 . . . . . . . 8 (𝑚 = (𝑛𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛𝑏) + 𝑏)))
226225oveq2d 6897 . . . . . . 7 (𝑚 = (𝑛𝑏) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
227223, 226oveq12d 6899 . . . . . 6 (𝑚 = (𝑛𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
22839a1i 11 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
229 uzssz 11931 . . . . . . . . . 10 (ℤ‘-𝑏) ⊆ ℤ
230 simp2 1160 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ‘-𝑏))
231229, 230sseldi 3807 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
23213ad2ant1 1156 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
233573ad2ant1 1156 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
234228, 231, 232, 233reprfi 31029 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
2359a1i 11 . . . . . . . . 9 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
236583adant2 1154 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
237236ad2antrr 708 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
238593adant2 1154 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
239238ad2antrr 708 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
240603adant2 1154 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
241240ad2antrr 708 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
242613adant2 1154 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
243242ad2antrr 708 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
244363ad2ant1 1156 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆))
245244adantr 468 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
246245sselda 3809 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
24739a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ)
248231adantr 468 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ)
249232adantr 468 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈ ℕ0)
250 simpr 473 . . . . . . . . . . . . . 14 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
251247, 248, 249, 250reprf 31025 . . . . . . . . . . . . 13 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
252251adantr 468 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
253 simpr 473 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
254252, 253ffvelrnd 6589 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ (1...𝑁))
25539, 254sseldi 3807 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑𝑎) ∈ ℕ)
256237, 239, 241, 243, 246, 255breprexplemb 31044 . . . . . . . . 9 ((((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
257235, 256fprodcl 14910 . . . . . . . 8 (((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
258234, 257fsumcl 14694 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
259703adant2 1154 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
260723adant2 1154 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
261236, 238, 240, 242, 259, 260breprexplemb 31044 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
262231zcnd 11756 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ)
263 simp3 1161 . . . . . . . . . . . . 13 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
264119, 263sseldi 3807 . . . . . . . . . . . 12 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
265264zcnd 11756 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
266262, 265subnegd 10691 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏))
267264znegcld 11757 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ)
268 eluzle 11924 . . . . . . . . . . . 12 (𝑚 ∈ (ℤ‘-𝑏) → -𝑏𝑚)
269230, 268syl 17 . . . . . . . . . . 11 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏𝑚)
270 znn0sub 11697 . . . . . . . . . . . 12 ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏𝑚 ↔ (𝑚 − -𝑏) ∈ ℕ0))
271270biimpa 464 . . . . . . . . . . 11 (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏𝑚) → (𝑚 − -𝑏) ∈ ℕ0)
272267, 231, 269, 271syl21anc 857 . . . . . . . . . 10 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈ ℕ0)
273266, 272eqeltrrd 2897 . . . . . . . . 9 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
274240, 273expcld 13238 . . . . . . . 8 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
275261, 274mulcld 10352 . . . . . . 7 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
276258, 275mulcld 10352 . . . . . 6 ((𝜑𝑚 ∈ (ℤ‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ)
27758adantr 468 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℕ0)
278 ssidd 3832 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁))
279 fzssz 12573 . . . . . . . . . . . . 13 ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℤ
280 simpr 473 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)))
281279, 280sseldi 3807 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ)
282 simplr 776 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁))
283119, 282sseldi 3807 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ)
284281, 283zsubcld 11760 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛𝑏) ∈ ℤ)
2851ad2antrr 708 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℕ0)
28625ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ)
287277nn0red 11625 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ)
288286, 287remulcld 10362 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ)
289283zred 11755 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ)
290221adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈ ℕ0)
291290, 74nn0addcld 11628 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈ ℕ0)
292186a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑𝑏 ∈ (1...𝑁)) → 1 ∈ ℕ0)
293291, 292nn0addcld 11628 . . . . . . . . . . . . . . 15 ((𝜑𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0)
294 fz2ssnn0 29884 . . . . . . . . . . . . . . 15 ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
295293, 294syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
296295sselda 3809 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0)
297296nn0red 11625 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ)
29823ad2antrr 708 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ)
299277nn0zd 11753 . . . . . . . . . . . . . . 15 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ)
300298, 299zmulcld 11761 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ)
301300, 283zaddcld 11759 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ)
302 elfzle1 12574 . . . . . . . . . . . . . 14 (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
303280, 302syl 17 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
304 zltp1le 11700 . . . . . . . . . . . . . 14 ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛))
305304biimpar 465 . . . . . . . . . . . . 13 (((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
306301, 281, 303, 305syl21anc 857 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
307 ltaddsub 10794 . . . . . . . . . . . . 13 (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛𝑏)))
308307biimpa 464 . . . . . . . . . . . 12 ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛𝑏))
309288, 289, 297, 306, 308syl31anc 1485 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛𝑏))
310277, 278, 284, 285, 309reprgt 31034 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
311310sumeq1d 14661 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
312 sum0 14682 . . . . . . . . 9 Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0
313311, 312syl6eq 2867 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
314313oveq1d 6896 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
31573adantr 468 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
31660adantr 468 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ)
317281zcnd 11756 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ)
318283zcnd 11756 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ)
319317, 318npcand 10688 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) = 𝑛)
320319, 296eqeltrd 2896 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
321316, 320expcld 13238 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
322315, 321mulcld 10352 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
323322mul02d 10526 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
324314, 323eqtrd 2851 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
32539a1i 11 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ)
326 fzossfz 12719 . . . . . . . . . . . . . 14 (0..^𝑏) ⊆ (0...𝑏)
327 fzssz 12573 . . . . . . . . . . . . . 14 (0...𝑏) ⊆ ℤ
328326, 327sstri 3818 . . . . . . . . . . . . 13 (0..^𝑏) ⊆ ℤ
329 simpr 473 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏))
330328, 329sseldi 3807 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ)
331 simplr 776 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁))
332119, 331sseldi 3807 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ)
333330, 332zsubcld 11760 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℤ)
3341ad2antrr 708 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℕ0)
335333zred 11755 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) ∈ ℝ)
336 0red 10335 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ)
33725ad2antrr 708 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ)
338 elfzolt2 12710 . . . . . . . . . . . . . 14 (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏)
339338adantl 469 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏)
340330zred 11755 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ)
341332zred 11755 . . . . . . . . . . . . . 14 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ)
342340, 341sublt0d 10945 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) < 0 ↔ 𝑛 < 𝑏))
343339, 342mpbird 248 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 0)
34462ad2antrr 708 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇)
345335, 336, 337, 343, 344ltletrd 10489 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛𝑏) < 𝑇)
346325, 333, 334, 345reprlt 31032 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛𝑏)) = ∅)
347346sumeq1d 14661 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)))
348347, 312syl6eq 2867 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) = 0)
349348oveq1d 6896 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
35073adantr 468 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
35160adantr 468 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ)
352340recnd 10360 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ)
353341recnd 10360 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ)
354352, 353npcand 10688 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) = 𝑛)
355 fzo0ssnn0 12780 . . . . . . . . . . . 12 (0..^𝑏) ⊆ ℕ0
356355, 329sseldi 3807 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0)
357354, 356eqeltrd 2896 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛𝑏) + 𝑏) ∈ ℕ0)
358351, 357expcld 13238 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛𝑏) + 𝑏)) ∈ ℂ)
359350, 358mulcld 10352 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))) ∈ ℂ)
360359mul02d 10526 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
361349, 360eqtrd 2851 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))) = 0)
362221, 14, 227, 276, 324, 361fsum2dsub 31020 . . . . 5 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
363 nn0sscn 11571 . . . . . . . . 9 0 ⊆ ℂ
364363, 1sseldi 3807 . . . . . . . 8 (𝜑𝑇 ∈ ℂ)
365363, 14sseldi 3807 . . . . . . . 8 (𝜑𝑁 ∈ ℂ)
366364, 365adddirp1d 10358 . . . . . . 7 (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁))
367366oveq2d 6897 . . . . . 6 (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁)))
368130, 363sstri 3818 . . . . . . . . . . . . 13 (0...((𝑇 + 1) · 𝑁)) ⊆ ℂ
369 simplr 776 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁)))
370368, 369sseldi 3807 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
37144, 363sstri 3818 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℂ
372 simpr 473 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
373371, 372sseldi 3807 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
374370, 373npcand 10688 . . . . . . . . . . 11 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛𝑏) + 𝑏) = 𝑛)
375374eqcomd 2823 . . . . . . . . . 10 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛𝑏) + 𝑏))
376375oveq2d 6897 . . . . . . . . 9 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍𝑛) = (𝑍↑((𝑛𝑏) + 𝑏)))
377376oveq2d 6897 . . . . . . . 8 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑛)) = (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏))))
378377oveq2d 6897 . . . . . . 7 (((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
379378sumeq2dv 14663 . . . . . 6 ((𝜑𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
380367, 379sumeq12dv 14667 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑((𝑛𝑏) + 𝑏)))))
381362, 380eqtr4d 2854 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑛))))
382107adantlr 697 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
383110adantlr 697 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑚) ∈ ℂ)
38476adantlr 697 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
385384adantr 468 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍𝑏)) ∈ ℂ)
386382, 383, 385mulassd 10355 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))))
38773ad4ant13 748 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
38875ad4ant13 748 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍𝑏) ∈ ℂ)
389383, 387, 388mulassd 10355 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
390387, 383, 388mulassd 10355 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
391383, 387mulcomd 10353 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍𝑚)))
392391oveq1d 6896 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = ((((𝐿𝑇)‘𝑏) · (𝑍𝑚)) · (𝑍𝑏)))
393108adantlr 697 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
39474ad4ant13 748 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0)
395109adantlr 697 . . . . . . . . . . . . . 14 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
396393, 394, 395expaddd 13240 . . . . . . . . . . . . 13 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍𝑚) · (𝑍𝑏)))
397396oveq2d 6897 . . . . . . . . . . . 12 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿𝑇)‘𝑏) · ((𝑍𝑚) · (𝑍𝑏))))
398390, 392, 3973eqtr4d 2861 . . . . . . . . . . 11 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍𝑚) · ((𝐿𝑇)‘𝑏)) · (𝑍𝑏)) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
399389, 398eqtr3d 2853 . . . . . . . . . 10 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
400399oveq2d 6897 . . . . . . . . 9 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · ((𝑍𝑚) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
401386, 400eqtrd 2851 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
402401sumeq2dv 14663 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
40389adantr 468 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
404111adantlr 697 . . . . . . . 8 ((((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) ∈ ℂ)
405403, 384, 404fsummulc1 14746 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
40673adantlr 697 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿𝑇)‘𝑏) ∈ ℂ)
40760adantlr 697 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
40885adantr 468 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0)
40974adantlr 697 . . . . . . . . . . 11 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
410408, 409nn0addcld 11628 . . . . . . . . . 10 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
411407, 410expcld 13238 . . . . . . . . 9 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
412406, 411mulcld 10352 . . . . . . . 8 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
413403, 412, 382fsummulc1 14746 . . . . . . 7 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
414402, 405, 4133eqtr4rd 2862 . . . . . 6 (((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
415414sumeq2dv 14663 . . . . 5 ((𝜑𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
416415sumeq2dv 14663 . . . 4 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (((𝐿𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))))
417220, 381, 4163eqtr2rd 2858 . . 3 (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)) · (((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
41880, 113, 4173eqtr2d 2857 . 2 (𝜑 → (∏𝑎 ∈ (0..^𝑇𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿𝑇)‘𝑏) · (𝑍𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
4196, 78, 4183eqtrd 2855 1 (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿𝑎)‘(𝑑𝑎)) · (𝑍𝑚)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  cun 3778  wss 3780  c0 4127  {csn 4381   class class class wbr 4855  wf 6104  cfv 6108  (class class class)co 6881  𝑚 cmap 8099  Fincfn 8199  cc 10226  cr 10227  0cc0 10228  1c1 10229   + caddc 10231   · cmul 10233   < clt 10366  cle 10367  cmin 10558  -cneg 10559  cn 11312  0cn0 11566  cz 11650  cuz 11911  ...cfz 12556  ..^cfzo 12696  cexp 13090  Σcsu 14646  cprod 14863  reprcrepr 31021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4975  ax-sep 4986  ax-nul 4994  ax-pow 5046  ax-pr 5107  ax-un 7186  ax-inf2 8792  ax-cnex 10284  ax-resscn 10285  ax-1cn 10286  ax-icn 10287  ax-addcl 10288  ax-addrcl 10289  ax-mulcl 10290  ax-mulrcl 10291  ax-mulcom 10292  ax-addass 10293  ax-mulass 10294  ax-distr 10295  ax-i2m1 10296  ax-1ne0 10297  ax-1rid 10298  ax-rnegex 10299  ax-rrecex 10300  ax-cnre 10301  ax-pre-lttri 10302  ax-pre-lttrn 10303  ax-pre-ltadd 10304  ax-pre-mulgt0 10305  ax-pre-sup 10306
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-disj 4824  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5230  df-eprel 5235  df-po 5243  df-so 5244  df-fr 5281  df-se 5282  df-we 5283  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-pred 5904  df-ord 5950  df-on 5951  df-lim 5952  df-suc 5953  df-iota 6071  df-fun 6110  df-fn 6111  df-f 6112  df-f1 6113  df-fo 6114  df-f1o 6115  df-fv 6116  df-isom 6117  df-riota 6842  df-ov 6884  df-oprab 6885  df-mpt2 6886  df-om 7303  df-1st 7405  df-2nd 7406  df-wrecs 7649  df-recs 7711  df-rdg 7749  df-1o 7803  df-2o 7804  df-oadd 7807  df-er 7986  df-map 8101  df-pm 8102  df-en 8200  df-dom 8201  df-sdom 8202  df-fin 8203  df-sup 8594  df-oi 8661  df-card 9055  df-pnf 10368  df-mnf 10369  df-xr 10370  df-ltxr 10371  df-le 10372  df-sub 10560  df-neg 10561  df-div 10977  df-nn 11313  df-2 11371  df-3 11372  df-n0 11567  df-z 11651  df-uz 11912  df-rp 12054  df-ico 12406  df-fz 12557  df-fzo 12697  df-seq 13032  df-exp 13091  df-hash 13345  df-cj 14069  df-re 14070  df-im 14071  df-sqrt 14205  df-abs 14206  df-clim 14449  df-sum 14647  df-prod 14864  df-repr 31022
This theorem is referenced by:  breprexp  31046
  Copyright terms: Public domain W3C validator