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