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

Metamath Proof Explorer

Theorem breprexp

Description: Express the S th power of the finite series in terms of the number of representations of integers m as sums of S terms. This is a general formulation which allows logarithmic weighting of the sums (see https://mathoverflow.net/questions/253246) and a mix of different smoothing functions taken into account in L . See breprexpnat for the simple case presented in the proposition of Nathanson p. 123. (Contributed by Thierry Arnoux, 6-Dec-2021)

Ref Expression
Hypotheses breprexp.n 
|- ( ph -> N e. NN0 )
breprexp.s 
|- ( ph -> S e. NN0 )
breprexp.z 
|- ( ph -> Z e. CC )
breprexp.h 
|- ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
Assertion breprexp 
|- ( ph -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )

Proof

Step Hyp Ref Expression
1 breprexp.n 
 |-  ( ph -> N e. NN0 )
2 breprexp.s 
 |-  ( ph -> S e. NN0 )
3 breprexp.z 
 |-  ( ph -> Z e. CC )
4 breprexp.h 
 |-  ( ph -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
5 nn0ssre 
 |-  NN0 C_ RR
6 5 a1i 
 |-  ( ph -> NN0 C_ RR )
7 6 sselda 
 |-  ( ( ph /\ S e. NN0 ) -> S e. RR )
8 leid 
 |-  ( S e. RR -> S <_ S )
9 7 8 syl 
 |-  ( ( ph /\ S e. NN0 ) -> S <_ S )
10 breq1 
 |-  ( t = 0 -> ( t <_ S <-> 0 <_ S ) )
11 oveq2 
 |-  ( t = 0 -> ( 0 ..^ t ) = ( 0 ..^ 0 ) )
12 11 prodeq1d 
 |-  ( t = 0 -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) )
13 oveq1 
 |-  ( t = 0 -> ( t x. N ) = ( 0 x. N ) )
14 13 oveq2d 
 |-  ( t = 0 -> ( 0 ... ( t x. N ) ) = ( 0 ... ( 0 x. N ) ) )
15 fveq2 
 |-  ( t = 0 -> ( repr ` t ) = ( repr ` 0 ) )
16 15 oveqd 
 |-  ( t = 0 -> ( ( 1 ... N ) ( repr ` t ) m ) = ( ( 1 ... N ) ( repr ` 0 ) m ) )
17 11 prodeq1d 
 |-  ( t = 0 -> prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) )
