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 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 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 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 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 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 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 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ - 𝑏 ) ∧ 𝑏 ∈ ( 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 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( 𝑍 ↑ 𝑚 ) ) )