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

Metamath Proof Explorer

Theorem fsum2dsub

Description: Lemma for breprexp - Re-index a double sum, using difference of the initial indices. (Contributed by Thierry Arnoux, 7-Dec-2021)

Ref Expression
Hypotheses fzsum2sub.m 
|- ( ph -> M e. NN0 )
fzsum2sub.n 
|- ( ph -> N e. NN0 )
fzsum2sub.1 
|- ( i = ( k - j ) -> A = B )
fzsum2sub.2 
|- ( ( ph /\ i e. ( ZZ>= ` -u j ) /\ j e. ( 1 ... N ) ) -> A e. CC )
fzsum2sub.3 
|- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) ) -> B = 0 )
fzsum2sub.4 
|- ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( 0 ..^ j ) ) -> B = 0 )
Assertion fsum2dsub 
|- ( ph -> sum_ i e. ( 0 ... M ) sum_ j e. ( 1 ... N ) A = sum_ k e. ( 0 ... ( M + N ) ) sum_ j e. ( 1 ... N ) B )

Proof

Step Hyp Ref Expression
1 fzsum2sub.m 
 |-  ( ph -> M e. NN0 )
2 fzsum2sub.n 
 |-  ( ph -> N e. NN0 )
3 fzsum2sub.1 
 |-  ( i = ( k - j ) -> A = B )
4 fzsum2sub.2 
 |-  ( ( ph /\ i e. ( ZZ>= ` -u j ) /\ j e. ( 1 ... N ) ) -> A e. CC )
5 fzsum2sub.3 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) ) -> B = 0 )
6 fzsum2sub.4 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( 0 ..^ j ) ) -> B = 0 )
7 simpr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
8 7 elfzelzd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ZZ )
9 0zd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> 0 e. ZZ )
10 1 nn0zd 
 |-  ( ph -> M e. ZZ )
11 10 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> M e. ZZ )
12 simpll 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ i e. ( 0 ... M ) ) -> ph )
13 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
14 nnssnn0 
 |-  NN C_ NN0
15 13 14 sstri 
 |-  ( 1 ... N ) C_ NN0
16 15 7 sselid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN0 )
17 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
18 16 17 eleqtrdi 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( ZZ>= ` 0 ) )
19 neg0 
 |-  -u 0 = 0
20 uzneg 
 |-  ( j e. ( ZZ>= ` 0 ) -> -u 0 e. ( ZZ>= ` -u j ) )
21 19 20 eqeltrrid 
 |-  ( j e. ( ZZ>= ` 0 ) -> 0 e. ( ZZ>= ` -u j ) )
22 fzss1 
 |-  ( 0 e. ( ZZ>= ` -u j ) -> ( 0 ... M ) C_ ( -u j ... M ) )
