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 simpr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ( 0 ... ( S x. N ) ) )
32 31 elfzelzd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ZZ )
33 32 adantlr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. ZZ )
34 11 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> S e. NN0 )
35 fzfid 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) e. Fin )
36 30 33 34 35 reprfi 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( 1 ... N ) ( repr ` S ) m ) e. Fin )
37 fzofi 
 |-  ( 0 ..^ S ) e. Fin
38 37 a1i 
 |-  ( ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 0 ..^ S ) e. Fin )
39 1 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> N e. NN0 )
40 10 ad3antrrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> S e. NN0 )
41 32 zcnd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. CC )
42 41 ad2antrr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> m e. CC )
43 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 ) )
44 simpr 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
45 29 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 1 ... N ) C_ NN )
46 32 adantr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> m e. ZZ )
47 10 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> S e. NN0 )
48 simpr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> c e. ( ( 1 ... N ) ( repr ` S ) m ) )
49 45 46 47 48 reprf 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> c : ( 0 ..^ S ) --> ( 1 ... N ) )
50 49 ffvelrnda 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. ( 1 ... N ) )
51 29 50 sselid 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN )
52 39 40 42 43 44 51 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 )
53 52 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 )
54 38 53 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 )
55 20 a1i 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( _i x. ( 2 x. _pi ) ) e. CC )
56 33 zcnd 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> m e. CC )
57 9 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> x e. CC )
58 56 57 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m x. x ) e. CC )
59 55 58 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) e. CC )
60 59 efcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( m x. x ) ) ) e. CC )
61 60 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 )
62 54 61 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 )
63 36 62 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 )
64 15 28 63 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 ) ) ) ) )
65 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 )
66 36 65 62 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 ) ) ) ) )
67 65 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 )
68 54 61 67 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 ) ) ) ) ) )
69 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 )
70 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 ) ) ) ) )
71 59 69 70 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 ) ) ) ) )
72 26 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( -u N x. x ) e. CC )
73 55 58 72 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 ) ) ) )
74 25 adantr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> -u N e. CC )
75 56 74 57 adddird 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m + -u N ) x. x ) = ( ( m x. x ) + ( -u N x. x ) ) )
76 22 ad2antrr 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> N e. CC )
77 56 76 negsubd 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m + -u N ) = ( m - N ) )
78 77 oveq1d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m + -u N ) x. x ) = ( ( m - N ) x. x ) )
79 75 78 eqtr3d 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m x. x ) + ( -u N x. x ) ) = ( ( m - N ) x. x ) )
80 79 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 ) ) )
81 73 80 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 ) ) )
82 81 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 ) ) ) )
83 71 82 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 ) ) ) )
84 83 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 ) ) ) ) )
85 84 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 ) ) ) ) )
86 68 85 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 ) ) ) ) )
87 86 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 ) ) ) ) )
88 66 87 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 ) ) ) ) )
89 88 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 ) ) ) ) )
90 14 64 89 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 ) ) ) ) )
91 90 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 )
92 ioombl 
 |-  ( 0 (,) 1 ) e. dom vol
93 92 a1i 
 |-  ( ph -> ( 0 (,) 1 ) e. dom vol )
94 fzfid 
 |-  ( ph -> ( 0 ... ( S x. N ) ) e. Fin )
95 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
96 95 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 )
97 93 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 (,) 1 ) e. dom vol )
98 29 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) C_ NN )
99 10 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> S e. NN0 )
100 fzfid 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 1 ... N ) e. Fin )
101 98 32 99 100 reprfi 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( 1 ... N ) ( repr ` S ) m ) e. Fin )
102 37 a1i 
 |-  ( ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 0 ..^ S ) e. Fin )
103 52 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 )
104 102 103 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 )
105 56 76 subcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m - N ) e. CC )
106 105 57 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m - N ) x. x ) e. CC )
107 55 106 mulcld 
 |-  ( ( ( ph /\ x e. ( 0 (,) 1 ) ) /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) e. CC )
108 107 an32s 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ x e. ( 0 (,) 1 ) ) -> ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) e. CC )
109 108 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 )
110 109 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 )
111 104 110 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 )
112 111 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 )
113 37 a1i 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( 0 ..^ S ) e. Fin )
114 113 52 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 )
115 fvex 
 |-  ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( ( m - N ) x. x ) ) ) e. _V
116 115 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 )
117 ioossicc 
 |-  ( 0 (,) 1 ) C_ ( 0 [,] 1 )
118 117 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 (,) 1 ) C_ ( 0 [,] 1 ) )
119 92 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 (,) 1 ) e. dom vol )
120 115 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 )
121 0red 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 0 e. RR )
122 1red 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 1 e. RR )
123 22 adantr 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> N e. CC )
124 41 123 subcld 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m - N ) e. CC )
125 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
126 125 a1i 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( 0 [,] 1 ) C_ CC )
127 ssidd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> CC C_ CC )
128 cncfmptc 
 |-  ( ( ( m - N ) e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( x e. ( 0 [,] 1 ) |-> ( m - N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
129 124 126 127 128 syl3anc 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> ( m - N ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
130 cncfmptid 
 |-  ( ( ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
131 126 127 130 syl2anc 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> x ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
132 129 131 mulcncf 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( x e. ( 0 [,] 1 ) |-> ( ( m - N ) x. x ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
133 132 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 ) )
134 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 )
135 121 122 133 134 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 )
136 118 119 120 135 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 )
137 136 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 )
138 114 116 137 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 )
139 97 101 112 138 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 ) )
140 139 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 )
141 93 94 96 140 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 ) )
142 141 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 )
143 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 ) )
144 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 ) )
145 101 114 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 )
146 145 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 ) ) )
147 145 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 )
148 143 144 146 147 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 ) ) )
149 velsn 
 |-  ( m e. { N } <-> m = N )
150 41 123 subeq0ad 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( ( m - N ) = 0 <-> m = N ) )
151 149 150 bitr4id 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> ( m e. { N } <-> ( m - N ) = 0 ) )
152 151 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 ) )
153 1 nn0zd 
 |-  ( ph -> N e. ZZ )
154 153 ad2antrr 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> N e. ZZ )
155 46 154 zsubcld 
 |-  ( ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) /\ c e. ( ( 1 ... N ) ( repr ` S ) m ) ) -> ( m - N ) e. ZZ )
