Metamath Proof Explorer

Theorem circlemeth

Description: The Hardy, Littlewood and Ramanujan Circle Method, in a generic form, with different weighting / smoothing functions. (Contributed by Thierry Arnoux, 13-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 circlemeth.n 
 |-  ( ph -> N e. NN0 )
2 circlemeth.s 
 |-  ( ph -> S e. NN )
3 circlemeth.l 
 |-  ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
4 1 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> N e. NN0 )
5 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
6 ax-resscn 
 |-  RR C_ CC
7 5 6 sstri 
 |-  ( 0 (,) 1 ) C_ CC
8 7 a1i 
 |-  ( ph -> ( 0 (,) 1 ) C_ CC )
9 8 sselda 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> x e. CC )
10 2 nnnn0d 
 |-  ( ph -> S e. NN0 )
11 10 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> S e. NN0 )
12 3 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
13 4 9 11 12 vtsprod 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> 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 ) ) ) ) )
14 13 oveq1d 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( ( L ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N 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. ( m x. x ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
15 fzfid 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 0 ... ( S x. N ) ) e. Fin )
16 ax-icn 
 |-  _i e. CC
17 2cn 
 |-  2 e. CC
18 picn 
 |-  _pi e. CC
19 17 18 mulcli 
 |-  ( 2 x. _pi ) e. CC
20 16 19 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
21 20 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
22 1 nn0cnd 
 |-  ( ph -> N e. CC )
23 22 negcld 
 |-  ( ph -> -u N e. CC )
24 23 ralrimivw 
 |-  ( ph -> A. x e. ( 0 (,) 1 ) -u N e. CC )
25 24 r19.21bi 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> -u N e. CC )
26 25 9 mulcld 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( -u N x. x ) e. CC )
27 21 26 mulcld 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) e. CC )
28 27 efcld 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) e. CC )
29 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
30 29 a1i 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) C_ NN )
31 fzssz 
 |-  ( 0 ... ( S x. N ) ) C_ ZZ
32 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ( 0 ... ( S x. N ) ) )
33 31 32 sseldi 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ZZ )
34 33 adantlr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ZZ )
35 11 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> S e. NN0 )
36 fzfid 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) e. Fin )
37 30 34 35 36 reprfi 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( 1 ... N ) ( repr ` S ) m ) e. Fin )
38 fzofi 
 |-  ( 0 ..^ S ) e. Fin
39 38 a1i 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 0 ..^ S ) e. Fin )
40 1 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> N e. NN0 )
41 10 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> S e. NN0 )
42 33 zcnd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. CC )
43 42 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> m e. CC )
44 3 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
45 simpr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
46 29 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 1 ... N ) C_ NN )
47 33 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> m e. ZZ )
48 10 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> S e. NN0 )
49 simpr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> c e. ( ( 1 ... N ) ( repr ` S ) m ) )
50 46 47 48 49 reprf 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> c : ( 0 ..^ S ) --> ( 1 ... N ) )
51 50 ffvelrnda 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. ( 1 ... N ) )
52 29 51 sseldi 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN )
53 40 41 43 44 45 52 breprexplemb 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( c ` a ) ) e. CC )
54 53 adantl3r 
 |-  ( ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( c ` a ) ) e. CC )
