Metamath Proof Explorer


Definition df-vts

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

Ref Expression
Assertion df-vts vts = ( ๐‘™ โˆˆ ( โ„‚ โ†‘m โ„• ) , ๐‘› โˆˆ โ„•0 โ†ฆ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘Ž โˆˆ ( 1 ... ๐‘› ) ( ( ๐‘™ โ€˜ ๐‘Ž ) ยท ( exp โ€˜ ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvts โŠข vts
1 vl โŠข ๐‘™
2 cc โŠข โ„‚
3 cmap โŠข โ†‘m
4 cn โŠข โ„•
5 2 4 3 co โŠข ( โ„‚ โ†‘m โ„• )
6 vn โŠข ๐‘›
7 cn0 โŠข โ„•0
8 vx โŠข ๐‘ฅ
9 va โŠข ๐‘Ž
10 c1 โŠข 1
11 cfz โŠข ...
12 6 cv โŠข ๐‘›
13 10 12 11 co โŠข ( 1 ... ๐‘› )
14 1 cv โŠข ๐‘™
15 9 cv โŠข ๐‘Ž
16 15 14 cfv โŠข ( ๐‘™ โ€˜ ๐‘Ž )
17 cmul โŠข ยท
18 ce โŠข exp
19 ci โŠข i
20 c2 โŠข 2
21 cpi โŠข ฯ€
22 20 21 17 co โŠข ( 2 ยท ฯ€ )
23 19 22 17 co โŠข ( i ยท ( 2 ยท ฯ€ ) )
24 8 cv โŠข ๐‘ฅ
25 15 24 17 co โŠข ( ๐‘Ž ยท ๐‘ฅ )
26 23 25 17 co โŠข ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) )
27 26 18 cfv โŠข ( exp โ€˜ ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) ) )
28 16 27 17 co โŠข ( ( ๐‘™ โ€˜ ๐‘Ž ) ยท ( exp โ€˜ ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) ) ) )
29 13 28 9 csu โŠข ฮฃ ๐‘Ž โˆˆ ( 1 ... ๐‘› ) ( ( ๐‘™ โ€˜ ๐‘Ž ) ยท ( exp โ€˜ ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) ) ) )
30 8 2 29 cmpt โŠข ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘Ž โˆˆ ( 1 ... ๐‘› ) ( ( ๐‘™ โ€˜ ๐‘Ž ) ยท ( exp โ€˜ ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) ) ) ) )
31 1 6 5 7 30 cmpo โŠข ( ๐‘™ โˆˆ ( โ„‚ โ†‘m โ„• ) , ๐‘› โˆˆ โ„•0 โ†ฆ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘Ž โˆˆ ( 1 ... ๐‘› ) ( ( ๐‘™ โ€˜ ๐‘Ž ) ยท ( exp โ€˜ ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) ) ) ) ) )
32 0 31 wceq โŠข vts = ( ๐‘™ โˆˆ ( โ„‚ โ†‘m โ„• ) , ๐‘› โˆˆ โ„•0 โ†ฆ ( ๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘Ž โˆˆ ( 1 ... ๐‘› ) ( ( ๐‘™ โ€˜ ๐‘Ž ) ยท ( exp โ€˜ ( ( i ยท ( 2 ยท ฯ€ ) ) ยท ( ๐‘Ž ยท ๐‘ฅ ) ) ) ) ) )