Metamath Proof Explorer

Theorem breprexplemc

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

Ref Expression
Hypotheses breprexp.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
breprexp.s ${⊢}{\phi }\to {S}\in {ℕ}_{0}$
breprexp.z ${⊢}{\phi }\to {Z}\in ℂ$
breprexp.h ${⊢}{\phi }\to {L}:\left(0..^{S}\right)⟶{ℂ}^{ℕ}$
breprexplemc.t ${⊢}{\phi }\to {T}\in {ℕ}_{0}$
breprexplemc.s ${⊢}{\phi }\to {T}+1\le {S}$
breprexplemc.1 ${⊢}{\phi }\to \prod _{{a}\in \left(0..^{T}\right)}\sum _{{b}=1}^{{N}}{L}\left({a}\right)\left({b}\right){{Z}}^{{b}}=\sum _{{m}=0}^{{T}\cdot {N}}\sum _{{d}\in \left(1\dots {N}\right)\mathrm{repr}\left({T}\right){m}}\prod _{{a}\in \left(0..^{T}\right)}{L}\left({a}\right)\left({d}\left({a}\right)\right){{Z}}^{{m}}$
Assertion breprexplemc ${⊢}{\phi }\to \prod _{{a}\in \left(0..^{T}+1\right)}\sum _{{b}=1}^{{N}}{L}\left({a}\right)\left({b}\right){{Z}}^{{b}}=\sum _{{m}=0}^{\left({T}+1\right)\cdot {N}}\sum _{{d}\in \left(1\dots {N}\right)\mathrm{repr}\left({T}+1\right){m}}\prod _{{a}\in \left(0..^{T}+1\right)}{L}\left({a}\right)\left({d}\left({a}\right)\right){{Z}}^{{m}}$

Proof

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