55 39 54 fprodcl 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
56 20 a1i 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
57 34 zcnd 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. CC )
58 9 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> x e. CC )
59 57 58 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m x. x ) e. CC )
60 56 59 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) e. CC )
61 60 efcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) e. CC )
62 61 adantr 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) e. CC )
63 55 62 mulcld 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) ) e. CC )
64 37 63 fsumcl 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) ) e. CC )
65 15 28 64 fsummulc1 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( 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 ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N 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. ( m x. x ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
66 28 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) e. CC )
67 37 66 63 fsummulc1 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N 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. ( m x. x ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
68 66 adantr 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) e. CC )
69 55 62 68 mulassd 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) ) )
70 27 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) e. CC )
71 efadd 
 |-  ( ( ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) e. CC /\ ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) e. CC ) -> ( exp ` ( ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
72 60 70 71 syl2anc 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( exp ` ( ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
73 26 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( -u N x. x ) e. CC )
74 56 59 73 adddid 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( m x. x ) + ( -u N x. x ) ) ) = ( ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) )
75 25 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> -u N e. CC )
76 57 75 58 adddird 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m + -u N ) x. x ) = ( ( m x. x ) + ( -u N x. x ) ) )
77 22 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> N e. CC )
78 57 77 negsubd 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m + -u N ) = ( m - N ) )
79 78 oveq1d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m + -u N ) x. x ) = ( ( m - N ) x. x ) )
80 76 79 eqtr3d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m x. x ) + ( -u N x. x ) ) = ( ( m - N ) x. x ) )
81 80 oveq2d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( m x. x ) + ( -u N x. x ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) )
82 74 81 eqtr3d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) = ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) )
83 82 fveq2d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( exp ` ( ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) + ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) )
84 72 83 eqtr3d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) )
85 84 oveq2d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) )
86 85 adantr 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) )
87 69 86 eqtrd 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) )
88 87 sumeq2dv 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N 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. ( ( m - N ) x. x ) ) ) ) )
89 67 88 eqtrd 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ 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 ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N 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. ( ( m - N ) x. x ) ) ) ) )
90 89 sumeq2dv 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> 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 ) ) ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N 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. ( ( m - N ) x. x ) ) ) ) )
91 14 65 90 3eqtrd 
 |-  ( ( ph /\ x e. ( 0 (,) 1 ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( ( L ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N 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. ( ( m - N ) x. x ) ) ) ) )
92 91 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( ( L ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x = S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x )
93 ioombl 
 |-  ( 0 (,) 1 ) e. dom vol
94 93 a1i 
 |-  ( ph -> ( 0 (,) 1 ) e. dom vol )
95 fzfid 
 |-  ( ph -> ( 0 ... ( S x. N ) ) e. Fin )
96 sumex 
 |-  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 - N ) x. x ) ) ) ) e. _V
97 96 a1i 
 |-  ( ( ph /\ ( x e. ( 0 (,) 1 ) /\ 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 - N ) x. x ) ) ) ) e. _V )
98 94 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 (,) 1 ) e. dom vol )
99 29 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) C_ NN )
100 10 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> S e. NN0 )
101 fzfid 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) e. Fin )
102 99 33 100 101 reprfi 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( 1 ... N ) ( repr ` S ) m ) e. Fin )
103 38 a1i 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 0 ..^ S ) e. Fin )
104 53 adantllr 
 |-  ( ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( c ` a ) ) e. CC )
105 103 104 fprodcl 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
106 57 77 subcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m - N ) e. CC )
107 106 58 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m - N ) x. x ) e. CC )
108 56 107 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) e. CC )
109 108 an32s 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) e. CC )
110 109 adantr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) e. CC )
111 110 efcld 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) e. CC )
112 105 111 mulcld 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) /\ 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 - N ) x. x ) ) ) ) e. CC )
113 112 anasss 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ ( x e. ( 0 (,) 1 ) /\ 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 - N ) x. x ) ) ) ) e. CC )
114 38 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 0 ..^ S ) e. Fin )
115 114 53 fprodcl 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
116 fvex 
 |-  ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) e. _V
117 116 a1i 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ x e. ( 0 (,) 1 ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) e. _V )
118 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
119 118 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 (,) 1 ) C_ ( 0 [,] 1 ) )
120 93 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 (,) 1 ) e. dom vol )
121 116 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 [,] 1 ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) e. _V )
122 0red 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 0 e. RR )
123 1red 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 1 e. RR )
124 22 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> N e. CC )
125 42 124 subcld 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m - N ) e. CC )
126 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
127 126 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 [,] 1 ) C_ CC )
128 ssidd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> CC C_ CC )
129 cncfmptc 
 |-  ( ( ( m - N ) e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( x e. ( 0 [,] 1 ) |-> ( m - N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
130 125 127 128 129 syl3anc 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> ( m - N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
131 cncfmptid 
 |-  ( ( ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
132 127 128 131 syl2anc 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
133 130 132 mulcncf 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> ( ( m - N ) x. x ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
134 133 efmul2picn 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
135 cniccibl 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ ( x e. ( 0 [,] 1 ) |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) -> ( x e. ( 0 [,] 1 ) |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) e. L^1 )
136 122 123 134 135 syl3anc 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) e. L^1 )
137 119 120 121 136 iblss 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 (,) 1 ) |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) e. L^1 )
138 137 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( x e. ( 0 (,) 1 ) |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) e. L^1 )
139 115 117 138 iblmulc2 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( x e. ( 0 (,) 1 ) |-> ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) ) e. L^1 )
140 98 102 113 139 itgfsum 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( x e. ( 0 (,) 1 ) |-> 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 - N ) x. x ) ) ) ) ) e. L^1 /\ S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) _d x ) )
141 140 simpld 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 (,) 1 ) |-> 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 - N ) x. x ) ) ) ) ) e. L^1 )
142 94 95 97 141 itgfsum 
 |-  ( ph -> ( ( x e. ( 0 (,) 1 ) |-> 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 - N ) x. x ) ) ) ) ) e. L^1 /\ S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x = sum_ m e. ( 0 ... ( S x. N ) ) S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x ) )
143 142 simprd 
 |-  ( ph -> S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x = sum_ m e. ( 0 ... ( S x. N ) ) S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x )
144 oveq2 
 |-  ( if ( ( m - N ) = 0 , 1 , 0 ) = 1 -> ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. if ( ( m - N ) = 0 , 1 , 0 ) ) = ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. 1 ) )
145 oveq2 
 |-  ( if ( ( m - N ) = 0 , 1 , 0 ) = 0 -> ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. if ( ( m - N ) = 0 , 1 , 0 ) ) = ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. 0 ) )
146 102 115 fsumcl 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
147 146 mulid1d 
 |-  ( ( 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. 1 ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
148 146 mul01d 
 |-  ( ( 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. 0 ) = 0 )
149 144 145 147 148 ifeq3da 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> if ( ( m - N ) = 0 , sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) , 0 ) = ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. if ( ( m - N ) = 0 , 1 , 0 ) ) )
150 velsn 
 |-  ( m e. { N } <-> m = N )
151 42 124 subeq0ad 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m - N ) = 0 <-> m = N ) )
152 150 151 bitr4id 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m e. { N } <-> ( m - N ) = 0 ) )
153 152 ifbid 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> if ( m e. { N } , sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) , 0 ) = if ( ( m - N ) = 0 , sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) , 0 ) )
154 1 nn0zd 
 |-  ( ph -> N e. ZZ )
155 154 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> N e. ZZ )
156 47 155 zsubcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( m - N ) e. ZZ )
157 itgexpif 
 |-  ( ( m - N ) e. ZZ -> S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x = if ( ( m - N ) = 0 , 1 , 0 ) )
158 156 157 syl 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x = if ( ( m - N ) = 0 , 1 , 0 ) )
159 158 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. if ( ( m - N ) = 0 , 1 , 0 ) ) )
160 159 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. if ( ( m - N ) = 0 , 1 , 0 ) ) )
161 1cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 1 e. CC )
162 0cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 0 e. CC )
163 161 162 ifcld 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> if ( ( m - N ) = 0 , 1 , 0 ) e. CC )
164 102 163 115 fsummulc1 
 |-  ( ( 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. if ( ( m - N ) = 0 , 1 , 0 ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. if ( ( m - N ) = 0 , 1 , 0 ) ) )
165 160 164 eqtr4d 
 |-  ( ( 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = ( sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. if ( ( m - N ) = 0 , 1 , 0 ) ) )
166 149 153 165 3eqtr4rd 
 |-  ( ( 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = if ( m e. { N } , sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) , 0 ) )
167 166 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = sum_ m e. ( 0 ... ( S x. N ) ) if ( m e. { N } , sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) , 0 ) )
168 0zd 
 |-  ( ph -> 0 e. ZZ )
169 10 nn0zd 
 |-  ( ph -> S e. ZZ )
170 169 154 zmulcld 
 |-  ( ph -> ( S x. N ) e. ZZ )
171 1 nn0ge0d 
 |-  ( ph -> 0 <_ N )
172 nnmulge 
 |-  ( ( S e. NN /\ N e. NN0 ) -> N <_ ( S x. N ) )
173 2 1 172 syl2anc 
 |-  ( ph -> N <_ ( S x. N ) )
174 elfz4 
 |-  ( ( ( 0 e. ZZ /\ ( S x. N ) e. ZZ /\ N e. ZZ ) /\ ( 0 <_ N /\ N <_ ( S x. N ) ) ) -> N e. ( 0 ... ( S x. N ) ) )
175 168 170 154 171 173 174 syl32anc 
 |-  ( ph -> N e. ( 0 ... ( S x. N ) ) )
176 175 snssd 
 |-  ( ph -> { N } C_ ( 0 ... ( S x. N ) ) )
177 176 sselda 
 |-  ( ( ph /\ m e. { N } ) -> m e. ( 0 ... ( S x. N ) ) )
178 177 146 syldan 
 |-  ( ( ph /\ m e. { N } ) -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
179 178 ralrimiva 
 |-  ( ph -> A. m e. { N } sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
180 95 olcd 
 |-  ( ph -> ( ( 0 ... ( S x. N ) ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... ( S x. N ) ) e. Fin ) )
181 sumss2 
 |-  ( ( ( { N } C_ ( 0 ... ( S x. N ) ) /\ A. m e. { N } sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC ) /\ ( ( 0 ... ( S x. N ) ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... ( S x. N ) ) e. Fin ) ) -> sum_ m e. { N } sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) = sum_ m e. ( 0 ... ( S x. N ) ) if ( m e. { N } , sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) , 0 ) )
182 176 179 180 181 syl21anc 
 |-  ( ph -> sum_ m e. { N } sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) = sum_ m e. ( 0 ... ( S x. N ) ) if ( m e. { N } , sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) , 0 ) )
183 29 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
184 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
185 183 154 10 184 reprfi 
 |-  ( ph -> ( ( 1 ... N ) ( repr ` S ) N ) e. Fin )