23 18 21 22 3syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... M ) C_ ( -u j ... M ) )
24 fzssuz 
 |-  ( -u j ... M ) C_ ( ZZ>= ` -u j )
25 23 24 sstrdi 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... M ) C_ ( ZZ>= ` -u j ) )
26 25 sselda 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ i e. ( 0 ... M ) ) -> i e. ( ZZ>= ` -u j ) )
27 7 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ i e. ( 0 ... M ) ) -> j e. ( 1 ... N ) )
28 12 26 27 4 syl3anc 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ i e. ( 0 ... M ) ) -> A e. CC )
29 8 9 11 28 3 fsumshft 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ i e. ( 0 ... M ) A = sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B )
30 1 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> M e. NN0 )
31 13 7 sselid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN )
32 31 nnnn0d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN0 )
33 30 32 nn0addcld 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + j ) e. NN0 )
34 33 nn0red 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + j ) e. RR )
35 34 ltp1d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + j ) < ( ( M + j ) + 1 ) )
36 fzdisj 
 |-  ( ( M + j ) < ( ( M + j ) + 1 ) -> ( ( j ... ( M + j ) ) i^i ( ( ( M + j ) + 1 ) ... ( M + N ) ) ) = (/) )
37 35 36 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( j ... ( M + j ) ) i^i ( ( ( M + j ) + 1 ) ... ( M + N ) ) ) = (/) )
38 2 nn0zd 
 |-  ( ph -> N e. ZZ )
39 10 38 zaddcld 
 |-  ( ph -> ( M + N ) e. ZZ )
40 39 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + N ) e. ZZ )
41 33 nn0zd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + j ) e. ZZ )
42 31 nnred 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. RR )
43 nn0addge2 
 |-  ( ( j e. RR /\ M e. NN0 ) -> j <_ ( M + j ) )
44 42 30 43 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j <_ ( M + j ) )
45 2 nn0red 
 |-  ( ph -> N e. RR )
46 45 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> N e. RR )
47 30 nn0red 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> M e. RR )
48 elfzle2 
 |-  ( j e. ( 1 ... N ) -> j <_ N )
49 48 adantl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j <_ N )
50 42 46 47 49 leadd2dd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + j ) <_ ( M + N ) )
51 8 40 41 44 50 elfzd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + j ) e. ( j ... ( M + N ) ) )
52 fzsplit 
 |-  ( ( M + j ) e. ( j ... ( M + N ) ) -> ( j ... ( M + N ) ) = ( ( j ... ( M + j ) ) u. ( ( ( M + j ) + 1 ) ... ( M + N ) ) ) )
53 51 52 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j ... ( M + N ) ) = ( ( j ... ( M + j ) ) u. ( ( ( M + j ) + 1 ) ... ( M + N ) ) ) )
54 fzfid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j ... ( M + N ) ) e. Fin )
55 simpll 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( j ... ( M + N ) ) ) -> ph )
56 7 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( j ... ( M + N ) ) ) -> j e. ( 1 ... N ) )
57 15 56 sselid 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( j ... ( M + N ) ) ) -> j e. NN0 )
58 fz2ssnn0 
 |-  ( j e. NN0 -> ( j ... ( M + N ) ) C_ NN0 )
59 57 58 syl 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( j ... ( M + N ) ) ) -> ( j ... ( M + N ) ) C_ NN0 )
60 simpr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( j ... ( M + N ) ) ) -> k e. ( j ... ( M + N ) ) )
61 59 60 sseldd 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( j ... ( M + N ) ) ) -> k e. NN0 )
62 3 eleq1d 
 |-  ( i = ( k - j ) -> ( A e. CC <-> B e. CC ) )
63 simpll 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` -u j ) ) /\ j e. ( 1 ... N ) ) -> ph )
64 simplr 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` -u j ) ) /\ j e. ( 1 ... N ) ) -> i e. ( ZZ>= ` -u j ) )
65 simpr 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` -u j ) ) /\ j e. ( 1 ... N ) ) -> j e. ( 1 ... N ) )
66 63 64 65 4 syl3anc 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` -u j ) ) /\ j e. ( 1 ... N ) ) -> A e. CC )
67 66 an32s 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ i e. ( ZZ>= ` -u j ) ) -> A e. CC )
68 67 ralrimiva 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> A. i e. ( ZZ>= ` -u j ) A e. CC )
69 68 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> A. i e. ( ZZ>= ` -u j ) A e. CC )
70 nnsscn 
 |-  NN C_ CC
71 13 70 sstri 
 |-  ( 1 ... N ) C_ CC
72 simplr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> j e. ( 1 ... N ) )
73 71 72 sselid 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> j e. CC )
74 simpr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> k e. NN0 )
75 74 nn0cnd 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> k e. CC )
76 73 75 negsubdi2d 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> -u ( j - k ) = ( k - j ) )
77 72 elfzelzd 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> j e. ZZ )
78 eluzmn 
 |-  ( ( j e. ZZ /\ k e. NN0 ) -> j e. ( ZZ>= ` ( j - k ) ) )
