circlevma

Description: The Circle Method, where the Vinogradov sums are weighted using the von Mangoldt function, as it appears as proposition 1.1 of Helfgott p. 5. (Contributed by Thierry Arnoux, 13-Dec-2021)

		Ref	Expression
	Hypothesis	circlevma.n	$⊢ φ \to N \in ℕ_{0}$
	Assertion	circlevma	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) Λ (n (1)) Λ (n (2)) = \int_{(0, 1)} {(Λ vts N) (x)}^{3} e^{i 2 π -N x} d x$

Proof

Step	Hyp	Ref	Expression
1		circlevma.n	$⊢ φ \to N \in ℕ_{0}$
2		3nn	$⊢ 3 \in ℕ$
3	2	a1i	$⊢ φ \to 3 \in ℕ$
4		vmaf	$⊢ Λ : ℕ ⟶ ℝ$
5		ax-resscn	$⊢ ℝ \subseteq ℂ$
6		fss	$⊢ (Λ : ℕ ⟶ ℝ \land ℝ \subseteq ℂ) \to Λ : ℕ ⟶ ℂ$
7	4 5 6	mp2an	$⊢ Λ : ℕ ⟶ ℂ$
8		cnex	$⊢ ℂ \in V$
9		nnex	$⊢ ℕ \in V$
10		elmapg	$⊢ (ℂ \in V \land ℕ \in V) \to (Λ \in (ℂ^{ℕ}) \leftrightarrow Λ : ℕ ⟶ ℂ)$
11	8 9 10	mp2an	$⊢ Λ \in (ℂ^{ℕ}) \leftrightarrow Λ : ℕ ⟶ ℂ$
12	7 11	mpbir	$⊢ Λ \in (ℂ^{ℕ})$
13	12	fconst6	$⊢ ((0 ..^3) \times \{Λ\}) : (0 ..^3) ⟶ ℂ^{ℕ}$
14	13	a1i	$⊢ φ \to ((0 ..^3) \times \{Λ\}) : (0 ..^3) ⟶ ℂ^{ℕ}$
15	1 3 14	circlemeth	$⊢ φ \to \sum_{n \in ℕ repr (3) N} \prod_{a \in (0 ..^3)} ((0 ..^3) \times \{Λ\}) (a) (n (a)) = \int_{(0, 1)} \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) e^{i 2 π -N x} d x$
16		c0ex	$⊢ 0 \in V$
17	16	tpid1	$⊢ 0 \in \{0, 1, 2\}$
18		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
19	17 18	eleqtrri	$⊢ 0 \in (0 ..^3)$
20		eleq1	$⊢ a = 0 \to (a \in (0 ..^3) \leftrightarrow 0 \in (0 ..^3))$
21	19 20	mpbiri	$⊢ a = 0 \to a \in (0 ..^3)$
22	12	elexi	$⊢ Λ \in V$
23	22	fvconst2	$⊢ a \in (0 ..^3) \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
24	21 23	syl	$⊢ a = 0 \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
25		fveq2	$⊢ a = 0 \to n (a) = n (0)$
26	24 25	fveq12d	$⊢ a = 0 \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (0))$
27		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
28	27 18	eleqtrri	$⊢ 1 \in (0 ..^3)$
29		eleq1	$⊢ a = 1 \to (a \in (0 ..^3) \leftrightarrow 1 \in (0 ..^3))$
30	28 29	mpbiri	$⊢ a = 1 \to a \in (0 ..^3)$
31	30 23	syl	$⊢ a = 1 \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
32		fveq2	$⊢ a = 1 \to n (a) = n (1)$
33	31 32	fveq12d	$⊢ a = 1 \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (1))$
34		2ex	$⊢ 2 \in V$
35	34	tpid3	$⊢ 2 \in \{0, 1, 2\}$
36	35 18	eleqtrri	$⊢ 2 \in (0 ..^3)$
37		eleq1	$⊢ a = 2 \to (a \in (0 ..^3) \leftrightarrow 2 \in (0 ..^3))$
38	36 37	mpbiri	$⊢ a = 2 \to a \in (0 ..^3)$
39	38 23	syl	$⊢ a = 2 \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
40		fveq2	$⊢ a = 2 \to n (a) = n (2)$
41	39 40	fveq12d	$⊢ a = 2 \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (2))$
42	23	fveq1d	$⊢ a \in (0 ..^3) \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (a))$
43	42	adantl	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (a))$
44	7	a1i	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to Λ : ℕ ⟶ ℂ$
45		ssidd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to ℕ \subseteq ℕ$
46	1	nn0zd	$⊢ φ \to N \in ℤ$
47	46	adantr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to N \in ℤ$
48	2	nnnn0i	$⊢ 3 \in ℕ_{0}$
49	48	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 3 \in ℕ_{0}$
50		simpr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n \in (ℕ repr (3) N)$
51	45 47 49 50	reprf	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n : (0 ..^3) ⟶ ℕ$
52	51	ffvelcdmda	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to n (a) \in ℕ$
53	44 52	ffvelcdmd	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to Λ (n (a)) \in ℂ$
54	43 53	eqeltrd	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) \in ℂ$
55	26 33 41 54	prodfzo03	$⊢ (φ \land n \in (ℕ repr (3) N)) \to \prod_{a \in (0 ..^3)} ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (0)) Λ (n (1)) Λ (n (2))$
56	55	sumeq2dv	$⊢ φ \to \sum_{n \in ℕ repr (3) N} \prod_{a \in (0 ..^3)} ((0 ..^3) \times \{Λ\}) (a) (n (a)) = \sum_{n \in ℕ repr (3) N} Λ (n (0)) Λ (n (1)) Λ (n (2))$
57	23	adantl	$⊢ ((φ \land x \in (0, 1)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
58	57	oveq1d	$⊢ ((φ \land x \in (0, 1)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) vts N = Λ vts N$
59	58	fveq1d	$⊢ ((φ \land x \in (0, 1)) \land a \in (0 ..^3)) \to (((0 ..^3) \times \{Λ\}) (a) vts N) (x) = (Λ vts N) (x)$
60	59	prodeq2dv	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) = \prod_{a \in (0 ..^3)} (Λ vts N) (x)$
61		fzofi	$⊢ (0 ..^3) \in Fin$
62	61	a1i	$⊢ (φ \land x \in (0, 1)) \to (0 ..^3) \in Fin$
63	1	adantr	$⊢ (φ \land x \in (0, 1)) \to N \in ℕ_{0}$
64		ioossre	$⊢ (0, 1) \subseteq ℝ$
65	64 5	sstri	$⊢ (0, 1) \subseteq ℂ$
66	65	a1i	$⊢ φ \to (0, 1) \subseteq ℂ$
67	66	sselda	$⊢ (φ \land x \in (0, 1)) \to x \in ℂ$
68	7	a1i	$⊢ (φ \land x \in (0, 1)) \to Λ : ℕ ⟶ ℂ$
69	63 67 68	vtscl	$⊢ (φ \land x \in (0, 1)) \to (Λ vts N) (x) \in ℂ$
70		fprodconst	$⊢ ((0 ..^3) \in Fin \land (Λ vts N) (x) \in ℂ) \to \prod_{a \in (0 ..^3)} (Λ vts N) (x) = {(Λ vts N) (x)}^{\|(0 ..^3)\|}$
71	62 69 70	syl2anc	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (Λ vts N) (x) = {(Λ vts N) (x)}^{\|(0 ..^3)\|}$
72		hashfzo0	$⊢ 3 \in ℕ_{0} \to \|(0 ..^3)\| = 3$
73	48 72	ax-mp	$⊢ \|(0 ..^3)\| = 3$
74	73	a1i	$⊢ (φ \land x \in (0, 1)) \to \|(0 ..^3)\| = 3$
75	74	oveq2d	$⊢ (φ \land x \in (0, 1)) \to {(Λ vts N) (x)}^{\|(0 ..^3)\|} = {(Λ vts N) (x)}^{3}$
76	60 71 75	3eqtrd	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) = {(Λ vts N) (x)}^{3}$
77	76	oveq1d	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) e^{i 2 π -N x} = {(Λ vts N) (x)}^{3} e^{i 2 π -N x}$
78	77	itgeq2dv	$⊢ φ \to \int_{(0, 1)} \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) e^{i 2 π -N x} d x = \int_{(0, 1)} {(Λ vts N) (x)}^{3} e^{i 2 π -N x} d x$
79	15 56 78	3eqtr3d	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) Λ (n (1)) Λ (n (2)) = \int_{(0, 1)} {(Λ vts N) (x)}^{3} e^{i 2 π -N x} d x$

Metamath Proof Explorer

Theorem circlevma

Proof