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 ) |