circlemeth

Description: The Hardy, Littlewood and Ramanujan Circle Method, in a generic form, with different weighting / smoothing functions. (Contributed by Thierry Arnoux, 13-Dec-2021)

	Ref	Expression
Hypotheses	circlemeth.n	$⊢ φ \to N \in ℕ_{0}$
	circlemeth.s	$⊢ φ \to S \in ℕ$
	circlemeth.l	$⊢ φ \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
Assertion	circlemeth	$⊢ φ \to \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \int_{(0, 1)} \prod_{a \in (0 ..^S)} (L (a) vts N) (x) e^{i 2 π -N x} d x$

Proof

Step	Hyp	Ref	Expression
1		circlemeth.n	$⊢ φ \to N \in ℕ_{0}$
2		circlemeth.s	$⊢ φ \to S \in ℕ$
3		circlemeth.l	$⊢ φ \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
4	1	adantr	$⊢ (φ \land x \in (0, 1)) \to N \in ℕ_{0}$
5		ioossre	$⊢ (0, 1) \subseteq ℝ$
6		ax-resscn	$⊢ ℝ \subseteq ℂ$
7	5 6	sstri	$⊢ (0, 1) \subseteq ℂ$
8	7	a1i	$⊢ φ \to (0, 1) \subseteq ℂ$
9	8	sselda	$⊢ (φ \land x \in (0, 1)) \to x \in ℂ$
10	2	nnnn0d	$⊢ φ \to S \in ℕ_{0}$
11	10	adantr	$⊢ (φ \land x \in (0, 1)) \to S \in ℕ_{0}$
12	3	adantr	$⊢ (φ \land x \in (0, 1)) \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
13	4 9 11 12	vtsprod	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^S)} (L (a) vts N) (x) = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x}$
14	13	oveq1d	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^S)} (L (a) vts N) (x) e^{i 2 π -N x} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x}$
15		fzfid	$⊢ (φ \land x \in (0, 1)) \to (0 \dots S \cdot N) \in Fin$
16		ax-icn	$⊢ i \in ℂ$
17		2cn	$⊢ 2 \in ℂ$
18		picn	$⊢ π \in ℂ$
19	17 18	mulcli	$⊢ 2 π \in ℂ$
20	16 19	mulcli	$⊢ i 2 π \in ℂ$
21	20	a1i	$⊢ (φ \land x \in (0, 1)) \to i 2 π \in ℂ$
22	1	nn0cnd	$⊢ φ \to N \in ℂ$
23	22	negcld	$⊢ φ \to - N \in ℂ$
24	23	ralrimivw	$⊢ φ \to \forall x \in (0, 1) - N \in ℂ$
25	24	r19.21bi	$⊢ (φ \land x \in (0, 1)) \to - N \in ℂ$
26	25 9	mulcld	$⊢ (φ \land x \in (0, 1)) \to -N x \in ℂ$
27	21 26	mulcld	$⊢ (φ \land x \in (0, 1)) \to i 2 π -N x \in ℂ$
28	27	efcld	$⊢ (φ \land x \in (0, 1)) \to e^{i 2 π -N x} \in ℂ$
29		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
30	29	a1i	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \subseteq ℕ$
31		fzssz	$⊢ (0 \dots S \cdot N) \subseteq ℤ$
32		simpr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in (0 \dots S \cdot N)$
33	31 32	sseldi	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in ℤ$
34	33	adantlr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m \in ℤ$
35	11	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to S \in ℕ_{0}$
36		fzfid	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \in Fin$
37	30 34 35 36	reprfi	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (1 \dots N) repr (S) m \in Fin$
38		fzofi	$⊢ (0 ..^S) \in Fin$
39	38	a1i	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (0 ..^S) \in Fin$
40	1	ad3antrrr	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to N \in ℕ_{0}$
41	10	ad3antrrr	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to S \in ℕ_{0}$
42	33	zcnd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in ℂ$
43	42	ad2antrr	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to m \in ℂ$
44	3	ad3antrrr	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
45		simpr	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
46	29	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (1 \dots N) \subseteq ℕ$
47	33	adantr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m \in ℤ$
48	10	ad2antrr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to S \in ℕ_{0}$
49		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)$
50	46 47 48 49	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)$
51	50	ffvelrnda	$⊢ (((φ \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)$
52	29 51	sseldi	$⊢ (((φ \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 ℕ$
53	40 41 43 44 45 52	breprexplemb	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to L (a) (c (a)) \in ℂ$
54	53	adantl3r	$⊢ ((((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to L (a) (c (a)) \in ℂ$
55	39 54	fprodcl	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
56	20	a1i	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π \in ℂ$
57	34	zcnd	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m \in ℂ$
58	9	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to x \in ℂ$
59	57 58	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m x \in ℂ$
60	56 59	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π m x \in ℂ$
61	60	efcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to e^{i 2 π m x} \in ℂ$
62	61	adantr	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to e^{i 2 π m x} \in ℂ$
63	55 62	mulcld	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} \in ℂ$
64	37 63	fsumcl	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} \in ℂ$
65	15 28 64	fsummulc1	$⊢ (φ \land x \in (0, 1)) \to \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x}$
66	28	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to e^{i 2 π -N x} \in ℂ$
67	37 66 63	fsummulc1	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x}$
68	66	adantr	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to e^{i 2 π -N x} \in ℂ$
69	55 62 68	mulassd	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x}$
70	27	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π -N x \in ℂ$
71		efadd	$⊢ (i 2 π m x \in ℂ \land i 2 π -N x \in ℂ) \to e^{i 2 π m x + i 2 π -N x} = e^{i 2 π m x} e^{i 2 π -N x}$
72	60 70 71	syl2anc	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to e^{i 2 π m x + i 2 π -N x} = e^{i 2 π m x} e^{i 2 π -N x}$
73	26	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to -N x \in ℂ$
74	56 59 73	adddid	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π (m x + -N x) = i 2 π m x + i 2 π -N x$
75	25	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to - N \in ℂ$
76	57 75 58	adddird	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (m + -N) x = m x + -N x$
77	22	ad2antrr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to N \in ℂ$
78	57 77	negsubd	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m + -N = m - N$
79	78	oveq1d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (m + -N) x = (m - N) x$
80	76 79	eqtr3d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m x + -N x = (m - N) x$
81	80	oveq2d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π (m x + -N x) = i 2 π (m - N) x$
82	74 81	eqtr3d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π m x + i 2 π -N x = i 2 π (m - N) x$
83	82	fveq2d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to e^{i 2 π m x + i 2 π -N x} = e^{i 2 π (m - N) x}$
84	72 83	eqtr3d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to e^{i 2 π m x} e^{i 2 π -N x} = e^{i 2 π (m - N) x}$
85	84	oveq2d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}$
86	85	adantr	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}$
87	69 86	eqtrd	$⊢ (((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}$
88	87	sumeq2dv	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}$
89	67 88	eqtrd	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}$
90	89	sumeq2dv	$⊢ (φ \land x \in (0, 1)) \to \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m x} e^{i 2 π -N x} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}$
91	14 65 90	3eqtrd	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^S)} (L (a) vts N) (x) e^{i 2 π -N x} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}$
92	91	itgeq2dv	$⊢ φ \to \int_{(0, 1)} \prod_{a \in (0 ..^S)} (L (a) vts N) (x) e^{i 2 π -N x} d x = \int_{(0, 1)} \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x$
93		ioombl	$⊢ (0, 1) \in dom vol$
94	93	a1i	$⊢ φ \to (0, 1) \in dom vol$
95		fzfid	$⊢ φ \to (0 \dots S \cdot N) \in Fin$
96		sumex	$⊢ \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} \in V$
97	96	a1i	$⊢ (φ \land (x \in (0, 1) \land m \in (0 \dots S \cdot N))) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} \in V$
98	94	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (0, 1) \in dom vol$
99	29	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \subseteq ℕ$
100	10	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to S \in ℕ_{0}$
101		fzfid	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \in Fin$
102	99 33 100 101	reprfi	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) repr (S) m \in Fin$
103	38	a1i	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \land c \in ((1 \dots N) repr (S) m)) \to (0 ..^S) \in Fin$
104	53	adantllr	$⊢ ((((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \land c \in ((1 \dots N) repr (S) m)) \land a \in (0 ..^S)) \to L (a) (c (a)) \in ℂ$
105	103 104	fprodcl	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
106	57 77	subcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m - N \in ℂ$
107	106 58	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (m - N) x \in ℂ$
108	56 107	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π (m - N) x \in ℂ$
109	108	an32s	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \to i 2 π (m - N) x \in ℂ$
110	109	adantr	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \land c \in ((1 \dots N) repr (S) m)) \to i 2 π (m - N) x \in ℂ$
111	110	efcld	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \land c \in ((1 \dots N) repr (S) m)) \to e^{i 2 π (m - N) x} \in ℂ$
112	105 111	mulcld	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} \in ℂ$
113	112	anasss	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land (x \in (0, 1) \land c \in ((1 \dots N) repr (S) m))) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} \in ℂ$
114	38	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (0 ..^S) \in Fin$
115	114 53	fprodcl	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
116		fvex	$⊢ e^{i 2 π (m - N) x} \in V$
117	116	a1i	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land x \in (0, 1)) \to e^{i 2 π (m - N) x} \in V$
118		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
119	118	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (0, 1) \subseteq [0, 1]$
120	93	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (0, 1) \in dom vol$
121	116	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land x \in [0, 1]) \to e^{i 2 π (m - N) x} \in V$
122		0red	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 0 \in ℝ$
123		1red	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 1 \in ℝ$
124	22	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to N \in ℂ$
125	42 124	subcld	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m - N \in ℂ$
126		unitsscn	$⊢ [0, 1] \subseteq ℂ$
127	126	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to [0, 1] \subseteq ℂ$
128		ssidd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to ℂ \subseteq ℂ$
129		cncfmptc	$⊢ (m - N \in ℂ \land [0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [0, 1] ⟼ m - N) : [0, 1] \underset{cn}{⟶} ℂ$
130	125 127 128 129	syl3anc	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ m - N) : [0, 1] \underset{cn}{⟶} ℂ$
131		cncfmptid	$⊢ ([0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [0, 1] ⟼ x) : [0, 1] \underset{cn}{⟶} ℂ$
132	127 128 131	syl2anc	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ x) : [0, 1] \underset{cn}{⟶} ℂ$
133	130 132	mulcncf	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ (m - N) x) : [0, 1] \underset{cn}{⟶} ℂ$
134	133	efmul2picn	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ e^{i 2 π (m - N) x}) : [0, 1] \underset{cn}{⟶} ℂ$
135		cniccibl	$⊢ (0 \in ℝ \land 1 \in ℝ \land (x \in [0, 1] ⟼ e^{i 2 π (m - N) x}) : [0, 1] \underset{cn}{⟶} ℂ) \to (x \in [0, 1] ⟼ e^{i 2 π (m - N) x}) \in 𝐿^{1}$
136	122 123 134 135	syl3anc	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ e^{i 2 π (m - N) x}) \in 𝐿^{1}$
137	119 120 121 136	iblss	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in (0, 1) ⟼ e^{i 2 π (m - N) x}) \in 𝐿^{1}$
138	137	adantr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (x \in (0, 1) ⟼ e^{i 2 π (m - N) x}) \in 𝐿^{1}$
139	115 117 138	iblmulc2	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (x \in (0, 1) ⟼ \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}) \in 𝐿^{1}$
140	98 102 113 139	itgfsum	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to ((x \in (0, 1) ⟼ \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}) \in 𝐿^{1} \land \int_{(0, 1)} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x = \sum_{c \in (1 \dots N) repr (S) m} \int_{(0, 1)} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x)$
141	140	simpld	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in (0, 1) ⟼ \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}) \in 𝐿^{1}$
142	94 95 97 141	itgfsum	$⊢ φ \to ((x \in (0, 1) ⟼ \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x}) \in 𝐿^{1} \land \int_{(0, 1)} \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x = \sum_{m = 0}^{S \cdot N} \int_{(0, 1)} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x)$
143	142	simprd	$⊢ φ \to \int_{(0, 1)} \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x = \sum_{m = 0}^{S \cdot N} \int_{(0, 1)} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x$
144		oveq2	$⊢ if (m - N = 0, 1, 0) = 1 \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0) = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \cdot 1$
145		oveq2	$⊢ if (m - N = 0, 1, 0) = 0 \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0) = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \cdot 0$
146	102 115	fsumcl	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
147	146	mulid1d	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \cdot 1 = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a))$
148	146	mul01d	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \cdot 0 = 0$
149	144 145 147 148	ifeq3da	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to if (m - N = 0, \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)), 0) = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0)$
150		velsn	$⊢ m \in \{N\} \leftrightarrow m = N$
151	42 124	subeq0ad	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (m - N = 0 \leftrightarrow m = N)$
152	150 151	bitr4id	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (m \in \{N\} \leftrightarrow m - N = 0)$
153	152	ifbid	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to if (m \in \{N\}, \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)), 0) = if (m - N = 0, \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)), 0)$
154	1	nn0zd	$⊢ φ \to N \in ℤ$
155	154	ad2antrr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to N \in ℤ$
156	47 155	zsubcld	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m - N \in ℤ$
157		itgexpif	$⊢ m - N \in ℤ \to \int_{(0, 1)} e^{i 2 π (m - N) x} d x = if (m - N = 0, 1, 0)$
158	156 157	syl	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \int_{(0, 1)} e^{i 2 π (m - N) x} d x = if (m - N = 0, 1, 0)$
159	158	oveq2d	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0)$
160	159	sumeq2dv	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0)$
161		1cnd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 1 \in ℂ$
162		0cnd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 0 \in ℂ$
163	161 162	ifcld	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to if (m - N = 0, 1, 0) \in ℂ$
164	102 163 115	fsummulc1	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0) = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0)$
165	160 164	eqtr4d	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) if (m - N = 0, 1, 0)$
166	149 153 165	3eqtr4rd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = if (m \in \{N\}, \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)), 0)$
167	166	sumeq2dv	$⊢ φ \to \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = \sum_{m = 0}^{S \cdot N} if (m \in \{N\}, \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)), 0)$
168		0zd	$⊢ φ \to 0 \in ℤ$
169	10	nn0zd	$⊢ φ \to S \in ℤ$
170	169 154	zmulcld	$⊢ φ \to S \cdot N \in ℤ$
171	1	nn0ge0d	$⊢ φ \to 0 \leq N$
172		nnmulge	$⊢ (S \in ℕ \land N \in ℕ_{0}) \to N \leq S \cdot N$
173	2 1 172	syl2anc	$⊢ φ \to N \leq S \cdot N$
174		elfz4	$⊢ ((0 \in ℤ \land S \cdot N \in ℤ \land N \in ℤ) \land (0 \leq N \land N \leq S \cdot N)) \to N \in (0 \dots S \cdot N)$
175	168 170 154 171 173 174	syl32anc	$⊢ φ \to N \in (0 \dots S \cdot N)$
176	175	snssd	$⊢ φ \to \{N\} \subseteq (0 \dots S \cdot N)$
177	176	sselda	$⊢ (φ \land m \in \{N\}) \to m \in (0 \dots S \cdot N)$
178	177 146	syldan	$⊢ (φ \land m \in \{N\}) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
179	178	ralrimiva	$⊢ φ \to \forall m \in \{N\} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
180	95	olcd	$⊢ φ \to ((0 \dots S \cdot N) \subseteq ℤ_{\geq 0} \lor (0 \dots S \cdot N) \in Fin)$
181		sumss2	$⊢ ((\{N\} \subseteq (0 \dots S \cdot N) \land \forall m \in \{N\} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ) \land ((0 \dots S \cdot N) \subseteq ℤ_{\geq 0} \lor (0 \dots S \cdot N) \in Fin)) \to \sum_{m \in \{N\}} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \sum_{m = 0}^{S \cdot N} if (m \in \{N\}, \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)), 0)$
182	176 179 180 181	syl21anc	$⊢ φ \to \sum_{m \in \{N\}} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \sum_{m = 0}^{S \cdot N} if (m \in \{N\}, \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)), 0)$
183	29	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
184		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
185	183 154 10 184	reprfi	$⊢ φ \to (1 \dots N) repr (S) N \in Fin$
186	38	a1i	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to (0 ..^S) \in Fin$
187	1	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to N \in ℕ_{0}$
188	10	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to S \in ℕ_{0}$
189	22	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to N \in ℂ$
190	3	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
191		simpr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
192	29	a1i	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to (1 \dots N) \subseteq ℕ$
193	154	adantr	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to N \in ℤ$
194	10	adantr	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to S \in ℕ_{0}$
195		simpr	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to c \in ((1 \dots N) repr (S) N)$
196	192 193 194 195	reprf	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to c : (0 ..^S) ⟶ (1 \dots N)$
197	196	ffvelrnda	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to c (a) \in (1 \dots N)$
198	29 197	sseldi	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to c (a) \in ℕ$
199	187 188 189 190 191 198	breprexplemb	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to L (a) (c (a)) \in ℂ$
200	186 199	fprodcl	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
201	185 200	fsumcl	$⊢ φ \to \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
202		oveq2	$⊢ m = N \to (1 \dots N) repr (S) m = (1 \dots N) repr (S) N$
203	202	sumeq1d	$⊢ m = N \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a))$
204	203	sumsn	$⊢ (N \in ℕ_{0} \land \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ) \to \sum_{m \in \{N\}} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a))$
205	1 201 204	syl2anc	$⊢ φ \to \sum_{m \in \{N\}} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a))$
206	167 182 205	3eqtr2d	$⊢ φ \to \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a))$
207	140	simprd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \int_{(0, 1)} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x = \sum_{c \in (1 \dots N) repr (S) m} \int_{(0, 1)} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x$
208	111	an32s	$⊢ (((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \land x \in (0, 1)) \to e^{i 2 π (m - N) x} \in ℂ$
209	115 208 138	itgmulc2	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = \int_{(0, 1)} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x$
210	209	sumeq2dv	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x = \sum_{c \in (1 \dots N) repr (S) m} \int_{(0, 1)} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x$
211	207 210	eqtr4d	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \int_{(0, 1)} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x$
212	211	sumeq2dv	$⊢ φ \to \sum_{m = 0}^{S \cdot N} \int_{(0, 1)} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) \int_{(0, 1)} e^{i 2 π (m - N) x} d x$
213	1 10	reprfz1	$⊢ φ \to ℕ repr (S) N = (1 \dots N) repr (S) N$
214	213	sumeq1d	$⊢ φ \to \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a))$
215	206 212 214	3eqtr4d	$⊢ φ \to \sum_{m = 0}^{S \cdot N} \int_{(0, 1)} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π (m - N) x} d x = \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a))$
216	92 143 215	3eqtrrd	$⊢ φ \to \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a)) = \int_{(0, 1)} \prod_{a \in (0 ..^S)} (L (a) vts N) (x) e^{i 2 π -N x} d x$

Metamath Proof Explorer

Theorem circlemeth

Proof