18 17 oveq1d 
 |-  ( t = 0 -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
19 18 adantr 
 |-  ( ( t = 0 /\ c e. ( ( 1 ... N ) ( repr ` t ) m ) ) -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
20 16 19 sumeq12dv 
 |-  ( t = 0 -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
21 20 adantr 
 |-  ( ( t = 0 /\ m e. ( 0 ... ( t x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
22 14 21 sumeq12dv 
 |-  ( t = 0 -> sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ m e. ( 0 ... ( 0 x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
23 12 22 eqeq12d 
 |-  ( t = 0 -> ( prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) <-> prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( 0 x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
24 10 23 imbi12d 
 |-  ( t = 0 -> ( ( t <_ S -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) <-> ( 0 <_ S -> prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( 0 x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) )
25 breq1 
 |-  ( t = s -> ( t <_ S <-> s <_ S ) )
26 oveq2 
 |-  ( t = s -> ( 0 ..^ t ) = ( 0 ..^ s ) )
27 26 prodeq1d 
 |-  ( t = s -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) )
28 oveq1 
 |-  ( t = s -> ( t x. N ) = ( s x. N ) )
29 28 oveq2d 
 |-  ( t = s -> ( 0 ... ( t x. N ) ) = ( 0 ... ( s x. N ) ) )
30 fveq2 
 |-  ( t = s -> ( repr ` t ) = ( repr ` s ) )
31 30 oveqd 
 |-  ( t = s -> ( ( 1 ... N ) ( repr ` t ) m ) = ( ( 1 ... N ) ( repr ` s ) m ) )
32 26 prodeq1d 
 |-  ( t = s -> prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) )
33 32 oveq1d 
 |-  ( t = s -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
34 33 adantr 
 |-  ( ( t = s /\ c e. ( ( 1 ... N ) ( repr ` t ) m ) ) -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
35 31 34 sumeq12dv 
 |-  ( t = s -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
36 35 adantr 
 |-  ( ( t = s /\ m e. ( 0 ... ( t x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
37 29 36 sumeq12dv 
 |-  ( t = s -> sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = 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. ( Z ^ m ) ) )
38 27 37 eqeq12d 
 |-  ( t = s -> ( prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) <-> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
39 25 38 imbi12d 
 |-  ( t = s -> ( ( t <_ S -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) <-> ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) )
40 breq1 
 |-  ( t = ( s + 1 ) -> ( t <_ S <-> ( s + 1 ) <_ S ) )
41 oveq2 
 |-  ( t = ( s + 1 ) -> ( 0 ..^ t ) = ( 0 ..^ ( s + 1 ) ) )
42 41 prodeq1d 
 |-  ( t = ( s + 1 ) -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ a e. ( 0 ..^ ( s + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) )
43 oveq1 
 |-  ( t = ( s + 1 ) -> ( t x. N ) = ( ( s + 1 ) x. N ) )
44 43 oveq2d 
 |-  ( t = ( s + 1 ) -> ( 0 ... ( t x. N ) ) = ( 0 ... ( ( s + 1 ) x. N ) ) )
45 fveq2 
 |-  ( t = ( s + 1 ) -> ( repr ` t ) = ( repr ` ( s + 1 ) ) )
46 45 oveqd 
 |-  ( t = ( s + 1 ) -> ( ( 1 ... N ) ( repr ` t ) m ) = ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) )
47 41 prodeq1d 
 |-  ( t = ( s + 1 ) -> prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) )
48 47 oveq1d 
 |-  ( t = ( s + 1 ) -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
49 48 adantr 
 |-  ( ( t = ( s + 1 ) /\ c e. ( ( 1 ... N ) ( repr ` t ) m ) ) -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
50 46 49 sumeq12dv 
 |-  ( t = ( s + 1 ) -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
51 50 adantr 
 |-  ( ( t = ( s + 1 ) /\ m e. ( 0 ... ( t x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
52 44 51 sumeq12dv 
 |-  ( t = ( s + 1 ) -> sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ m e. ( 0 ... ( ( s + 1 ) x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
53 42 52 eqeq12d 
 |-  ( t = ( s + 1 ) -> ( prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) <-> prod_ a e. ( 0 ..^ ( s + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( s + 1 ) x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
54 40 53 imbi12d 
 |-  ( t = ( s + 1 ) -> ( ( t <_ S -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) <-> ( ( s + 1 ) <_ S -> prod_ a e. ( 0 ..^ ( s + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( s + 1 ) x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) )
55 breq1 
 |-  ( t = S -> ( t <_ S <-> S <_ S ) )
56 oveq2 
 |-  ( t = S -> ( 0 ..^ t ) = ( 0 ..^ S ) )
57 56 prodeq1d 
 |-  ( t = S -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) )
58 oveq1 
 |-  ( t = S -> ( t x. N ) = ( S x. N ) )
59 58 oveq2d 
 |-  ( t = S -> ( 0 ... ( t x. N ) ) = ( 0 ... ( S x. N ) ) )
60 fveq2 
 |-  ( t = S -> ( repr ` t ) = ( repr ` S ) )
61 60 oveqd 
 |-  ( t = S -> ( ( 1 ... N ) ( repr ` t ) m ) = ( ( 1 ... N ) ( repr ` S ) m ) )
62 56 prodeq1d 
 |-  ( t = S -> prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) )
63 62 oveq1d 
 |-  ( t = S -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
64 63 adantr 
 |-  ( ( t = S /\ c e. ( ( 1 ... N ) ( repr ` t ) m ) ) -> ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
65 61 64 sumeq12dv 
 |-  ( t = S -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
66 65 adantr 
 |-  ( ( t = S /\ m e. ( 0 ... ( t x. N ) ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
67 59 66 sumeq12dv 
 |-  ( t = S -> sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = 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. ( Z ^ m ) ) )
68 57 67 eqeq12d 
 |-  ( t = S -> ( prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) <-> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
69 55 68 imbi12d 
 |-  ( t = S -> ( ( t <_ S -> prod_ a e. ( 0 ..^ t ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( t x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` t ) m ) ( prod_ a e. ( 0 ..^ t ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) <-> ( S <_ S -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) )
70 0nn0 
 |-  0 e. NN0
71 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
72 71 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
73 0zd 
 |-  ( ph -> 0 e. ZZ )
74 72 73 1 repr0 
 |-  ( ph -> ( ( 1 ... N ) ( repr ` 0 ) 0 ) = if ( 0 = 0 , { (/) } , (/) ) )
75 eqid 
 |-  0 = 0
76 75 iftruei 
 |-  if ( 0 = 0 , { (/) } , (/) ) = { (/) }
77 74 76 eqtrdi 
 |-  ( ph -> ( ( 1 ... N ) ( repr ` 0 ) 0 ) = { (/) } )
78 snfi 
 |-  { (/) } e. Fin
79 77 78 eqeltrdi 
 |-  ( ph -> ( ( 1 ... N ) ( repr ` 0 ) 0 ) e. Fin )
80 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
81 80 prodeq1i 
 |-  prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) = prod_ a e. (/) ( ( L ` a ) ` ( c ` a ) )
82 prod0 
 |-  prod_ a e. (/) ( ( L ` a ) ` ( c ` a ) ) = 1
83 81 82 eqtri 
 |-  prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) = 1
84 83 a1i 
 |-  ( ph -> prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) = 1 )
85 exp0 
 |-  ( Z e. CC -> ( Z ^ 0 ) = 1 )
86 3 85 syl 
 |-  ( ph -> ( Z ^ 0 ) = 1 )
87 84 86 oveq12d 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) = ( 1 x. 1 ) )
88 ax-1cn 
 |-  1 e. CC
89 88 mulridi 
 |-  ( 1 x. 1 ) = 1
90 87 89 eqtrdi 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) = 1 )
91 90 88 eqeltrdi 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) e. CC )
92 91 adantr 
 |-  ( ( ph /\ c e. ( ( 1 ... N ) ( repr ` 0 ) 0 ) ) -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) e. CC )
93 79 92 fsumcl 
 |-  ( ph -> sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) 0 ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) e. CC )
94 oveq2 
 |-  ( m = 0 -> ( ( 1 ... N ) ( repr ` 0 ) m ) = ( ( 1 ... N ) ( repr ` 0 ) 0 ) )
95 simpl 
 |-  ( ( m = 0 /\ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ) -> m = 0 )
96 95 oveq2d 
 |-  ( ( m = 0 /\ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ) -> ( Z ^ m ) = ( Z ^ 0 ) )
97 96 oveq2d 
 |-  ( ( m = 0 /\ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ) -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) )
98 94 97 sumeq12dv 
 |-  ( m = 0 -> sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) 0 ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) )
99 98 sumsn 
 |-  ( ( 0 e. NN0 /\ sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) 0 ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) e. CC ) -> sum_ m e. { 0 } sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) 0 ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) )
100 70 93 99 sylancr 
 |-  ( ph -> sum_ m e. { 0 } sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) 0 ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) )
101 77 sumeq1d 
 |-  ( ph -> sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) 0 ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) = sum_ c e. { (/) } ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) )
102 0ex 
 |-  (/) e. _V
103 80 prodeq1i 
 |-  prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) = prod_ a e. (/) ( ( L ` a ) ` ( (/) ` a ) )
104 prod0 
 |-  prod_ a e. (/) ( ( L ` a ) ` ( (/) ` a ) ) = 1
105 103 104 eqtri 
 |-  prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) = 1
106 105 a1i 
 |-  ( ph -> prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) = 1 )
107 106 88 eqeltrdi 
 |-  ( ph -> prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) e. CC )
108 86 88 eqeltrdi 
 |-  ( ph -> ( Z ^ 0 ) e. CC )
109 107 108 mulcld 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) x. ( Z ^ 0 ) ) e. CC )
110 fveq1 
 |-  ( c = (/) -> ( c ` a ) = ( (/) ` a ) )
