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	\|- ( ph -> N e. NN0 )
	Assertion	circlevma	\|- ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = S. ( 0 (,) 1 ) ( ( ( ( Lam vts N ) ` x ) ^ 3 ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )

Proof

Step	Hyp	Ref	Expression
1		circlevma.n	\|- ( ph -> N e. NN0 )
2		3nn	\|- 3 e. NN
3	2	a1i	\|- ( ph -> 3 e. NN )
4		vmaf	\|- Lam : NN --> RR
5		ax-resscn	\|- RR C_ CC
6		fss	\|- ( ( Lam : NN --> RR /\ RR C_ CC ) -> Lam : NN --> CC )
7	4 5 6	mp2an	\|- Lam : NN --> CC
8		cnex	\|- CC e. _V
9		nnex	\|- NN e. _V
10		elmapg	\|- ( ( CC e. _V /\ NN e. _V ) -> ( Lam e. ( CC ^m NN ) <-> Lam : NN --> CC ) )
11	8 9 10	mp2an	\|- ( Lam e. ( CC ^m NN ) <-> Lam : NN --> CC )
12	7 11	mpbir	\|- Lam e. ( CC ^m NN )
13	12	fconst6	\|- ( ( 0 ..^ 3 ) X. { Lam } ) : ( 0 ..^ 3 ) --> ( CC ^m NN )
14	13	a1i	\|- ( ph -> ( ( 0 ..^ 3 ) X. { Lam } ) : ( 0 ..^ 3 ) --> ( CC ^m NN ) )
15	1 3 14	circlemeth	\|- ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) prod_ a e. ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
16		c0ex	\|- 0 e. _V
17	16	tpid1	\|- 0 e. { 0 , 1 , 2 }
18		fzo0to3tp	\|- ( 0 ..^ 3 ) = { 0 , 1 , 2 }
19	17 18	eleqtrri	\|- 0 e. ( 0 ..^ 3 )
20		eleq1	\|- ( a = 0 -> ( a e. ( 0 ..^ 3 ) <-> 0 e. ( 0 ..^ 3 ) ) )
21	19 20	mpbiri	\|- ( a = 0 -> a e. ( 0 ..^ 3 ) )
22	12	elexi	\|- Lam e. _V
23	22	fvconst2	\|- ( a e. ( 0 ..^ 3 ) -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
24	21 23	syl	\|- ( a = 0 -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
25		fveq2	\|- ( a = 0 -> ( n ` a ) = ( n ` 0 ) )
26	24 25	fveq12d	\|- ( a = 0 -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` 0 ) ) )
27		1ex	\|- 1 e. _V
28	27	tpid2	\|- 1 e. { 0 , 1 , 2 }
29	28 18	eleqtrri	\|- 1 e. ( 0 ..^ 3 )
30		eleq1	\|- ( a = 1 -> ( a e. ( 0 ..^ 3 ) <-> 1 e. ( 0 ..^ 3 ) ) )
31	29 30	mpbiri	\|- ( a = 1 -> a e. ( 0 ..^ 3 ) )
32	31 23	syl	\|- ( a = 1 -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
33		fveq2	\|- ( a = 1 -> ( n ` a ) = ( n ` 1 ) )
34	32 33	fveq12d	\|- ( a = 1 -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` 1 ) ) )
35		2ex	\|- 2 e. _V
36	35	tpid3	\|- 2 e. { 0 , 1 , 2 }
37	36 18	eleqtrri	\|- 2 e. ( 0 ..^ 3 )
38		eleq1	\|- ( a = 2 -> ( a e. ( 0 ..^ 3 ) <-> 2 e. ( 0 ..^ 3 ) ) )
39	37 38	mpbiri	\|- ( a = 2 -> a e. ( 0 ..^ 3 ) )
40	39 23	syl	\|- ( a = 2 -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
41		fveq2	\|- ( a = 2 -> ( n ` a ) = ( n ` 2 ) )
42	40 41	fveq12d	\|- ( a = 2 -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` 2 ) ) )
43	23	fveq1d	\|- ( a e. ( 0 ..^ 3 ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` a ) ) )
44	43	adantl	\|- ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` a ) ) )
45	7	a1i	\|- ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> Lam : NN --> CC )
46		ssidd	\|- ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> NN C_ NN )
47	1	nn0zd	\|- ( ph -> N e. ZZ )
48	47	adantr	\|- ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> N e. ZZ )
49	2	nnnn0i	\|- 3 e. NN0
50	49	a1i	\|- ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 3 e. NN0 )
51		simpr	\|- ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n e. ( NN ( repr ` 3 ) N ) )
52	46 48 50 51	reprf	\|- ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n : ( 0 ..^ 3 ) --> NN )
53	52	ffvelcdmda	\|- ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( n ` a ) e. NN )
54	45 53	ffvelcdmd	\|- ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( Lam ` ( n ` a ) ) e. CC )
55	44 54	eqeltrd	\|- ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) e. CC )
56	26 34 42 55	prodfzo03	\|- ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
57	56	sumeq2dv	\|- ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) prod_ a e. ( 0 ..^ 3 ) ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = sum_ n e. ( NN ( repr ` 3 ) N ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
58	23	adantl	\|- ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
59	58	oveq1d	\|- ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) = ( Lam vts N ) )
60	59	fveq1d	\|- ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) = ( ( Lam vts N ) ` x ) )
61	60	prodeq2dv	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) = prod_ a e. ( 0 ..^ 3 ) ( ( Lam vts N ) ` x ) )
62		fzofi	\|- ( 0 ..^ 3 ) e. Fin
63	62	a1i	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 0 ..^ 3 ) e. Fin )
64	1	adantr	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> N e. NN0 )
65		ioossre	\|- ( 0 (,) 1 ) C_ RR
66	65 5	sstri	\|- ( 0 (,) 1 ) C_ CC
67	66	a1i	\|- ( ph -> ( 0 (,) 1 ) C_ CC )
68	67	sselda	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> x e. CC )
69	7	a1i	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> Lam : NN --> CC )
70	64 68 69	vtscl	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( Lam vts N ) ` x ) e. CC )
71		fprodconst	\|- ( ( ( 0 ..^ 3 ) e. Fin /\ ( ( Lam vts N ) ` x ) e. CC ) -> prod_ a e. ( 0 ..^ 3 ) ( ( Lam vts N ) ` x ) = ( ( ( Lam vts N ) ` x ) ^ ( # ` ( 0 ..^ 3 ) ) ) )
72	63 70 71	syl2anc	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( Lam vts N ) ` x ) = ( ( ( Lam vts N ) ` x ) ^ ( # ` ( 0 ..^ 3 ) ) ) )
73		hashfzo0	\|- ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
74	49 73	ax-mp	\|- ( # ` ( 0 ..^ 3 ) ) = 3
75	74	a1i	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( # ` ( 0 ..^ 3 ) ) = 3 )
76	75	oveq2d	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( Lam vts N ) ` x ) ^ ( # ` ( 0 ..^ 3 ) ) ) = ( ( ( Lam vts N ) ` x ) ^ 3 ) )
77	61 72 76	3eqtrd	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) = ( ( ( Lam vts N ) ` x ) ^ 3 ) )
78	77	oveq1d	\|- ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( prod_ a e. ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( ( ( ( Lam vts N ) ` x ) ^ 3 ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
79	78	itgeq2dv	\|- ( ph -> S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x = S. ( 0 (,) 1 ) ( ( ( ( Lam vts N ) ` x ) ^ 3 ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
80	15 57 79	3eqtr3d	\|- ( ph -> sum_ n e. ( NN ( repr ` 3 ) N ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = S. ( 0 (,) 1 ) ( ( ( ( Lam vts N ) ` x ) ^ 3 ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )

Metamath Proof Explorer

Theorem circlevma

Proof