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 addlidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 addridd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 addlidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 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 ... 𝑁 ) 𝐵 )