186 38 a1i 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> ( 0 ..^ S ) e. Fin )
187 1 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> N e. NN0 )
188 10 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> S e. NN0 )
189 22 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> N e. CC )
190 3 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
191 simpr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
192 29 a1i 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> ( 1 ... N ) C_ NN )
193 154 adantr 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> N e. ZZ )
194 10 adantr 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> S e. NN0 )
195 simpr 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> c e. ( ( 1 ... N ) ( repr ` S ) N ) )
196 192 193 194 195 reprf 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> c : ( 0 ..^ S ) --> ( 1 ... N ) )
197 196 ffvelrnda 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. ( 1 ... N ) )
198 29 197 sseldi 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN )
199 187 188 189 190 191 198 breprexplemb 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( c ` a ) ) e. CC )
200 186 199 fprodcl 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
201 185 200 fsumcl 
 |-  ( ph -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
202 oveq2 
 |-  ( m = N -> ( ( 1 ... N ) ( repr ` S ) m ) = ( ( 1 ... N ) ( repr ` S ) N ) )
203 202 sumeq1d 
 |-  ( m = N -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
204 203 sumsn 
 |-  ( ( N e. NN0 /\ sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC ) -> sum_ m e. { N } sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
205 1 201 204 syl2anc 
 |-  ( ph -> sum_ m e. { N } sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
206 167 182 205 3eqtr2d 
 |-  ( 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
207 140 simprd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) _d x )
208 111 an32s 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ x e. ( 0 (,) 1 ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) e. CC )
209 115 208 138 itgmulc2 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) _d x )
210 209 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) ) _d x )
211 207 210 eqtr4d 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) )
212 211 sumeq2dv 
 |-  ( ph -> sum_ m e. ( 0 ... ( S x. N ) ) S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d 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. S. ( 0 (,) 1 ) ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) _d x ) )
213 1 10 reprfz1 
 |-  ( ph -> ( NN ( repr ` S ) N ) = ( ( 1 ... N ) ( repr ` S ) N ) )
214 213 sumeq1d 
 |-  ( ph -> sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
215 206 212 214 3eqtr4d 
 |-  ( ph -> sum_ m e. ( 0 ... ( S x. N ) ) S. ( 0 (,) 1 ) 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 - N ) x. x ) ) ) ) _d x = sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
216 92 143 215 3eqtrrd 
 |-  ( ph -> sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) = S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( ( L ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )