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