breprexp

Description: Express the S th power of the finite series in terms of the number of representations of integers m as sums of S terms. This is a general formulation which allows logarithmic weighting of the sums (see https://mathoverflow.net/questions/253246) and a mix of different smoothing functions taken into account in L . See breprexpnat for the simple case presented in the proposition of Nathanson p. 123. (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) ⟶ ℂ^{ℕ}$
Assertion	breprexp	$⊢ φ \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (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		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
6	5	a1i	$⊢ φ \to ℕ_{0} \subseteq ℝ$
7	6	sselda	$⊢ (φ \land S \in ℕ_{0}) \to S \in ℝ$
8		leid	$⊢ S \in ℝ \to S \leq S$
9	7 8	syl	$⊢ (φ \land S \in ℕ_{0}) \to S \leq S$
10		breq1	$⊢ t = 0 \to (t \leq S \leftrightarrow 0 \leq S)$
11		oveq2	$⊢ t = 0 \to (0 ..^t) = (0 ..^0)$
12	11	prodeq1d	$⊢ t = 0 \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b}$
13		oveq1	$⊢ t = 0 \to t \cdot N = 0 \cdot N$
14	13	oveq2d	$⊢ t = 0 \to (0 \dots t \cdot N) = (0 \dots 0 \cdot N)$
15		fveq2	$⊢ t = 0 \to repr (t) = repr (0)$
16	15	oveqd	$⊢ t = 0 \to (1 \dots N) repr (t) m = (1 \dots N) repr (0) m$
17	11	prodeq1d	$⊢ t = 0 \to \prod_{a \in (0 ..^t)} L (a) (c (a)) = \prod_{a \in (0 ..^0)} L (a) (c (a))$
18	17	oveq1d	$⊢ t = 0 \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}$
19	18	adantr	$⊢ (t = 0 \land c \in ((1 \dots N) repr (t) m)) \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}$
20	16 19	sumeq12dv	$⊢ t = 0 \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}$
21	20	adantr	$⊢ (t = 0 \land m \in (0 \dots t \cdot N)) \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}$
22	14 21	sumeq12dv	$⊢ t = 0 \to \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{m = 0}^{0 \cdot N} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}$
23	12 22	eqeq12d	$⊢ t = 0 \to (\prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} \leftrightarrow \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{0 \cdot N} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m})$
24	10 23	imbi12d	$⊢ t = 0 \to ((t \leq S \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m}) \leftrightarrow (0 \leq S \to \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{0 \cdot N} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}))$
25		breq1	$⊢ t = s \to (t \leq S \leftrightarrow s \leq S)$
26		oveq2	$⊢ t = s \to (0 ..^t) = (0 ..^s)$
27	26	prodeq1d	$⊢ t = s \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b}$
28		oveq1	$⊢ t = s \to t \cdot N = s \cdot N$
29	28	oveq2d	$⊢ t = s \to (0 \dots t \cdot N) = (0 \dots s \cdot N)$
30		fveq2	$⊢ t = s \to repr (t) = repr (s)$
31	30	oveqd	$⊢ t = s \to (1 \dots N) repr (t) m = (1 \dots N) repr (s) m$
32	26	prodeq1d	$⊢ t = s \to \prod_{a \in (0 ..^t)} L (a) (c (a)) = \prod_{a \in (0 ..^s)} L (a) (c (a))$
33	32	oveq1d	$⊢ t = s \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}$
34	33	adantr	$⊢ (t = s \land c \in ((1 \dots N) repr (t) m)) \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}$
35	31 34	sumeq12dv	$⊢ t = s \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}$
36	35	adantr	$⊢ (t = s \land m \in (0 \dots t \cdot N)) \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}$
37	29 36	sumeq12dv	$⊢ t = s \to \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}$
38	27 37	eqeq12d	$⊢ t = s \to (\prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} \leftrightarrow \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})$
39	25 38	imbi12d	$⊢ t = s \to ((t \leq S \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m}) \leftrightarrow (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}))$
40		breq1	$⊢ t = s + 1 \to (t \leq S \leftrightarrow s + 1 \leq S)$
41		oveq2	$⊢ t = s + 1 \to (0 ..^t) = (0 ..^s + 1)$
42	41	prodeq1d	$⊢ t = s + 1 \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \prod_{a \in (0 ..^s + 1)} \sum_{b = 1}^{N} L (a) (b) Z^{b}$
43		oveq1	$⊢ t = s + 1 \to t \cdot N = (s + 1) \cdot N$
44	43	oveq2d	$⊢ t = s + 1 \to (0 \dots t \cdot N) = (0 \dots (s + 1) \cdot N)$
45		fveq2	$⊢ t = s + 1 \to repr (t) = repr (s + 1)$
46	45	oveqd	$⊢ t = s + 1 \to (1 \dots N) repr (t) m = (1 \dots N) repr (s + 1) m$
47	41	prodeq1d	$⊢ t = s + 1 \to \prod_{a \in (0 ..^t)} L (a) (c (a)) = \prod_{a \in (0 ..^s + 1)} L (a) (c (a))$
48	47	oveq1d	$⊢ t = s + 1 \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}$
49	48	adantr	$⊢ (t = s + 1 \land c \in ((1 \dots N) repr (t) m)) \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}$
50	46 49	sumeq12dv	$⊢ t = s + 1 \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}$
51	50	adantr	$⊢ (t = s + 1 \land m \in (0 \dots t \cdot N)) \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}$
52	44 51	sumeq12dv	$⊢ t = s + 1 \to \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{m = 0}^{(s + 1) \cdot N} \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}$
53	42 52	eqeq12d	$⊢ t = s + 1 \to (\prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} \leftrightarrow \prod_{a \in (0 ..^s + 1)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{(s + 1) \cdot N} \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m})$
54	40 53	imbi12d	$⊢ t = s + 1 \to ((t \leq S \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m}) \leftrightarrow (s + 1 \leq S \to \prod_{a \in (0 ..^s + 1)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{(s + 1) \cdot N} \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}))$
55		breq1	$⊢ t = S \to (t \leq S \leftrightarrow S \leq S)$
56		oveq2	$⊢ t = S \to (0 ..^t) = (0 ..^S)$
57	56	prodeq1d	$⊢ t = S \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) Z^{b}$
58		oveq1	$⊢ t = S \to t \cdot N = S \cdot N$
59	58	oveq2d	$⊢ t = S \to (0 \dots t \cdot N) = (0 \dots S \cdot N)$
60		fveq2	$⊢ t = S \to repr (t) = repr (S)$
61	60	oveqd	$⊢ t = S \to (1 \dots N) repr (t) m = (1 \dots N) repr (S) m$
62	56	prodeq1d	$⊢ t = S \to \prod_{a \in (0 ..^t)} L (a) (c (a)) = \prod_{a \in (0 ..^S)} L (a) (c (a))$
63	62	oveq1d	$⊢ t = S \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}$
64	63	adantr	$⊢ (t = S \land c \in ((1 \dots N) repr (t) m)) \to \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}$
65	61 64	sumeq12dv	$⊢ t = S \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}$
66	65	adantr	$⊢ (t = S \land m \in (0 \dots t \cdot N)) \to \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}$
67	59 66	sumeq12dv	$⊢ t = S \to \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}$
68	57 67	eqeq12d	$⊢ t = S \to (\prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m} \leftrightarrow \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m})$
69	55 68	imbi12d	$⊢ t = S \to ((t \leq S \to \prod_{a \in (0 ..^t)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{t \cdot N} \sum_{c \in (1 \dots N) repr (t) m} \prod_{a \in (0 ..^t)} L (a) (c (a)) Z^{m}) \leftrightarrow (S \leq S \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}))$
70		0nn0	$⊢ 0 \in ℕ_{0}$
71		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
72	71	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
73		0zd	$⊢ φ \to 0 \in ℤ$
74	72 73 1	repr0	$⊢ φ \to (1 \dots N) repr (0) 0 = if (0 = 0, \{\emptyset\}, \emptyset)$
75		eqid	$⊢ 0 = 0$
76	75	iftruei	$⊢ if (0 = 0, \{\emptyset\}, \emptyset) = \{\emptyset\}$
77	74 76	eqtrdi	$⊢ φ \to (1 \dots N) repr (0) 0 = \{\emptyset\}$
78		snfi	$⊢ \{\emptyset\} \in Fin$
79	77 78	eqeltrdi	$⊢ φ \to (1 \dots N) repr (0) 0 \in Fin$
80		fzo0	$⊢ (0 ..^0) = \emptyset$
81	80	prodeq1i	$⊢ \prod_{a \in (0 ..^0)} L (a) (c (a)) = \prod_{a \in \emptyset} L (a) (c (a))$
82		prod0	$⊢ \prod_{a \in \emptyset} L (a) (c (a)) = 1$
83	81 82	eqtri	$⊢ \prod_{a \in (0 ..^0)} L (a) (c (a)) = 1$
84	83	a1i	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (c (a)) = 1$
85		exp0	$⊢ Z \in ℂ \to Z^{0} = 1$
86	3 85	syl	$⊢ φ \to Z^{0} = 1$
87	84 86	oveq12d	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} = 1 \cdot 1$
88		ax-1cn	$⊢ 1 \in ℂ$
89	88	mulid1i	$⊢ 1 \cdot 1 = 1$
90	87 89	eqtrdi	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} = 1$
91	90 88	eqeltrdi	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} \in ℂ$
92	91	adantr	$⊢ (φ \land c \in ((1 \dots N) repr (0) 0)) \to \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} \in ℂ$
93	79 92	fsumcl	$⊢ φ \to \sum_{c \in (1 \dots N) repr (0) 0} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} \in ℂ$
94		oveq2	$⊢ m = 0 \to (1 \dots N) repr (0) m = (1 \dots N) repr (0) 0$
95		simpl	$⊢ (m = 0 \land c \in ((1 \dots N) repr (0) m)) \to m = 0$
96	95	oveq2d	$⊢ (m = 0 \land c \in ((1 \dots N) repr (0) m)) \to Z^{m} = Z^{0}$
97	96	oveq2d	$⊢ (m = 0 \land c \in ((1 \dots N) repr (0) m)) \to \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0}$
98	94 97	sumeq12dv	$⊢ m = 0 \to \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (0) 0} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0}$
99	98	sumsn	$⊢ (0 \in ℕ_{0} \land \sum_{c \in (1 \dots N) repr (0) 0} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} \in ℂ) \to \sum_{m \in \{0\}} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (0) 0} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0}$
100	70 93 99	sylancr	$⊢ φ \to \sum_{m \in \{0\}} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (0) 0} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0}$
101	77	sumeq1d	$⊢ φ \to \sum_{c \in (1 \dots N) repr (0) 0} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} = \sum_{c \in \{\emptyset\}} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0}$
102		0ex	$⊢ \emptyset \in V$
103	80	prodeq1i	$⊢ \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) = \prod_{a \in \emptyset} L (a) (\emptyset (a))$
104		prod0	$⊢ \prod_{a \in \emptyset} L (a) (\emptyset (a)) = 1$
105	103 104	eqtri	$⊢ \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) = 1$
106	105	a1i	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) = 1$
107	106 88	eqeltrdi	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) \in ℂ$
108	86 88	eqeltrdi	$⊢ φ \to Z^{0} \in ℂ$
109	107 108	mulcld	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) Z^{0} \in ℂ$
110		fveq1	$⊢ c = \emptyset \to c (a) = \emptyset (a)$
111	110	fveq2d	$⊢ c = \emptyset \to L (a) (c (a)) = L (a) (\emptyset (a))$
112	111	ralrimivw	$⊢ c = \emptyset \to \forall a \in (0 ..^0) L (a) (c (a)) = L (a) (\emptyset (a))$
113	112	prodeq2d	$⊢ c = \emptyset \to \prod_{a \in (0 ..^0)} L (a) (c (a)) = \prod_{a \in (0 ..^0)} L (a) (\emptyset (a))$
114	113	oveq1d	$⊢ c = \emptyset \to \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} = \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) Z^{0}$
115	114	sumsn	$⊢ (\emptyset \in V \land \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) Z^{0} \in ℂ) \to \sum_{c \in \{\emptyset\}} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} = \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) Z^{0}$
116	102 109 115	sylancr	$⊢ φ \to \sum_{c \in \{\emptyset\}} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} = \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) Z^{0}$
117	106 86	oveq12d	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) Z^{0} = 1 \cdot 1$
118	117 87 90	3eqtr2d	$⊢ φ \to \prod_{a \in (0 ..^0)} L (a) (\emptyset (a)) Z^{0} = 1$
119	116 118	eqtrd	$⊢ φ \to \sum_{c \in \{\emptyset\}} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{0} = 1$
120	100 101 119	3eqtrd	$⊢ φ \to \sum_{m \in \{0\}} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m} = 1$
121	1	nn0cnd	$⊢ φ \to N \in ℂ$
122	121	mul02d	$⊢ φ \to 0 \cdot N = 0$
123	122	oveq2d	$⊢ φ \to (0 \dots 0 \cdot N) = (0 \dots 0)$
124		fz0sn	$⊢ (0 \dots 0) = \{0\}$
125	123 124	eqtrdi	$⊢ φ \to (0 \dots 0 \cdot N) = \{0\}$
126	125	sumeq1d	$⊢ φ \to \sum_{m = 0}^{0 \cdot N} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m} = \sum_{m \in \{0\}} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}$
127	80	prodeq1i	$⊢ \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \prod_{a \in \emptyset} \sum_{b = 1}^{N} L (a) (b) Z^{b}$
128		prod0	$⊢ \prod_{a \in \emptyset} \sum_{b = 1}^{N} L (a) (b) Z^{b} = 1$
129	127 128	eqtri	$⊢ \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = 1$
130	129	a1i	$⊢ φ \to \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = 1$
131	120 126 130	3eqtr4rd	$⊢ φ \to \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{0 \cdot N} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m}$
132	131	a1d	$⊢ φ \to (0 \leq S \to \prod_{a \in (0 ..^0)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{0 \cdot N} \sum_{c \in (1 \dots N) repr (0) m} \prod_{a \in (0 ..^0)} L (a) (c (a)) Z^{m})$
133		simpll	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})) \land s + 1 \leq S) \to (φ \land s \in ℕ_{0})$
134		simplr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})) \land s + 1 \leq S) \to (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})$
135		oveq2	$⊢ m = n \to (1 \dots N) repr (s) m = (1 \dots N) repr (s) n$
136		oveq2	$⊢ m = n \to Z^{m} = Z^{n}$
137	136	oveq2d	$⊢ m = n \to \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n}$
138	137	adantr	$⊢ (m = n \land c \in ((1 \dots N) repr (s) m)) \to \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n}$
139	135 138	sumeq12dv	$⊢ m = n \to \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n}$
140	139	cbvsumv	$⊢ \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m} = \sum_{n = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n}$
141	140	eqeq2i	$⊢ \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m} \leftrightarrow \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{n = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n}$
142		simpl	$⊢ (a = i \land b \in (1 \dots N)) \to a = i$
143	142	fveq2d	$⊢ (a = i \land b \in (1 \dots N)) \to L (a) = L (i)$
144	143	fveq1d	$⊢ (a = i \land b \in (1 \dots N)) \to L (a) (b) = L (i) (b)$
145	144	oveq1d	$⊢ (a = i \land b \in (1 \dots N)) \to L (a) (b) Z^{b} = L (i) (b) Z^{b}$
146	145	sumeq2dv	$⊢ a = i \to \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{b = 1}^{N} L (i) (b) Z^{b}$
147	146	cbvprodv	$⊢ \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \prod_{i \in (0 ..^s)} \sum_{b = 1}^{N} L (i) (b) Z^{b}$
148		fveq2	$⊢ b = j \to L (i) (b) = L (i) (j)$
149		oveq2	$⊢ b = j \to Z^{b} = Z^{j}$
150	148 149	oveq12d	$⊢ b = j \to L (i) (b) Z^{b} = L (i) (j) Z^{j}$
151	150	cbvsumv	$⊢ \sum_{b = 1}^{N} L (i) (b) Z^{b} = \sum_{j = 1}^{N} L (i) (j) Z^{j}$
152	151	a1i	$⊢ i \in (0 ..^s) \to \sum_{b = 1}^{N} L (i) (b) Z^{b} = \sum_{j = 1}^{N} L (i) (j) Z^{j}$
153	152	prodeq2i	$⊢ \prod_{i \in (0 ..^s)} \sum_{b = 1}^{N} L (i) (b) Z^{b} = \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j}$
154	147 153	eqtri	$⊢ \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j}$
155		fveq2	$⊢ a = i \to L (a) = L (i)$
156		fveq2	$⊢ a = i \to c (a) = c (i)$
157	155 156	fveq12d	$⊢ a = i \to L (a) (c (a)) = L (i) (c (i))$
158	157	cbvprodv	$⊢ \prod_{a \in (0 ..^s)} L (a) (c (a)) = \prod_{i \in (0 ..^s)} L (i) (c (i))$
159	158	oveq1i	$⊢ \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n} = \prod_{i \in (0 ..^s)} L (i) (c (i)) Z^{n}$
160	159	a1i	$⊢ c \in ((1 \dots N) repr (s) n) \to \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n} = \prod_{i \in (0 ..^s)} L (i) (c (i)) Z^{n}$
161	160	sumeq2i	$⊢ \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n} = \sum_{c \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (c (i)) Z^{n}$
162		simpl	$⊢ (c = k \land i \in (0 ..^s)) \to c = k$
163	162	fveq1d	$⊢ (c = k \land i \in (0 ..^s)) \to c (i) = k (i)$
164	163	fveq2d	$⊢ (c = k \land i \in (0 ..^s)) \to L (i) (c (i)) = L (i) (k (i))$
165	164	prodeq2dv	$⊢ c = k \to \prod_{i \in (0 ..^s)} L (i) (c (i)) = \prod_{i \in (0 ..^s)} L (i) (k (i))$
166	165	oveq1d	$⊢ c = k \to \prod_{i \in (0 ..^s)} L (i) (c (i)) Z^{n} = \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n}$
167	166	cbvsumv	$⊢ \sum_{c \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (c (i)) Z^{n} = \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n}$
168	161 167	eqtri	$⊢ \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n} = \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n}$
169	168	a1i	$⊢ n \in (0 \dots s \cdot N) \to \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n} = \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n}$
170	169	sumeq2i	$⊢ \sum_{n = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n}$
171	154 170	eqeq12i	$⊢ \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{n = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) n} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{n} \leftrightarrow \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n}$
172	141 171	bitri	$⊢ \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m} \leftrightarrow \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n}$
173	172	imbi2i	$⊢ (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}) \leftrightarrow (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})$
174	134 173	sylib	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})) \land s + 1 \leq S) \to (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})$
175		simpr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})) \land s + 1 \leq S) \to s + 1 \leq S$
176	1	ad3antrrr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to N \in ℕ_{0}$
177	2	ad3antrrr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to S \in ℕ_{0}$
178	3	ad3antrrr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to Z \in ℂ$
179	4	ad3antrrr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
180		simpllr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to s \in ℕ_{0}$
181		simpr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to s + 1 \leq S$
182	5 180	sseldi	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to s \in ℝ$
183		1red	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to 1 \in ℝ$
184	182 183	readdcld	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to s + 1 \in ℝ$
185	5 177	sseldi	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to S \in ℝ$
186	182	ltp1d	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to s < s + 1$
187	182 184 186	ltled	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to s \leq s + 1$
188	182 184 185 187 181	letrd	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to s \leq S$
189		simplr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})$
190	189 173	sylibr	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})$
191	188 190	mpd	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m}$
192	176 177 178 179 180 181 191	breprexplemc	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{i \in (0 ..^s)} \sum_{j = 1}^{N} L (i) (j) Z^{j} = \sum_{n = 0}^{s \cdot N} \sum_{k \in (1 \dots N) repr (s) n} \prod_{i \in (0 ..^s)} L (i) (k (i)) Z^{n})) \land s + 1 \leq S) \to \prod_{a \in (0 ..^s + 1)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{(s + 1) \cdot N} \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}$
193	133 174 175 192	syl21anc	$⊢ (((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})) \land s + 1 \leq S) \to \prod_{a \in (0 ..^s + 1)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{(s + 1) \cdot N} \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m}$
194	193	ex	$⊢ ((φ \land s \in ℕ_{0}) \land (s \leq S \to \prod_{a \in (0 ..^s)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{s \cdot N} \sum_{c \in (1 \dots N) repr (s) m} \prod_{a \in (0 ..^s)} L (a) (c (a)) Z^{m})) \to (s + 1 \leq S \to \prod_{a \in (0 ..^s + 1)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{(s + 1) \cdot N} \sum_{c \in (1 \dots N) repr (s + 1) m} \prod_{a \in (0 ..^s + 1)} L (a) (c (a)) Z^{m})$
195	24 39 54 69 132 194	nn0indd	$⊢ (φ \land S \in ℕ_{0}) \to (S \leq S \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m})$
196	9 195	mpd	$⊢ (φ \land S \in ℕ_{0}) \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}$
197	2 196	mpdan	$⊢ φ \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) Z^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) Z^{m}$

Metamath Proof Explorer

Theorem breprexp

Proof