breprexpnat

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 of elements of A , bounded by N . Proposition of Nathanson p. 123. (Contributed by Thierry Arnoux, 11-Dec-2021)

	Ref	Expression
Hypotheses	breprexp.n	$⊢ φ \to N \in ℕ_{0}$
	breprexp.s	$⊢ φ \to S \in ℕ_{0}$
	breprexp.z	$⊢ φ \to Z \in ℂ$
	breprexpnat.a	$⊢ φ \to A \subseteq ℕ$
	breprexpnat.p	$⊢ P = \sum_{b \in A \cap (1 \dots N)} Z^{b}$
	breprexpnat.r	$⊢ R = \|(A \cap (1 \dots N)) repr (S) m\|$
Assertion	breprexpnat	$⊢ φ \to P^{S} = \sum_{m = 0}^{S \cdot N} R 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		breprexpnat.a	$⊢ φ \to A \subseteq ℕ$
5		breprexpnat.p	$⊢ P = \sum_{b \in A \cap (1 \dots N)} Z^{b}$
6		breprexpnat.r	$⊢ R = \|(A \cap (1 \dots N)) repr (S) m\|$
7		fvex	$⊢ 𝟙_{ℕ} (A) \in V$
8	7	fconst	$⊢ ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) : (0 ..^S) ⟶ \{𝟙_{ℕ} (A)\}$
9		nnex	$⊢ ℕ \in V$
10		indf	$⊢ (ℕ \in V \land A \subseteq ℕ) \to 𝟙_{ℕ} (A) : ℕ ⟶ \{0, 1\}$
11	9 4 10	sylancr	$⊢ φ \to 𝟙_{ℕ} (A) : ℕ ⟶ \{0, 1\}$
12		0cn	$⊢ 0 \in ℂ$
13		ax-1cn	$⊢ 1 \in ℂ$
14		prssi	$⊢ (0 \in ℂ \land 1 \in ℂ) \to \{0, 1\} \subseteq ℂ$
15	12 13 14	mp2an	$⊢ \{0, 1\} \subseteq ℂ$
16		fss	$⊢ (𝟙_{ℕ} (A) : ℕ ⟶ \{0, 1\} \land \{0, 1\} \subseteq ℂ) \to 𝟙_{ℕ} (A) : ℕ ⟶ ℂ$
17	11 15 16	sylancl	$⊢ φ \to 𝟙_{ℕ} (A) : ℕ ⟶ ℂ$
18		cnex	$⊢ ℂ \in V$
19	18 9	elmap	$⊢ 𝟙_{ℕ} (A) \in (ℂ^{ℕ}) \leftrightarrow 𝟙_{ℕ} (A) : ℕ ⟶ ℂ$
20	17 19	sylibr	$⊢ φ \to 𝟙_{ℕ} (A) \in (ℂ^{ℕ})$
21	7	snss	$⊢ 𝟙_{ℕ} (A) \in (ℂ^{ℕ}) \leftrightarrow \{𝟙_{ℕ} (A)\} \subseteq ℂ^{ℕ}$
22	20 21	sylib	$⊢ φ \to \{𝟙_{ℕ} (A)\} \subseteq ℂ^{ℕ}$
23		fss	$⊢ (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) : (0 ..^S) ⟶ \{𝟙_{ℕ} (A)\} \land \{𝟙_{ℕ} (A)\} \subseteq ℂ^{ℕ}) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) : (0 ..^S) ⟶ ℂ^{ℕ}$
24	8 22 23	sylancr	$⊢ φ \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) : (0 ..^S) ⟶ ℂ^{ℕ}$
25	1 2 3 24	breprexp	$⊢ φ \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (b) Z^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) Z^{m}$
26	7	fvconst2	$⊢ a \in (0 ..^S) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) = 𝟙_{ℕ} (A)$
27	26	ad2antlr	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) = 𝟙_{ℕ} (A)$
28	27	fveq1d	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (b) = 𝟙_{ℕ} (A) (b)$
29	28	oveq1d	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (b) Z^{b} = 𝟙_{ℕ} (A) (b) Z^{b}$
30	29	sumeq2dv	$⊢ (φ \land a \in (0 ..^S)) \to \sum_{b = 1}^{N} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (b) Z^{b} = \sum_{b = 1}^{N} 𝟙_{ℕ} (A) (b) Z^{b}$
31	9	a1i	$⊢ (φ \land a \in (0 ..^S)) \to ℕ \in V$
32		fzfi	$⊢ (1 \dots N) \in Fin$
33	32	a1i	$⊢ (φ \land a \in (0 ..^S)) \to (1 \dots N) \in Fin$
34		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
35	34	a1i	$⊢ (φ \land a \in (0 ..^S)) \to (1 \dots N) \subseteq ℕ$
36	4	adantr	$⊢ (φ \land a \in (0 ..^S)) \to A \subseteq ℕ$
37	3	ad2antrr	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to Z \in ℂ$
38		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
39	34 38	sstri	$⊢ (1 \dots N) \subseteq ℕ_{0}$
40		simpr	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to b \in (1 \dots N)$
41	39 40	sselid	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to b \in ℕ_{0}$
42	37 41	expcld	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to Z^{b} \in ℂ$
43	31 33 35 36 42	indsumin	$⊢ (φ \land a \in (0 ..^S)) \to \sum_{b = 1}^{N} 𝟙_{ℕ} (A) (b) Z^{b} = \sum_{b \in (1 \dots N) \cap A} Z^{b}$
44		incom	$⊢ (1 \dots N) \cap A = A \cap (1 \dots N)$
45	44	a1i	$⊢ (φ \land a \in (0 ..^S)) \to (1 \dots N) \cap A = A \cap (1 \dots N)$
46	45	sumeq1d	$⊢ (φ \land a \in (0 ..^S)) \to \sum_{b \in (1 \dots N) \cap A} Z^{b} = \sum_{b \in A \cap (1 \dots N)} Z^{b}$
47	30 43 46	3eqtrd	$⊢ (φ \land a \in (0 ..^S)) \to \sum_{b = 1}^{N} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (b) Z^{b} = \sum_{b \in A \cap (1 \dots N)} Z^{b}$
48	47	prodeq2dv	$⊢ φ \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (b) Z^{b} = \prod_{a \in (0 ..^S)} \sum_{b \in A \cap (1 \dots N)} Z^{b}$
49		fzofi	$⊢ (0 ..^S) \in Fin$
50	49	a1i	$⊢ φ \to (0 ..^S) \in Fin$
51		inss2	$⊢ A \cap (1 \dots N) \subseteq (1 \dots N)$
52		ssfi	$⊢ ((1 \dots N) \in Fin \land A \cap (1 \dots N) \subseteq (1 \dots N)) \to A \cap (1 \dots N) \in Fin$
53	32 51 52	mp2an	$⊢ A \cap (1 \dots N) \in Fin$
54	53	a1i	$⊢ φ \to A \cap (1 \dots N) \in Fin$
55	3	adantr	$⊢ (φ \land b \in (A \cap (1 \dots N))) \to Z \in ℂ$
56	51 39	sstri	$⊢ A \cap (1 \dots N) \subseteq ℕ_{0}$
57		simpr	$⊢ (φ \land b \in (A \cap (1 \dots N))) \to b \in (A \cap (1 \dots N))$
58	56 57	sselid	$⊢ (φ \land b \in (A \cap (1 \dots N))) \to b \in ℕ_{0}$
59	55 58	expcld	$⊢ (φ \land b \in (A \cap (1 \dots N))) \to Z^{b} \in ℂ$
60	54 59	fsumcl	$⊢ φ \to \sum_{b \in A \cap (1 \dots N)} Z^{b} \in ℂ$
61		fprodconst	$⊢ ((0 ..^S) \in Fin \land \sum_{b \in A \cap (1 \dots N)} Z^{b} \in ℂ) \to \prod_{a \in (0 ..^S)} \sum_{b \in A \cap (1 \dots N)} Z^{b} = {\sum_{b \in A \cap (1 \dots N)} Z^{b}}^{\|(0 ..^S)\|}$
62	50 60 61	syl2anc	$⊢ φ \to \prod_{a \in (0 ..^S)} \sum_{b \in A \cap (1 \dots N)} Z^{b} = {\sum_{b \in A \cap (1 \dots N)} Z^{b}}^{\|(0 ..^S)\|}$
63		hashfzo0	$⊢ S \in ℕ_{0} \to \|(0 ..^S)\| = S$
64	2 63	syl	$⊢ φ \to \|(0 ..^S)\| = S$
65	64	oveq2d	$⊢ φ \to {\sum_{b \in A \cap (1 \dots N)} Z^{b}}^{\|(0 ..^S)\|} = {\sum_{b \in A \cap (1 \dots N)} Z^{b}}^{S}$
66	48 62 65	3eqtrd	$⊢ φ \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (b) Z^{b} = {\sum_{b \in A \cap (1 \dots N)} Z^{b}}^{S}$
67	34	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \subseteq ℕ$
68		fzssz	$⊢ (0 \dots S \cdot N) \subseteq ℤ$
69		simpr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in (0 \dots S \cdot N)$
70	68 69	sselid	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in ℤ$
71	2	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to S \in ℕ_{0}$
72	32	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \in Fin$
73	67 70 71 72	reprfi	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) repr (S) m \in Fin$
74	3	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to Z \in ℂ$
75		fz0ssnn0	$⊢ (0 \dots S \cdot N) \subseteq ℕ_{0}$
76	75 69	sselid	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in ℕ_{0}$
77	74 76	expcld	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to Z^{m} \in ℂ$
78	49	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (0 ..^S) \in Fin$
79	11	ad3antrrr	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to 𝟙_{ℕ} (A) : ℕ ⟶ \{0, 1\}$
80	34	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (1 \dots N) \subseteq ℕ$
81	70	adantr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m \in ℤ$
82	71	adantr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to S \in ℕ_{0}$
83		simpr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to c \in ((1 \dots N) repr (S) m)$
84	80 81 82 83	reprf	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to c : (0 ..^S) ⟶ (1 \dots N)$
85	84	ffvelcdmda	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to c (a) \in (1 \dots N)$
86	34 85	sselid	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to c (a) \in ℕ$
87	79 86	ffvelcdmd	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to 𝟙_{ℕ} (A) (c (a)) \in \{0, 1\}$
88	15 87	sselid	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to 𝟙_{ℕ} (A) (c (a)) \in ℂ$
89	78 88	fprodcl	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) \in ℂ$
90	73 77 89	fsummulc1	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) Z^{m}$
91	4	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to A \subseteq ℕ$
92	91 70 71 72 67	hashreprin	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \|(A \cap (1 \dots N)) repr (S) m\| = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
93	92	oveq1d	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \|(A \cap (1 \dots N)) repr (S) m\| Z^{m} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) Z^{m}$
94	26	fveq1d	$⊢ a \in (0 ..^S) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = 𝟙_{ℕ} (A) (c (a))$
95	94	adantl	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land a \in (0 ..^S)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = 𝟙_{ℕ} (A) (c (a))$
96	95	prodeq2dv	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
97	96	adantr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
98	97	oveq1d	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) Z^{m} = \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) Z^{m}$
99	98	sumeq2dv	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) Z^{m} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a)) Z^{m}$
100	90 93 99	3eqtr4rd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) Z^{m} = \|(A \cap (1 \dots N)) repr (S) m\| Z^{m}$
101	100	sumeq2dv	$⊢ φ \to \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) Z^{m} = \sum_{m = 0}^{S \cdot N} \|(A \cap (1 \dots N)) repr (S) m\| Z^{m}$
102	25 66 101	3eqtr3d	$⊢ φ \to {\sum_{b \in A \cap (1 \dots N)} Z^{b}}^{S} = \sum_{m = 0}^{S \cdot N} \|(A \cap (1 \dots N)) repr (S) m\| Z^{m}$
103	5	oveq1i	$⊢ P^{S} = {\sum_{b \in A \cap (1 \dots N)} Z^{b}}^{S}$
104	6	oveq1i	$⊢ R Z^{m} = \|(A \cap (1 \dots N)) repr (S) m\| Z^{m}$
105	104	a1i	$⊢ m \in (0 \dots S \cdot N) \to R Z^{m} = \|(A \cap (1 \dots N)) repr (S) m\| Z^{m}$
106	105	sumeq2i	$⊢ \sum_{m = 0}^{S \cdot N} R Z^{m} = \sum_{m = 0}^{S \cdot N} \|(A \cap (1 \dots N)) repr (S) m\| Z^{m}$
107	102 103 106	3eqtr4g	$⊢ φ \to P^{S} = \sum_{m = 0}^{S \cdot N} R Z^{m}$

Metamath Proof Explorer

Theorem breprexpnat

Proof