79 77 74 78 syl2anc 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> j e. ( ZZ>= ` ( j - k ) ) )
80 uzneg 
 |-  ( j e. ( ZZ>= ` ( j - k ) ) -> -u ( j - k ) e. ( ZZ>= ` -u j ) )
81 79 80 syl 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> -u ( j - k ) e. ( ZZ>= ` -u j ) )
82 76 81 eqeltrrd 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> ( k - j ) e. ( ZZ>= ` -u j ) )
83 62 69 82 rspcdva 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. NN0 ) -> B e. CC )
84 55 56 61 83 syl21anc 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( j ... ( M + N ) ) ) -> B e. CC )
85 37 53 54 84 fsumsplit 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( j ... ( M + N ) ) B = ( sum_ k e. ( j ... ( M + j ) ) B + sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) B ) )
86 8 zcnd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. CC )
87 86 addlidd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 + j ) = j )
88 87 oveq1d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 0 + j ) ... ( M + j ) ) = ( j ... ( M + j ) ) )
89 88 eqcomd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j ... ( M + j ) ) = ( ( 0 + j ) ... ( M + j ) ) )
90 89 sumeq1d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( j ... ( M + j ) ) B = sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B )
91 5 sumeq2dv 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) B = sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) 0 )
92 fzfi 
 |-  ( ( ( M + j ) + 1 ) ... ( M + N ) ) e. Fin
93 sumz 
 |-  ( ( ( ( ( M + j ) + 1 ) ... ( M + N ) ) C_ ( ZZ>= ` 0 ) \/ ( ( ( M + j ) + 1 ) ... ( M + N ) ) e. Fin ) -> sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) 0 = 0 )
94 93 olcs 
 |-  ( ( ( ( M + j ) + 1 ) ... ( M + N ) ) e. Fin -> sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) 0 = 0 )
95 92 94 ax-mp 
 |-  sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) 0 = 0
96 91 95 eqtrdi 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) B = 0 )
97 90 96 oveq12d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( sum_ k e. ( j ... ( M + j ) ) B + sum_ k e. ( ( ( M + j ) + 1 ) ... ( M + N ) ) B ) = ( sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B + 0 ) )
98 fzfid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 0 + j ) ... ( M + j ) ) e. Fin )
99 simpll 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> ph )
100 7 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> j e. ( 1 ... N ) )
101 elfzuz3 
 |-  ( j e. ( 1 ... N ) -> N e. ( ZZ>= ` j ) )
102 101 adantl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> N e. ( ZZ>= ` j ) )
103 eluzadd 
 |-  ( ( N e. ( ZZ>= ` j ) /\ M e. ZZ ) -> ( N + M ) e. ( ZZ>= ` ( j + M ) ) )
104 102 11 103 syl2anc 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( N + M ) e. ( ZZ>= ` ( j + M ) ) )
105 2 nn0cnd 
 |-  ( ph -> N e. CC )
106 105 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> N e. CC )
107 zsscn 
 |-  ZZ C_ CC
108 107 11 sselid 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> M e. CC )
109 106 108 addcomd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( N + M ) = ( M + N ) )
110 86 108 addcomd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j + M ) = ( M + j ) )
111 110 fveq2d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ZZ>= ` ( j + M ) ) = ( ZZ>= ` ( M + j ) ) )
112 104 109 111 3eltr3d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + N ) e. ( ZZ>= ` ( M + j ) ) )
113 112 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> ( M + N ) e. ( ZZ>= ` ( M + j ) ) )
114 fzss2 
 |-  ( ( M + N ) e. ( ZZ>= ` ( M + j ) ) -> ( j ... ( M + j ) ) C_ ( j ... ( M + N ) ) )
