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 ( 𝜑𝑀 ∈ ℕ0 )
fzsum2sub.n ( 𝜑𝑁 ∈ ℕ0 )
fzsum2sub.1 ( 𝑖 = ( 𝑘𝑗 ) → 𝐴 = 𝐵 )
fzsum2sub.2 ( ( 𝜑𝑖 ∈ ( ℤ ‘ - 𝑗 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fzsum2sub.3 ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( ( ( 𝑀 + 𝑗 ) + 1 ) ... ( 𝑀 + 𝑁 ) ) ) → 𝐵 = 0 )
fzsum2sub.4 ( ( ( 𝜑𝑗 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ..^ 𝑗 ) ) → 𝐵 = 0 )
Assertion fsum2dsub ( 𝜑 → Σ 𝑖 ∈ ( 0 ... 𝑀 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 0 ... ( 𝑀 + 𝑁 ) ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) 𝐵 )

Proof

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