breprexplemc

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

	Ref	Expression
Hypotheses	breprexp.n	$⊢ φ \to N \in ℕ_{0}$
	breprexp.s	$⊢ φ \to S \in ℕ_{0}$
	breprexp.z	$⊢ φ \to Z \in ℂ$
	breprexp.h	$⊢ φ \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
	breprexplemc.t	$⊢ φ \to T \in ℕ_{0}$
	breprexplemc.s	$⊢ φ \to T + 1 \leq S$
	breprexplemc.1	$⊢ φ \to \prod_{a \in (0 ..^T)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{T \cdot N} \sum_{d \in (1 \dots N) repr (T) m} \prod_{a \in (0 ..^T)} L (a) (d (a)) Z^{m}$
Assertion	breprexplemc	$⊢ φ \to \prod_{a \in (0 ..^T + 1)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{(T + 1) \cdot N} \sum_{d \in (1 \dots N) repr (T + 1) m} \prod_{a \in (0 ..^T + 1)} L (a) (d (a)) Z^{m}$

Proof

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

Metamath Proof Explorer

Theorem breprexplemc

Proof