111 110 fveq2d 
 |-  ( c = (/) -> ( ( L ` a ) ` ( c ` a ) ) = ( ( L ` a ) ` ( (/) ` a ) ) )
112 111 ralrimivw 
 |-  ( c = (/) -> A. a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) = ( ( L ` a ) ` ( (/) ` a ) ) )
113 112 prodeq2d 
 |-  ( c = (/) -> prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) )
114 113 oveq1d 
 |-  ( c = (/) -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) = ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) x. ( Z ^ 0 ) ) )
115 114 sumsn 
 |-  ( ( (/) e. _V /\ ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) x. ( Z ^ 0 ) ) e. CC ) -> sum_ c e. { (/) } ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) = ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) x. ( Z ^ 0 ) ) )
116 102 109 115 sylancr 
 |-  ( ph -> sum_ c e. { (/) } ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) = ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) x. ( Z ^ 0 ) ) )
117 106 86 oveq12d 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) x. ( Z ^ 0 ) ) = ( 1 x. 1 ) )
118 117 87 90 3eqtr2d 
 |-  ( ph -> ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( (/) ` a ) ) x. ( Z ^ 0 ) ) = 1 )
119 116 118 eqtrd 
 |-  ( ph -> sum_ c e. { (/) } ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ 0 ) ) = 1 )
