Metamath Proof Explorer


Theorem vtsval

Description: Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Hypotheses vtsval.n φN0
vtsval.x φX
vtsval.l φL:
Assertion vtsval φLvtsNX=a=1NLaei2πaX

Proof

Step Hyp Ref Expression
1 vtsval.n φN0
2 vtsval.x φX
3 vtsval.l φL:
4 cnex V
5 nnex V
6 4 5 elmap LL:
7 3 6 sylibr φL
8 fveq1 l=Lla=La
9 8 oveq1d l=Llaei2πax=Laei2πax
10 9 sumeq2sdv l=La=1nlaei2πax=a=1nLaei2πax
11 10 mpteq2dv l=Lxa=1nlaei2πax=xa=1nLaei2πax
12 oveq2 n=N1n=1N
13 12 sumeq1d n=Na=1nLaei2πax=a=1NLaei2πax
14 13 mpteq2dv n=Nxa=1nLaei2πax=xa=1NLaei2πax
15 df-vts vts=l,n0xa=1nlaei2πax
16 4 mptex xa=1NLaei2πaxV
17 11 14 15 16 ovmpo LN0LvtsN=xa=1NLaei2πax
18 7 1 17 syl2anc φLvtsN=xa=1NLaei2πax
19 oveq2 x=Xax=aX
20 19 oveq2d x=Xi2πax=i2πaX
21 20 fveq2d x=Xei2πax=ei2πaX
22 21 oveq2d x=XLaei2πax=Laei2πaX
23 22 sumeq2sdv x=Xa=1NLaei2πax=a=1NLaei2πaX
24 23 adantl φx=Xa=1NLaei2πax=a=1NLaei2πaX
25 sumex a=1NLaei2πaXV
26 25 a1i φa=1NLaei2πaXV
27 18 24 2 26 fvmptd φLvtsNX=a=1NLaei2πaX