Metamath Proof Explorer

Theorem 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 ffvelrnda 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( n ` a ) e. NN )
54 45 53 ffvelrnd 
 |-  ( ( ( 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 )