Metamath Proof Explorer


Theorem breprexplemc

Description: Lemma for breprexp (induction step). (Contributed by Thierry Arnoux, 6-Dec-2021)

Ref Expression
Hypotheses breprexp.n ( 𝜑𝑁 ∈ ℕ0 )
breprexp.s ( 𝜑𝑆 ∈ ℕ0 )
breprexp.z ( 𝜑𝑍 ∈ ℂ )
breprexp.h ( 𝜑𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
breprexplemc.t ( 𝜑𝑇 ∈ ℕ0 )
breprexplemc.s ( 𝜑 → ( 𝑇 + 1 ) ≤ 𝑆 )
breprexplemc.1 ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑇 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑇 · 𝑁 ) ) Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑇 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑇 ) ( ( 𝐿𝑎 ) ‘ ( 𝑑𝑎 ) ) · ( 𝑍𝑚 ) ) )
Assertion breprexplemc ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( ( 𝑇 + 1 ) · 𝑁 ) ) Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑇 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑇 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑑𝑎 ) ) · ( 𝑍𝑚 ) ) )

Proof

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