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 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
28 27 18 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
29 eleq1 
 |-  ( a = 1 -> ( a e. ( 0 ..^ 3 ) <-> 1 e. ( 0 ..^ 3 ) ) )
30 28 29 mpbiri 
 |-  ( a = 1 -> a e. ( 0 ..^ 3 ) )
31 30 23 syl 
 |-  ( a = 1 -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
32 fveq2 
 |-  ( a = 1 -> ( n ` a ) = ( n ` 1 ) )
33 31 32 fveq12d 
 |-  ( a = 1 -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` 1 ) ) )
34 2ex 
 |-  2 e. _V
35 34 tpid3 
 |-  2 e. { 0 , 1 , 2 }
36 35 18 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
37 eleq1 
 |-  ( a = 2 -> ( a e. ( 0 ..^ 3 ) <-> 2 e. ( 0 ..^ 3 ) ) )
38 36 37 mpbiri 
 |-  ( a = 2 -> a e. ( 0 ..^ 3 ) )
39 38 23 syl 
 |-  ( a = 2 -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
40 fveq2 
 |-  ( a = 2 -> ( n ` a ) = ( n ` 2 ) )
41 39 40 fveq12d 
 |-  ( a = 2 -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` 2 ) ) )
42 23 fveq1d 
 |-  ( a e. ( 0 ..^ 3 ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` a ) ) )
43 42 adantl 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) = ( Lam ` ( n ` a ) ) )
44 7 a1i 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> Lam : NN --> CC )
45 ssidd 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> NN C_ NN )
46 1 nn0zd 
 |-  ( ph -> N e. ZZ )
47 46 adantr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> N e. ZZ )
48 2 nnnn0i 
 |-  3 e. NN0
49 48 a1i 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> 3 e. NN0 )
50 simpr 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n e. ( NN ( repr ` 3 ) N ) )
51 45 47 49 50 reprf 
 |-  ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) -> n : ( 0 ..^ 3 ) --> NN )
52 51 ffvelcdmda 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( n ` a ) e. NN )
53 44 52 ffvelcdmd 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( Lam ` ( n ` a ) ) e. CC )
54 43 53 eqeltrd 
 |-  ( ( ( ph /\ n e. ( NN ( repr ` 3 ) N ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) ` ( n ` a ) ) e. CC )
55 26 33 41 54 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 ) ) ) ) )
56 55 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 ) ) ) ) )
57 23 adantl 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) = Lam )
58 57 oveq1d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) = ( Lam vts N ) )
59 58 fveq1d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ 3 ) ) -> ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) = ( ( Lam vts N ) ` x ) )
60 59 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 ) )
61 fzofi 
 |-  ( 0 ..^ 3 ) e. Fin
62 61 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 0 ..^ 3 ) e. Fin )
63 1 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> N e. NN0 )
64 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
65 64 5 sstri 
 |-  ( 0 (,) 1 ) C_ CC
66 65 a1i 
 |-  ( ph -> ( 0 (,) 1 ) C_ CC )
67 66 sselda 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> x e. CC )
68 7 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> Lam : NN --> CC )
69 63 67 68 vtscl 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( Lam vts N ) ` x ) e. CC )
70 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 ) ) ) )
71 62 69 70 syl2anc 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( Lam vts N ) ` x ) = ( ( ( Lam vts N ) ` x ) ^ ( # ` ( 0 ..^ 3 ) ) ) )
72 hashfzo0 
 |-  ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
73 48 72 ax-mp 
 |-  ( # ` ( 0 ..^ 3 ) ) = 3
74 73 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( # ` ( 0 ..^ 3 ) ) = 3 )
75 74 oveq2d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( ( Lam vts N ) ` x ) ^ ( # ` ( 0 ..^ 3 ) ) ) = ( ( ( Lam vts N ) ` x ) ^ 3 ) )
76 60 71 75 3eqtrd 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ 3 ) ( ( ( ( ( 0 ..^ 3 ) X. { Lam } ) ` a ) vts N ) ` x ) = ( ( ( Lam vts N ) ` x ) ^ 3 ) )
77 76 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 ) ) ) ) )
78 77 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 )
79 15 56 78 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 )