This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtscl

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

Ref Expression
Hypotheses vtsval.n 
|- ( ph -> N e. NN0 )
vtsval.x 
|- ( ph -> X e. CC )
vtsval.l 
|- ( ph -> L : NN --> CC )
Assertion vtscl 
|- ( ph -> ( ( L vts N ) ` X ) e. CC )

Proof

Step Hyp Ref Expression
1 vtsval.n 
 |-  ( ph -> N e. NN0 )
2 vtsval.x 
 |-  ( ph -> X e. CC )
3 vtsval.l 
 |-  ( ph -> L : NN --> CC )
4 1 2 3 vtsval 
 |-  ( ph -> ( ( L vts N ) ` X ) = sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) )
5 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
6 3 adantr 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> L : NN --> CC )
7 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
8 7 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
9 8 sselda 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> a e. NN )
10 6 9 ffvelcdmd 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> ( L ` a ) e. CC )
11 ax-icn 
 |-  _i e. CC
12 2cn 
 |-  2 e. CC
13 picn 
 |-  _pi e. CC
14 12 13 mulcli 
 |-  ( 2 x. _pi ) e. CC
15 11 14 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
16 15 a1i 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
17 9 nncnd 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> a e. CC )
18 2 adantr 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> X e. CC )
19 17 18 mulcld 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> ( a x. X ) e. CC )
20 16 19 mulcld 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) e. CC )
21 20 efcld 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) e. CC )
22 10 21 mulcld 
 |-  ( ( ph /\ a e. ( 1 ... N ) ) -> ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) e. CC )
23 5 22 fsumcl 
 |-  ( ph -> sum_ a e. ( 1 ... N ) ( ( L ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. X ) ) ) ) e. CC )
24 4 23 eqeltrd 
 |-  ( ph -> ( ( L vts N ) ` X ) e. CC )