Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-vts Structured version   Visualization version   GIF version

Definition df-vts 33648
Description: Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021.)
Assertion
Ref Expression
df-vts vts = (๐‘™ โˆˆ (โ„‚ โ†‘m โ„•), ๐‘› โˆˆ โ„•0 โ†ฆ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ๐‘Ž โˆˆ (1...๐‘›)((๐‘™โ€˜๐‘Ž) ยท (expโ€˜((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ))))))
Distinct variable group:   ๐‘Ž,๐‘™,๐‘›,๐‘ฅ

Detailed syntax breakdown of Definition df-vts
StepHypRef Expression
1 cvts 33647 . 2 class vts
2 vl . . 3 setvar ๐‘™
3 vn . . 3 setvar ๐‘›
4 cc 11108 . . . 4 class โ„‚
5 cn 12212 . . . 4 class โ„•
6 cmap 8820 . . . 4 class โ†‘m
74, 5, 6co 7409 . . 3 class (โ„‚ โ†‘m โ„•)
8 cn0 12472 . . 3 class โ„•0
9 vx . . . 4 setvar ๐‘ฅ
10 c1 11111 . . . . . 6 class 1
113cv 1541 . . . . . 6 class ๐‘›
12 cfz 13484 . . . . . 6 class ...
1310, 11, 12co 7409 . . . . 5 class (1...๐‘›)
14 va . . . . . . . 8 setvar ๐‘Ž
1514cv 1541 . . . . . . 7 class ๐‘Ž
162cv 1541 . . . . . . 7 class ๐‘™
1715, 16cfv 6544 . . . . . 6 class (๐‘™โ€˜๐‘Ž)
18 ci 11112 . . . . . . . . 9 class i
19 c2 12267 . . . . . . . . . 10 class 2
20 cpi 16010 . . . . . . . . . 10 class ฯ€
21 cmul 11115 . . . . . . . . . 10 class ยท
2219, 20, 21co 7409 . . . . . . . . 9 class (2 ยท ฯ€)
2318, 22, 21co 7409 . . . . . . . 8 class (i ยท (2 ยท ฯ€))
249cv 1541 . . . . . . . . 9 class ๐‘ฅ
2515, 24, 21co 7409 . . . . . . . 8 class (๐‘Ž ยท ๐‘ฅ)
2623, 25, 21co 7409 . . . . . . 7 class ((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ))
27 ce 16005 . . . . . . 7 class exp
2826, 27cfv 6544 . . . . . 6 class (expโ€˜((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ)))
2917, 28, 21co 7409 . . . . 5 class ((๐‘™โ€˜๐‘Ž) ยท (expโ€˜((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ))))
3013, 29, 14csu 15632 . . . 4 class ฮฃ๐‘Ž โˆˆ (1...๐‘›)((๐‘™โ€˜๐‘Ž) ยท (expโ€˜((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ))))
319, 4, 30cmpt 5232 . . 3 class (๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ๐‘Ž โˆˆ (1...๐‘›)((๐‘™โ€˜๐‘Ž) ยท (expโ€˜((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ)))))
322, 3, 7, 8, 31cmpo 7411 . 2 class (๐‘™ โˆˆ (โ„‚ โ†‘m โ„•), ๐‘› โˆˆ โ„•0 โ†ฆ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ๐‘Ž โˆˆ (1...๐‘›)((๐‘™โ€˜๐‘Ž) ยท (expโ€˜((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ))))))
331, 32wceq 1542 1 wff vts = (๐‘™ โˆˆ (โ„‚ โ†‘m โ„•), ๐‘› โˆˆ โ„•0 โ†ฆ (๐‘ฅ โˆˆ โ„‚ โ†ฆ ฮฃ๐‘Ž โˆˆ (1...๐‘›)((๐‘™โ€˜๐‘Ž) ยท (expโ€˜((i ยท (2 ยท ฯ€)) ยท (๐‘Ž ยท ๐‘ฅ))))))
Colors of variables: wff setvar class
This definition is referenced by:  vtsval  33649
  Copyright terms: Public domain W3C validator