Description: Value of the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vtsval.n | |
|
vtsval.x | |
||
vtsval.l | |
||
Assertion | vtsval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtsval.n | |
|
2 | vtsval.x | |
|
3 | vtsval.l | |
|
4 | cnex | |
|
5 | nnex | |
|
6 | 4 5 | elmap | |
7 | 3 6 | sylibr | |
8 | fveq1 | |
|
9 | 8 | oveq1d | |
10 | 9 | sumeq2sdv | |
11 | 10 | mpteq2dv | |
12 | oveq2 | |
|
13 | 12 | sumeq1d | |
14 | 13 | mpteq2dv | |
15 | df-vts | |
|
16 | 4 | mptex | |
17 | 11 14 15 16 | ovmpo | |
18 | 7 1 17 | syl2anc | |
19 | oveq2 | |
|
20 | 19 | oveq2d | |
21 | 20 | fveq2d | |
22 | 21 | oveq2d | |
23 | 22 | sumeq2sdv | |
24 | 23 | adantl | |
25 | sumex | |
|
26 | 25 | a1i | |
27 | 18 24 2 26 | fvmptd | |