156 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 ) )
157 155 156 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 ) )
158 157 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 ) ) )
159 158 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 ) ) )
160 1cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 1 e. CC )
161 0cnd 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> 0 e. CC )
162 160 161 ifcld 
 |-  ( ( ph /\ m e. ( 0 ... ( S x. N ) ) ) -> if ( ( m - N ) = 0 , 1 , 0 ) e. CC )
163 101 162 114 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 ) ) )
164 159 163 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 ) ) )
165 148 152 164 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 ) )
166 165 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 ) )
167 0zd 
 |-  ( ph -> 0 e. ZZ )
168 10 nn0zd 
 |-  ( ph -> S e. ZZ )
169 168 153 zmulcld 
 |-  ( ph -> ( S x. N ) e. ZZ )
170 1 nn0ge0d 
 |-  ( ph -> 0 <_ N )
171 nnmulge 
 |-  ( ( S e. NN /\ N e. NN0 ) -> N <_ ( S x. N ) )
172 2 1 171 syl2anc 
 |-  ( ph -> N <_ ( S x. N ) )
173 167 169 153 170 172 elfzd 
 |-  ( ph -> N e. ( 0 ... ( S x. N ) ) )
174 173 snssd 
 |-  ( ph -> { N } C_ ( 0 ... ( S x. N ) ) )
175 174 sselda 
 |-  ( ( ph /\ m e. { N } ) -> m e. ( 0 ... ( S x. N ) ) )
176 175 145 syldan 
 |-  ( ( ph /\ m e. { N } ) -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
177 176 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 )
178 94 olcd 
 |-  ( ph -> ( ( 0 ... ( S x. N ) ) C_ ( ZZ>= ` 0 ) \/ ( 0 ... ( S x. N ) ) e. Fin ) )
179 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 ) )
180 174 177 178 179 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 ) )
181 29 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
182 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
183 181 153 10 182 reprfi 
 |-  ( ph -> ( ( 1 ... N ) ( repr ` S ) N ) e. Fin )
184 37 a1i 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> ( 0 ..^ S ) e. Fin )
185 1 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> N e. NN0 )
186 10 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> S e. NN0 )
187 22 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> N e. CC )
188 3 ad2antrr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
189 simpr 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
190 29 a1i 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> ( 1 ... N ) C_ NN )
191 153 adantr 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> N e. ZZ )
192 10 adantr 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> S e. NN0 )
193 simpr 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> c e. ( ( 1 ... N ) ( repr ` S ) N ) )
194 190 191 192 193 reprf 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> c : ( 0 ..^ S ) --> ( 1 ... N ) )
195 194 ffvelrnda 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. ( 1 ... N ) )
196 29 195 sselid 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN )
197 185 186 187 188 189 196 breprexplemb 
 |-  ( ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( L ` a ) ` ( c ` a ) ) e. CC )
198 184 197 fprodcl 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` S ) N ) ) -> prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
199 183 198 fsumcl 
 |-  ( ph -> sum_ c e. ( ( 1 ... N ) ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) e. CC )
200 oveq2 
 |-  ( m = N -> ( ( 1 ... N ) ( repr ` S ) m ) = ( ( 1 ... N ) ( repr ` S ) N ) )
201 200 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 ) ) )
202 201 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 ) ) )
203 1 199 202 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 ) ) )
204 166 180 203 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 ) ) )
205 139 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 )
206 110 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 )
207 114 206 137 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 )
208 207 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 )
209 205 208 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 ) )
210 209 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 ) )
211 1 10 reprfz1 
 |-  ( ph -> ( NN ( repr ` S ) N ) = ( ( 1 ... N ) ( repr ` S ) N ) )
212 211 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 ) ) )
213 204 210 212 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 ) ) )
214 91 142 213 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 )