Metamath Proof Explorer

Theorem vtsprod

Description: Express the Vinogradov trigonometric sums to the power of S (Contributed by Thierry Arnoux, 12-Dec-2021)

Ref Expression
Hypotheses vtsval.n 
|- ( ph -> N e. NN0 )
vtsval.x 
|- ( ph -> X e. CC )
vtsprod.s 
|- ( ph -> S e. NN0 )
vtsprod.l 
|- ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
Assertion vtsprod 
|- ( ph -> prod_ a e. ( 0 ..^ S ) ( ( ( L ` a ) vts N ) ` X ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) ) ) )

Proof

Step Hyp Ref Expression
1 vtsval.n 
 |-  ( ph -> N e. NN0 )
2 vtsval.x 
 |-  ( ph -> X e. CC )
3 vtsprod.s 
 |-  ( ph -> S e. NN0 )
4 vtsprod.l 
 |-  ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
5 ax-icn 
 |-  _i e. CC
6 5 a1i 
 |-  ( ph -> _i e. CC )
7 2cnd 
 |-  ( ph -> 2 e. CC )
8 picn 
 |-  _pi e. CC
9 8 a1i 
 |-  ( ph -> _pi e. CC )
10 7 9 mulcld 
 |-  ( ph -> ( 2 x. _pi ) e. CC )
11 6 10 mulcld 
 |-  ( ph -> ( _i x. ( 2 x. _pi ) ) e. CC )
12 11 2 mulcld 
 |-  ( ph -> ( ( _i x. ( 2 x. _pi ) ) x. X ) e. CC )
13 12 efcld 
 |-  ( ph -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) e. CC )
14 1 3 13 4 breprexp 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ m ) ) )
15 1 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> N e. NN0 )
16 2 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> X e. CC )
17 4 ffvelrnda 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( L ` a ) e. ( CC ^m NN ) )
18 elmapi 
 |-  ( ( L ` a ) e. ( CC ^m NN ) -> ( L ` a ) : NN --> CC )
19 17 18 syl 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( L ` a ) : NN --> CC )
20 15 16 19 vtsval 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( ( ( L ` a ) vts N ) ` X ) = sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( b x. X ) ) ) ) )
21 fzssz 
 |-  ( 1 ... N ) C_ ZZ
22 simpr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> b e. ( 1 ... N ) )
23 21 22 sseldi 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> b e. ZZ )
24 23 zcnd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> b e. CC )
25 11 ad2antrr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
26 16 adantr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> X e. CC )
27 24 25 26 mul12d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( b x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) = ( ( _i x. ( 2 x. _pi ) ) x. ( b x. X ) ) )
28 27 fveq2d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( exp ` ( b x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( b x. X ) ) ) )
29 12 ad2antrr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. X ) e. CC )
30 efexp 
 |-  ( ( ( ( _i x. ( 2 x. _pi ) ) x. X ) e. CC /\ b e. ZZ ) -> ( exp ` ( b x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) )
31 29 23 30 syl2anc 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( exp ` ( b x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) )
32 28 31 eqtr3d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( b x. X ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) )
33 32 oveq2d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ S ) ) /\ b e. ( 1 ... N ) ) -> ( ( ( L ` a ) ` b ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( b x. X ) ) ) ) = ( ( ( L ` a ) ` b ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) ) )
34 33 sumeq2dv 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( b x. X ) ) ) ) = sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) ) )
35 20 34 eqtrd 
 |-  ( ( ph /\ a e. ( 0 ..^ S ) ) -> ( ( ( L ` a ) vts N ) ` X ) = sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) ) )
36 35 prodeq2dv 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) ( ( ( L ` a ) vts N ) ` X ) = prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ b ) ) )
37 fzssz 
 |-  ( 0 ... ( S x. N ) ) C_ ZZ
38 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ( 0 ... ( S x. N ) ) )
39 37 38 sseldi 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ZZ )
40 39 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> m e. ZZ )
41 40 zcnd 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> m e. CC )
42 11 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
43 2 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> X e. CC )
44 41 42 43 mul12d 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( m x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) = ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) )
45 44 fveq2d 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( exp ` ( m x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) ) )
46 12 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. X ) e. CC )
47 efexp 
 |-  ( ( ( ( _i x. ( 2 x. _pi ) ) x. X ) e. CC /\ m e. ZZ ) -> ( exp ` ( m x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ m ) )
48 46 40 47 syl2anc 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( exp ` ( m x. ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ m ) )
49 45 48 eqtr3d 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ m ) )
50 49 oveq2d 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ m ) ) )
51 50 sumeq2dv 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ m ) ) )
52 51 sumeq2dv 
 |-  ( ph -> sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. X ) ) ^ m ) ) )
53 14 36 52 3eqtr4d 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) ( ( ( L ` a ) vts N ) ` X ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. X ) ) ) ) )