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		simpr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in (0 \dots S \cdot N)$
32	31	elfzelzd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in ℤ$
33	32	adantlr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m \in ℤ$
34	11	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to S \in ℕ_{0}$
35		fzfid	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \in Fin$
36	30 33 34 35	reprfi	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (1 \dots N) repr (S) m \in Fin$
37		fzofi	$⊢ (0 ..^S) \in Fin$
38	37	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$
39	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}$
40	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}$
41	32	zcnd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in ℂ$
42	41	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 ℂ$
43	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) ⟶ ℂ^{ℕ}$
44		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)$
45	29	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (1 \dots N) \subseteq ℕ$
46	32	adantr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m \in ℤ$
47	10	ad2antrr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to S \in ℕ_{0}$
48		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)$
49	45 46 47 48	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)$
50	49	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)$
51	29 50	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 ℕ$
52	39 40 42 43 44 51	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 ℂ$
53	52	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 ℂ$
54	38 53	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 ℂ$
55	20	a1i	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π \in ℂ$
56	33	zcnd	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m \in ℂ$
57	9	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to x \in ℂ$
58	56 57	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m x \in ℂ$
59	55 58	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π m x \in ℂ$
60	59	efcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to e^{i 2 π m x} \in ℂ$
61	60	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 ℂ$
62	54 61	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 ℂ$
63	36 62	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 ℂ$
64	15 28 63	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}$
65	28	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to e^{i 2 π -N x} \in ℂ$
66	36 65 62	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}$
67	65	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 ℂ$
68	54 61 67	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}$
69	27	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π -N x \in ℂ$
70		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}$
71	59 69 70	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}$
72	26	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to -N x \in ℂ$
73	55 58 72	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$
74	25	adantr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to - N \in ℂ$
75	56 74 57	adddird	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (m + -N) x = m x + -N x$
76	22	ad2antrr	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to N \in ℂ$
77	56 76	negsubd	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m + -N = m - N$
78	77	oveq1d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (m + -N) x = (m - N) x$
79	75 78	eqtr3d	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m x + -N x = (m - N) x$
80	79	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$
81	73 80	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$
82	81	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}$
83	71 82	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}$
84	83	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}$
85	84	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}$
86	68 85	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}$
87	86	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}$
88	66 87	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}$
89	88	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}$
90	14 64 89	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}$
91	90	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$
92		ioombl	$⊢ (0, 1) \in dom vol$
93	92	a1i	$⊢ φ \to (0, 1) \in dom vol$
94		fzfid	$⊢ φ \to (0 \dots S \cdot N) \in Fin$
95		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$
96	95	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$
97	93	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (0, 1) \in dom vol$
98	29	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \subseteq ℕ$
99	10	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to S \in ℕ_{0}$
100		fzfid	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) \in Fin$
101	98 32 99 100	reprfi	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (1 \dots N) repr (S) m \in Fin$
102	37	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$
103	52	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 ℂ$
104	102 103	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 ℂ$
105	56 76	subcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to m - N \in ℂ$
106	105 57	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to (m - N) x \in ℂ$
107	55 106	mulcld	$⊢ ((φ \land x \in (0, 1)) \land m \in (0 \dots S \cdot N)) \to i 2 π (m - N) x \in ℂ$
108	107	an32s	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land x \in (0, 1)) \to i 2 π (m - N) x \in ℂ$
109	108	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 ℂ$
110	109	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 ℂ$
111	104 110	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 ℂ$
112	111	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 ℂ$
113	37	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to (0 ..^S) \in Fin$
114	113 52	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 ℂ$
115		fvex	$⊢ e^{i 2 π (m - N) x} \in V$
116	115	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$
117		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
118	117	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (0, 1) \subseteq [0, 1]$
119	92	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (0, 1) \in dom vol$
120	115	a1i	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land x \in [0, 1]) \to e^{i 2 π (m - N) x} \in V$
121		0red	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 0 \in ℝ$
122		1red	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 1 \in ℝ$
123	22	adantr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to N \in ℂ$
124	41 123	subcld	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m - N \in ℂ$
125		unitsscn	$⊢ [0, 1] \subseteq ℂ$
126	125	a1i	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to [0, 1] \subseteq ℂ$
127		ssidd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to ℂ \subseteq ℂ$
128		cncfmptc	$⊢ (m - N \in ℂ \land [0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [0, 1] ⟼ m - N) : [0, 1] \underset{cn}{⟶} ℂ$
129	124 126 127 128	syl3anc	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ m - N) : [0, 1] \underset{cn}{⟶} ℂ$
130		cncfmptid	$⊢ ([0, 1] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [0, 1] ⟼ x) : [0, 1] \underset{cn}{⟶} ℂ$
131	126 127 130	syl2anc	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ x) : [0, 1] \underset{cn}{⟶} ℂ$
132	129 131	mulcncf	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ (m - N) x) : [0, 1] \underset{cn}{⟶} ℂ$
133	132	efmul2picn	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ e^{i 2 π (m - N) x}) : [0, 1] \underset{cn}{⟶} ℂ$
134		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}$
135	121 122 133 134	syl3anc	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in [0, 1] ⟼ e^{i 2 π (m - N) x}) \in 𝐿^{1}$
136	118 119 120 135	iblss	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (x \in (0, 1) ⟼ e^{i 2 π (m - N) x}) \in 𝐿^{1}$
137	136	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}$
138	114 116 137	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}$
139	97 101 112 138	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)$
140	139	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}$
141	93 94 96 140	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)$
142	141	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$
143		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$
144		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$
145	101 114	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 ℂ$
146	145	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))$
147	145	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$
148	143 144 146 147	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)$
149		velsn	$⊢ m \in \{N\} \leftrightarrow m = N$
150	41 123	subeq0ad	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (m - N = 0 \leftrightarrow m = N)$
151	149 150	bitr4id	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to (m \in \{N\} \leftrightarrow m - N = 0)$
152	151	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)$
153	1	nn0zd	$⊢ φ \to N \in ℤ$
154	153	ad2antrr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to N \in ℤ$
155	46 154	zsubcld	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m - N \in ℤ$
156		itgexpif	$⊢ m - N \in ℤ \to \int_{(0, 1)} e^{i 2 π (m - N) x} d x = if (m - N = 0, 1, 0)$
157	155 156	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)$
158	157	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)$
159	158	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)$
160		1cnd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 1 \in ℂ$
161		0cnd	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to 0 \in ℂ$
162	160 161	ifcld	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to if (m - N = 0, 1, 0) \in ℂ$
163	101 162 114	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)$
164	159 163	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)$
165	148 152 164	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)$
166	165	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)$
167		0zd	$⊢ φ \to 0 \in ℤ$
168	10	nn0zd	$⊢ φ \to S \in ℤ$
169	168 153	zmulcld	$⊢ φ \to S \cdot N \in ℤ$
170	1	nn0ge0d	$⊢ φ \to 0 \leq N$
171		nnmulge	$⊢ (S \in ℕ \land N \in ℕ_{0}) \to N \leq S \cdot N$
172	2 1 171	syl2anc	$⊢ φ \to N \leq S \cdot N$
173	167 169 153 170 172	elfzd	$⊢ φ \to N \in (0 \dots S \cdot N)$
174	173	snssd	$⊢ φ \to \{N\} \subseteq (0 \dots S \cdot N)$
175	174	sselda	$⊢ (φ \land m \in \{N\}) \to m \in (0 \dots S \cdot N)$
176	175 145	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 ℂ$
177	176	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 ℂ$
178	94	olcd	$⊢ φ \to ((0 \dots S \cdot N) \subseteq ℤ_{\geq 0} \lor (0 \dots S \cdot N) \in Fin)$
179		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)$
180	174 177 178 179	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)$
181	29	a1i	$⊢ φ \to (1 \dots N) \subseteq ℕ$
182		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
183	181 153 10 182	reprfi	$⊢ φ \to (1 \dots N) repr (S) N \in Fin$
184	37	a1i	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to (0 ..^S) \in Fin$
185	1	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to N \in ℕ_{0}$
186	10	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to S \in ℕ_{0}$
187	22	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to N \in ℂ$
188	3	ad2antrr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
189		simpr	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
190	29	a1i	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to (1 \dots N) \subseteq ℕ$
191	153	adantr	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to N \in ℤ$
192	10	adantr	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to S \in ℕ_{0}$
193		simpr	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to c \in ((1 \dots N) repr (S) N)$
194	190 191 192 193	reprf	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to c : (0 ..^S) ⟶ (1 \dots N)$
195	194	ffvelrnda	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to c (a) \in (1 \dots N)$
196	29 195	sselid	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to c (a) \in ℕ$
197	185 186 187 188 189 196	breprexplemb	$⊢ ((φ \land c \in ((1 \dots N) repr (S) N)) \land a \in (0 ..^S)) \to L (a) (c (a)) \in ℂ$
198	184 197	fprodcl	$⊢ (φ \land c \in ((1 \dots N) repr (S) N)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
199	183 198	fsumcl	$⊢ φ \to \sum_{c \in (1 \dots N) repr (S) N} \prod_{a \in (0 ..^S)} L (a) (c (a)) \in ℂ$
200		oveq2	$⊢ m = N \to (1 \dots N) repr (S) m = (1 \dots N) repr (S) N$
201	200	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))$
202	201	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))$
203	1 199 202	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))$
204	166 180 203	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))$
205	139	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$
206	110	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 ℂ$
207	114 206 137	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$
208	207	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$
209	205 208	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$
210	209	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$
211	1 10	reprfz1	$⊢ φ \to ℕ repr (S) N = (1 \dots N) repr (S) N$
212	211	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))$
213	204 210 212	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))$
214	91 142 213	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