120 100 101 119 3eqtrd 
 |-  ( ph -> sum_ m e. { 0 } sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = 1 )
121 1 nn0cnd 
 |-  ( ph -> N e. CC )
122 121 mul02d 
 |-  ( ph -> ( 0 x. N ) = 0 )
123 122 oveq2d 
 |-  ( ph -> ( 0 ... ( 0 x. N ) ) = ( 0 ... 0 ) )
124 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
125 123 124 eqtrdi 
 |-  ( ph -> ( 0 ... ( 0 x. N ) ) = { 0 } )
126 125 sumeq1d 
 |-  ( ph -> sum_ m e. ( 0 ... ( 0 x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ m e. { 0 } sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
127 80 prodeq1i 
 |-  prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ a e. (/) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) )
128 prod0 
 |-  prod_ a e. (/) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = 1
129 127 128 eqtri 
 |-  prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = 1
130 129 a1i 
 |-  ( ph -> prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = 1 )
131 120 126 130 3eqtr4rd 
 |-  ( ph -> prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( 0 x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
132 131 a1d 
 |-  ( ph -> ( 0 <_ S -> prod_ a e. ( 0 ..^ 0 ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( 0 x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` 0 ) m ) ( prod_ a e. ( 0 ..^ 0 ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
133 simpll 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( ph /\ s e. NN0 ) )
134 simplr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
135 oveq2 
 |-  ( m = n -> ( ( 1 ... N ) ( repr ` s ) m ) = ( ( 1 ... N ) ( repr ` s ) n ) )
136 oveq2 
 |-  ( m = n -> ( Z ^ m ) = ( Z ^ n ) )
137 136 oveq2d 
 |-  ( m = n -> ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) )
138 137 adantr 
 |-  ( ( m = n /\ c e. ( ( 1 ... N ) ( repr ` s ) m ) ) -> ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) )
139 135 138 sumeq12dv 
 |-  ( m = n -> sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) )
140 139 cbvsumv 
 |-  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. ( Z ^ m ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) )
141 140 eqeq2i 
 |-  ( prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) <-> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) )
142 simpl 
 |-  ( ( a = i /\ b e. ( 1 ... N ) ) -> a = i )
143 142 fveq2d 
 |-  ( ( a = i /\ b e. ( 1 ... N ) ) -> ( L ` a ) = ( L ` i ) )
144 143 fveq1d 
 |-  ( ( a = i /\ b e. ( 1 ... N ) ) -> ( ( L ` a ) ` b ) = ( ( L ` i ) ` b ) )
145 144 oveq1d 
 |-  ( ( a = i /\ b e. ( 1 ... N ) ) -> ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = ( ( ( L ` i ) ` b ) x. ( Z ^ b ) ) )
146 145 sumeq2dv 
 |-  ( a = i -> sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ b e. ( 1 ... N ) ( ( ( L ` i ) ` b ) x. ( Z ^ b ) ) )
147 146 cbvprodv 
 |-  prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ i e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` i ) ` b ) x. ( Z ^ b ) )
148 fveq2 
 |-  ( b = j -> ( ( L ` i ) ` b ) = ( ( L ` i ) ` j ) )
149 oveq2 
 |-  ( b = j -> ( Z ^ b ) = ( Z ^ j ) )
150 148 149 oveq12d 
 |-  ( b = j -> ( ( ( L ` i ) ` b ) x. ( Z ^ b ) ) = ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) )
151 150 cbvsumv 
 |-  sum_ b e. ( 1 ... N ) ( ( ( L ` i ) ` b ) x. ( Z ^ b ) ) = sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) )
152 151 a1i 
 |-  ( i e. ( 0 ..^ s ) -> sum_ b e. ( 1 ... N ) ( ( ( L ` i ) ` b ) x. ( Z ^ b ) ) = sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) )
153 152 prodeq2i 
 |-  prod_ i e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` i ) ` b ) x. ( Z ^ b ) ) = prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) )
154 147 153 eqtri 
 |-  prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) )
155 fveq2 
 |-  ( a = i -> ( L ` a ) = ( L ` i ) )
156 fveq2 
 |-  ( a = i -> ( c ` a ) = ( c ` i ) )
157 155 156 fveq12d 
 |-  ( a = i -> ( ( L ` a ) ` ( c ` a ) ) = ( ( L ` i ) ` ( c ` i ) ) )
158 157 cbvprodv 
 |-  prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) = prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( c ` i ) )
159 158 oveq1i 
 |-  ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) = ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( c ` i ) ) x. ( Z ^ n ) )
