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