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