115 113 114 syl 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> ( j ... ( M + j ) ) C_ ( j ... ( M + N ) ) )
116 simpr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> k e. ( ( 0 + j ) ... ( M + j ) ) )
117 88 adantr 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> ( ( 0 + j ) ... ( M + j ) ) = ( j ... ( M + j ) ) )
118 116 117 eleqtrd 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> k e. ( j ... ( M + j ) ) )
119 115 118 sseldd 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> k e. ( j ... ( M + N ) ) )
120 99 100 119 61 syl21anc 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> k e. NN0 )
121 99 100 120 83 syl21anc 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( ( 0 + j ) ... ( M + j ) ) ) -> B e. CC )
122 98 121 fsumcl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B e. CC )
123 122 addridd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B + 0 ) = sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B )
124 85 97 123 3eqtrrd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B = sum_ k e. ( j ... ( M + N ) ) B )
125 fzval3 
 |-  ( ( M + N ) e. ZZ -> ( j ... ( M + N ) ) = ( j ..^ ( ( M + N ) + 1 ) ) )
126 40 125 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( j ... ( M + N ) ) = ( j ..^ ( ( M + N ) + 1 ) ) )
127 126 ineq2d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 0 ..^ j ) i^i ( j ... ( M + N ) ) ) = ( ( 0 ..^ j ) i^i ( j ..^ ( ( M + N ) + 1 ) ) ) )
128 fzodisj 
 |-  ( ( 0 ..^ j ) i^i ( j ..^ ( ( M + N ) + 1 ) ) ) = (/)
129 127 128 eqtrdi 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 0 ..^ j ) i^i ( j ... ( M + N ) ) ) = (/) )
130 40 peano2zd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( M + N ) + 1 ) e. ZZ )
131 32 nn0ge0d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> 0 <_ j )
132 130 zred 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( M + N ) + 1 ) e. RR )
133 40 zred 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + N ) e. RR )
134 nn0addge2 
 |-  ( ( N e. RR /\ M e. NN0 ) -> N <_ ( M + N ) )
135 45 1 134 syl2anc 
 |-  ( ph -> N <_ ( M + N ) )
136 135 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> N <_ ( M + N ) )
137 133 lep1d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( M + N ) <_ ( ( M + N ) + 1 ) )
138 46 133 132 136 137 letrd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> N <_ ( ( M + N ) + 1 ) )
139 42 46 132 49 138 letrd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j <_ ( ( M + N ) + 1 ) )
140 9 130 8 131 139 elfzd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. ( 0 ... ( ( M + N ) + 1 ) ) )
141 fzosplit 
 |-  ( j e. ( 0 ... ( ( M + N ) + 1 ) ) -> ( 0 ..^ ( ( M + N ) + 1 ) ) = ( ( 0 ..^ j ) u. ( j ..^ ( ( M + N ) + 1 ) ) ) )
142 140 141 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ..^ ( ( M + N ) + 1 ) ) = ( ( 0 ..^ j ) u. ( j ..^ ( ( M + N ) + 1 ) ) ) )
143 fzval3 
 |-  ( ( M + N ) e. ZZ -> ( 0 ... ( M + N ) ) = ( 0 ..^ ( ( M + N ) + 1 ) ) )
144 40 143 syl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... ( M + N ) ) = ( 0 ..^ ( ( M + N ) + 1 ) ) )
145 126 uneq2d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( ( 0 ..^ j ) u. ( j ... ( M + N ) ) ) = ( ( 0 ..^ j ) u. ( j ..^ ( ( M + N ) + 1 ) ) ) )
146 142 144 145 3eqtr4d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... ( M + N ) ) = ( ( 0 ..^ j ) u. ( j ... ( M + N ) ) ) )
147 fzfid 
 |-  ( ph -> ( 0 ... ( M + N ) ) e. Fin )
148 147 adantr 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 ... ( M + N ) ) e. Fin )
149 simpl 
 |-  ( ( ph /\ ( k e. ( 0 ... ( M + N ) ) /\ j e. ( 1 ... N ) ) ) -> ph )
150 7 adantrl 
 |-  ( ( ph /\ ( k e. ( 0 ... ( M + N ) ) /\ j e. ( 1 ... N ) ) ) -> j e. ( 1 ... N ) )
151 fz0ssnn0 
 |-  ( 0 ... ( M + N ) ) C_ NN0
152 simprl 
 |-  ( ( ph /\ ( k e. ( 0 ... ( M + N ) ) /\ j e. ( 1 ... N ) ) ) -> k e. ( 0 ... ( M + N ) ) )