160 159 a1i 
 |-  ( c e. ( ( 1 ... N ) ( repr ` s ) n ) -> ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) = ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( c ` i ) ) x. ( Z ^ n ) ) )
161 160 sumeq2i 
 |-  sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) = sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( c ` i ) ) x. ( Z ^ n ) )
162 simpl 
 |-  ( ( c = k /\ i e. ( 0 ..^ s ) ) -> c = k )
163 162 fveq1d 
 |-  ( ( c = k /\ i e. ( 0 ..^ s ) ) -> ( c ` i ) = ( k ` i ) )
164 163 fveq2d 
 |-  ( ( c = k /\ i e. ( 0 ..^ s ) ) -> ( ( L ` i ) ` ( c ` i ) ) = ( ( L ` i ) ` ( k ` i ) ) )
165 164 prodeq2dv 
 |-  ( c = k -> prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( c ` i ) ) = prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) )
166 165 oveq1d 
 |-  ( c = k -> ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( c ` i ) ) x. ( Z ^ n ) ) = ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) )
167 166 cbvsumv 
 |-  sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( c ` i ) ) x. ( Z ^ n ) ) = sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) )
168 161 167 eqtri 
 |-  sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) = sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) )
169 168 a1i 
 |-  ( n e. ( 0 ... ( s x. N ) ) -> sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) = sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) )
170 169 sumeq2i 
 |-  sum_ n e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) )
171 154 170 eqeq12i 
 |-  ( prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ n ) ) <-> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) )
172 141 171 bitri 
 |-  ( prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) <-> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) )
173 172 imbi2i 
 |-  ( ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) <-> ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) )
174 134 173 sylib 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) )
175 simpr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( s + 1 ) <_ S )
176 1 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> N e. NN0 )
177 2 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> S e. NN0 )
178 3 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> Z e. CC )
179 4 ad3antrrr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> L : ( 0 ..^ S ) --> ( CC ^m NN ) )
180 simpllr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> s e. NN0 )
181 simpr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( s + 1 ) <_ S )
182 5 180 sselid 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> s e. RR )
183 1red 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> 1 e. RR )
184 182 183 readdcld 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( s + 1 ) e. RR )
185 5 177 sselid 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> S e. RR )
186 182 ltp1d 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> s < ( s + 1 ) )
187 182 184 186 ltled 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> s <_ ( s + 1 ) )
188 182 184 185 187 181 letrd 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> s <_ S )
189 simplr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) )
190 189 173 sylibr 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
191 188 190 mpd 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
192 176 177 178 179 180 181 191 breprexplemc 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ i e. ( 0 ..^ s ) sum_ j e. ( 1 ... N ) ( ( ( L ` i ) ` j ) x. ( Z ^ j ) ) = sum_ n e. ( 0 ... ( s x. N ) ) sum_ k e. ( ( 1 ... N ) ( repr ` s ) n ) ( prod_ i e. ( 0 ..^ s ) ( ( L ` i ) ` ( k ` i ) ) x. ( Z ^ n ) ) ) ) /\ ( s + 1 ) <_ S ) -> prod_ a e. ( 0 ..^ ( s + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( s + 1 ) x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
193 133 174 175 192 syl21anc 
 |-  ( ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) /\ ( s + 1 ) <_ S ) -> prod_ a e. ( 0 ..^ ( s + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( s + 1 ) x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
194 193 ex 
 |-  ( ( ( ph /\ s e. NN0 ) /\ ( s <_ S -> prod_ a e. ( 0 ..^ s ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( s x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` s ) m ) ( prod_ a e. ( 0 ..^ s ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) ) -> ( ( s + 1 ) <_ S -> prod_ a e. ( 0 ..^ ( s + 1 ) ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( ( s + 1 ) x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` ( s + 1 ) ) m ) ( prod_ a e. ( 0 ..^ ( s + 1 ) ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
195 24 39 54 69 132 194 nn0indd 
 |-  ( ( ph /\ S e. NN0 ) -> ( S <_ S -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) ) )
196 9 195 mpd 
 |-  ( ( ph /\ S e. NN0 ) -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )
197 2 196 mpdan 
 |-  ( ph -> prod_ a e. ( 0 ..^ S ) sum_ b e. ( 1 ... N ) ( ( ( L ` a ) ` b ) x. ( Z ^ b ) ) = sum_ m e. ( 0 ... ( S x. N ) ) sum_ c e. ( ( 1 ... N ) ( repr ` S ) m ) ( prod_ a e. ( 0 ..^ S ) ( ( L ` a ) ` ( c ` a ) ) x. ( Z ^ m ) ) )