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 addid2d
 |-  ( ( 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 addid1d
 |-  ( ( 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 addid2d
 |-  ( ( 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 )