153 151 152 sselid 
 |-  ( ( ph /\ ( k e. ( 0 ... ( M + N ) ) /\ j e. ( 1 ... N ) ) ) -> k e. NN0 )
154 149 150 153 83 syl21anc 
 |-  ( ( ph /\ ( k e. ( 0 ... ( M + N ) ) /\ j e. ( 1 ... N ) ) ) -> B e. CC )
155 154 anass1rs 
 |-  ( ( ( ph /\ j e. ( 1 ... N ) ) /\ k e. ( 0 ... ( M + N ) ) ) -> B e. CC )
156 129 146 148 155 fsumsplit 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( 0 ... ( M + N ) ) B = ( sum_ k e. ( 0 ..^ j ) B + sum_ k e. ( j ... ( M + N ) ) B ) )
157 6 sumeq2dv 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( 0 ..^ j ) B = sum_ k e. ( 0 ..^ j ) 0 )
158 fzofi 
 |-  ( 0 ..^ j ) e. Fin
159 sumz 
 |-  ( ( ( 0 ..^ j ) C_ ( ZZ>= ` 0 ) \/ ( 0 ..^ j ) e. Fin ) -> sum_ k e. ( 0 ..^ j ) 0 = 0 )
160 159 olcs 
 |-  ( ( 0 ..^ j ) e. Fin -> sum_ k e. ( 0 ..^ j ) 0 = 0 )
161 158 160 ax-mp 
 |-  sum_ k e. ( 0 ..^ j ) 0 = 0
162 157 161 eqtrdi 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( 0 ..^ j ) B = 0 )
163 162 oveq1d 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( sum_ k e. ( 0 ..^ j ) B + sum_ k e. ( j ... ( M + N ) ) B ) = ( 0 + sum_ k e. ( j ... ( M + N ) ) B ) )
164 54 84 fsumcl 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( j ... ( M + N ) ) B e. CC )
165 164 addlidd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( 0 + sum_ k e. ( j ... ( M + N ) ) B ) = sum_ k e. ( j ... ( M + N ) ) B )
166 156 163 165 3eqtrrd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( j ... ( M + N ) ) B = sum_ k e. ( 0 ... ( M + N ) ) B )
167 124 166 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ k e. ( ( 0 + j ) ... ( M + j ) ) B = sum_ k e. ( 0 ... ( M + N ) ) B )
168 29 167 eqtrd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> sum_ i e. ( 0 ... M ) A = sum_ k e. ( 0 ... ( M + N ) ) B )
169 168 sumeq2dv 
 |-  ( ph -> sum_ j e. ( 1 ... N ) sum_ i e. ( 0 ... M ) A = sum_ j e. ( 1 ... N ) sum_ k e. ( 0 ... ( M + N ) ) B )
170 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
171 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
172 28 anasss 
 |-  ( ( ph /\ ( j e. ( 1 ... N ) /\ i e. ( 0 ... M ) ) ) -> A e. CC )
173 172 ancom2s 
 |-  ( ( ph /\ ( i e. ( 0 ... M ) /\ j e. ( 1 ... N ) ) ) -> A e. CC )
174 170 171 173 fsumcom 
 |-  ( ph -> sum_ i e. ( 0 ... M ) sum_ j e. ( 1 ... N ) A = sum_ j e. ( 1 ... N ) sum_ i e. ( 0 ... M ) A )
175 147 171 154 fsumcom 
 |-  ( ph -> sum_ k e. ( 0 ... ( M + N ) ) sum_ j e. ( 1 ... N ) B = sum_ j e. ( 1 ... N ) sum_ k e. ( 0 ... ( M + N ) ) B )
176 169 174 175 3eqtr4d 
 |-  ( ph -> sum_ i e. ( 0 ... M ) sum_ j e. ( 1 ... N ) A = sum_ k e. ( 0 ... ( M + N ) ) sum_ j e. ( 1 ... N ) B )