Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fsum2dsub Structured version   Visualization version   GIF version

Theorem fsum2dsub 32054
 Description: Lemma for breprexp 32080- Re-index a double sum, using difference of the initial indices. (Contributed by Thierry Arnoux, 7-Dec-2021.)
Hypotheses
Ref Expression
fzsum2sub.m (𝜑𝑀 ∈ ℕ0)
fzsum2sub.n (𝜑𝑁 ∈ ℕ0)
fzsum2sub.1 (𝑖 = (𝑘𝑗) → 𝐴 = 𝐵)
fzsum2sub.2 ((𝜑𝑖 ∈ (ℤ‘-𝑗) ∧ 𝑗 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
fzsum2sub.3 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) → 𝐵 = 0)
fzsum2sub.4 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0..^𝑗)) → 𝐵 = 0)
Assertion
Ref Expression
fsum2dsub (𝜑 → Σ𝑖 ∈ (0...𝑀𝑗 ∈ (1...𝑁)𝐴 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑗 ∈ (1...𝑁)𝐵)
Distinct variable groups:   𝐴,𝑘   𝐵,𝑖   𝑖,𝑀,𝑗,𝑘   𝑖,𝑁,𝑗,𝑘   𝜑,𝑖,𝑗,𝑘
Allowed substitution hints:   𝐴(𝑖,𝑗)   𝐵(𝑗,𝑘)

Proof of Theorem fsum2dsub
StepHypRef Expression
1 fzssz 12924 . . . . . 6 (1...𝑁) ⊆ ℤ
2 simpr 488 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
31, 2sseldi 3915 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ)
4 0zd 12001 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → 0 ∈ ℤ)
5 fzsum2sub.m . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
65nn0zd 12093 . . . . . 6 (𝜑𝑀 ∈ ℤ)
76adantr 484 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℤ)
8 simpll 766 . . . . . 6 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝜑)
9 fz1ssnn 12953 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℕ
10 nnssnn0 11906 . . . . . . . . . . . 12 ℕ ⊆ ℕ0
119, 10sstri 3926 . . . . . . . . . . 11 (1...𝑁) ⊆ ℕ0
1211, 2sseldi 3915 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ0)
13 nn0uz 12288 . . . . . . . . . 10 0 = (ℤ‘0)
1412, 13eleqtrdi 2900 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (ℤ‘0))
15 neg0 10939 . . . . . . . . . 10 -0 = 0
16 uzneg 12271 . . . . . . . . . 10 (𝑗 ∈ (ℤ‘0) → -0 ∈ (ℤ‘-𝑗))
1715, 16eqeltrrid 2895 . . . . . . . . 9 (𝑗 ∈ (ℤ‘0) → 0 ∈ (ℤ‘-𝑗))
18 fzss1 12961 . . . . . . . . 9 (0 ∈ (ℤ‘-𝑗) → (0...𝑀) ⊆ (-𝑗...𝑀))
1914, 17, 183syl 18 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (0...𝑀) ⊆ (-𝑗...𝑀))
20 fzssuz 12963 . . . . . . . 8 (-𝑗...𝑀) ⊆ (ℤ‘-𝑗)
2119, 20sstrdi 3929 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (0...𝑀) ⊆ (ℤ‘-𝑗))
2221sselda 3917 . . . . . 6 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (ℤ‘-𝑗))
232adantr 484 . . . . . 6 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝑗 ∈ (1...𝑁))
24 fzsum2sub.2 . . . . . 6 ((𝜑𝑖 ∈ (ℤ‘-𝑗) ∧ 𝑗 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
258, 22, 23, 24syl3anc 1368 . . . . 5 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℂ)
26 fzsum2sub.1 . . . . 5 (𝑖 = (𝑘𝑗) → 𝐴 = 𝐵)
273, 4, 7, 25, 26fsumshft 15147 . . . 4 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑖 ∈ (0...𝑀)𝐴 = Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵)
285adantr 484 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℕ0)
299, 2sseldi 3915 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
3029nnnn0d 11963 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ0)
3128, 30nn0addcld 11967 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ ℕ0)
3231nn0red 11964 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ ℝ)
3332ltp1d 11577 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) < ((𝑀 + 𝑗) + 1))
34 fzdisj 12949 . . . . . . . 8 ((𝑀 + 𝑗) < ((𝑀 + 𝑗) + 1) → ((𝑗...(𝑀 + 𝑗)) ∩ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) = ∅)
3533, 34syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝑗...(𝑀 + 𝑗)) ∩ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) = ∅)
36 fzsum2sub.n . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
3736nn0zd 12093 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
386, 37zaddcld 12099 . . . . . . . . . 10 (𝜑 → (𝑀 + 𝑁) ∈ ℤ)
3938adantr 484 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ∈ ℤ)
4031nn0zd 12093 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ ℤ)
4129nnred 11658 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℝ)
42 nn0addge2 11950 . . . . . . . . . 10 ((𝑗 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → 𝑗 ≤ (𝑀 + 𝑗))
4341, 28, 42syl2anc 587 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ≤ (𝑀 + 𝑗))
4436nn0red 11964 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
4544adantr 484 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℝ)
4628nn0red 11964 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℝ)
47 elfzle2 12926 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑁) → 𝑗𝑁)
4847adantl 485 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗𝑁)
4941, 45, 46, 48leadd2dd 11262 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ≤ (𝑀 + 𝑁))
50 elfz4 12915 . . . . . . . . 9 (((𝑗 ∈ ℤ ∧ (𝑀 + 𝑁) ∈ ℤ ∧ (𝑀 + 𝑗) ∈ ℤ) ∧ (𝑗 ≤ (𝑀 + 𝑗) ∧ (𝑀 + 𝑗) ≤ (𝑀 + 𝑁))) → (𝑀 + 𝑗) ∈ (𝑗...(𝑀 + 𝑁)))
513, 39, 40, 43, 49, 50syl32anc 1375 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ (𝑗...(𝑀 + 𝑁)))
52 fzsplit 12948 . . . . . . . 8 ((𝑀 + 𝑗) ∈ (𝑗...(𝑀 + 𝑁)) → (𝑗...(𝑀 + 𝑁)) = ((𝑗...(𝑀 + 𝑗)) ∪ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))))
5351, 52syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑁)) = ((𝑗...(𝑀 + 𝑗)) ∪ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))))
54 fzfid 13356 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑁)) ∈ Fin)
55 simpll 766 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝜑)
562adantr 484 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑗 ∈ (1...𝑁))
5711, 56sseldi 3915 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑗 ∈ ℕ0)
58 fz2ssnn0 30578 . . . . . . . . . 10 (𝑗 ∈ ℕ0 → (𝑗...(𝑀 + 𝑁)) ⊆ ℕ0)
5957, 58syl 17 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → (𝑗...(𝑀 + 𝑁)) ⊆ ℕ0)
60 simpr 488 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑘 ∈ (𝑗...(𝑀 + 𝑁)))
6159, 60sseldd 3918 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑘 ∈ ℕ0)
6226eleq1d 2874 . . . . . . . . 9 (𝑖 = (𝑘𝑗) → (𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ))
63 simpll 766 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝜑)
64 simplr 768 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (ℤ‘-𝑗))
65 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
6663, 64, 65, 24syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
6766an32s 651 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (ℤ‘-𝑗)) → 𝐴 ∈ ℂ)
6867ralrimiva 3149 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → ∀𝑖 ∈ (ℤ‘-𝑗)𝐴 ∈ ℂ)
6968adantr 484 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → ∀𝑖 ∈ (ℤ‘-𝑗)𝐴 ∈ ℂ)
70 nnsscn 11648 . . . . . . . . . . . . 13 ℕ ⊆ ℂ
719, 70sstri 3926 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℂ
72 simplr 768 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ (1...𝑁))
7371, 72sseldi 3915 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ ℂ)
74 simpr 488 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
7574nn0cnd 11965 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
7673, 75negsubdi2d 11020 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → -(𝑗𝑘) = (𝑘𝑗))
771, 72sseldi 3915 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ ℤ)
78 eluzmn 12258 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ (ℤ‘(𝑗𝑘)))
7977, 74, 78syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ (ℤ‘(𝑗𝑘)))
80 uzneg 12271 . . . . . . . . . . 11 (𝑗 ∈ (ℤ‘(𝑗𝑘)) → -(𝑗𝑘) ∈ (ℤ‘-𝑗))
8179, 80syl 17 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → -(𝑗𝑘) ∈ (ℤ‘-𝑗))
8276, 81eqeltrrd 2891 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → (𝑘𝑗) ∈ (ℤ‘-𝑗))
8362, 69, 82rspcdva 3574 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
8455, 56, 61, 83syl21anc 836 . . . . . . 7 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝐵 ∈ ℂ)
8535, 53, 54, 84fsumsplit 15109 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵 = (Σ𝑘 ∈ (𝑗...(𝑀 + 𝑗))𝐵 + Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵))
863zcnd 12096 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℂ)
8786addid2d 10848 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → (0 + 𝑗) = 𝑗)
8887oveq1d 7160 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → ((0 + 𝑗)...(𝑀 + 𝑗)) = (𝑗...(𝑀 + 𝑗)))
8988eqcomd 2804 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑗)) = ((0 + 𝑗)...(𝑀 + 𝑗)))
9089sumeq1d 15070 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑗))𝐵 = Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵)
91 fzsum2sub.3 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) → 𝐵 = 0)
9291sumeq2dv 15072 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵 = Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0)
93 fzfi 13355 . . . . . . . . 9 (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ∈ Fin
94 sumz 15091 . . . . . . . . . 10 (((((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ⊆ (ℤ‘0) ∨ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ∈ Fin) → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0 = 0)
9594olcs 873 . . . . . . . . 9 ((((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ∈ Fin → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0 = 0)
9693, 95ax-mp 5 . . . . . . . 8 Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0 = 0
9792, 96eqtrdi 2849 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵 = 0)
9890, 97oveq12d 7163 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (Σ𝑘 ∈ (𝑗...(𝑀 + 𝑗))𝐵 + Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵) = (Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 + 0))
99 fzfid 13356 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → ((0 + 𝑗)...(𝑀 + 𝑗)) ∈ Fin)
100 simpll 766 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝜑)
1012adantr 484 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑗 ∈ (1...𝑁))
102 elfzuz3 12919 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝑗))
103102adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ (ℤ𝑗))
104 eluzadd 12281 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ𝑗) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ‘(𝑗 + 𝑀)))
105103, 7, 104syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑁 + 𝑀) ∈ (ℤ‘(𝑗 + 𝑀)))
10636nn0cnd 11965 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
107106adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
108 zsscn 11997 . . . . . . . . . . . . . . . 16 ℤ ⊆ ℂ
109108, 7sseldi 3915 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℂ)
110107, 109addcomd 10849 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑁 + 𝑀) = (𝑀 + 𝑁))
11186, 109addcomd 10849 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 + 𝑀) = (𝑀 + 𝑗))
112111fveq2d 6659 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑁)) → (ℤ‘(𝑗 + 𝑀)) = (ℤ‘(𝑀 + 𝑗)))
113105, 110, 1123eltr3d 2904 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ∈ (ℤ‘(𝑀 + 𝑗)))
114113adantr 484 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → (𝑀 + 𝑁) ∈ (ℤ‘(𝑀 + 𝑗)))
115 fzss2 12962 . . . . . . . . . . . 12 ((𝑀 + 𝑁) ∈ (ℤ‘(𝑀 + 𝑗)) → (𝑗...(𝑀 + 𝑗)) ⊆ (𝑗...(𝑀 + 𝑁)))
116114, 115syl 17 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → (𝑗...(𝑀 + 𝑗)) ⊆ (𝑗...(𝑀 + 𝑁)))
117 simpr 488 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗)))
11888adantr 484 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → ((0 + 𝑗)...(𝑀 + 𝑗)) = (𝑗...(𝑀 + 𝑗)))
119117, 118eleqtrd 2892 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ (𝑗...(𝑀 + 𝑗)))
120116, 119sseldd 3918 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ (𝑗...(𝑀 + 𝑁)))
121100, 101, 120, 61syl21anc 836 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ ℕ0)
122100, 101, 121, 83syl21anc 836 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝐵 ∈ ℂ)
12399, 122fsumcl 15102 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 ∈ ℂ)
124123addid1d 10847 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 + 0) = Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵)
12585, 98, 1243eqtrrd 2838 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 = Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵)
126 fzval3 13121 . . . . . . . . . 10 ((𝑀 + 𝑁) ∈ ℤ → (𝑗...(𝑀 + 𝑁)) = (𝑗..^((𝑀 + 𝑁) + 1)))
12739, 126syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑁)) = (𝑗..^((𝑀 + 𝑁) + 1)))
128127ineq2d 4142 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → ((0..^𝑗) ∩ (𝑗...(𝑀 + 𝑁))) = ((0..^𝑗) ∩ (𝑗..^((𝑀 + 𝑁) + 1))))
129 fzodisj 13086 . . . . . . . 8 ((0..^𝑗) ∩ (𝑗..^((𝑀 + 𝑁) + 1))) = ∅
130128, 129eqtrdi 2849 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → ((0..^𝑗) ∩ (𝑗...(𝑀 + 𝑁))) = ∅)
13139peano2zd 12098 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝑀 + 𝑁) + 1) ∈ ℤ)
13230nn0ge0d 11966 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 0 ≤ 𝑗)
133131zred 12095 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝑀 + 𝑁) + 1) ∈ ℝ)
13439zred 12095 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ∈ ℝ)
135 nn0addge2 11950 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → 𝑁 ≤ (𝑀 + 𝑁))
13644, 5, 135syl2anc 587 . . . . . . . . . . . . 13 (𝜑𝑁 ≤ (𝑀 + 𝑁))
137136adantr 484 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ≤ (𝑀 + 𝑁))
138134lep1d 11578 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ≤ ((𝑀 + 𝑁) + 1))
13945, 134, 133, 137, 138letrd 10804 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ≤ ((𝑀 + 𝑁) + 1))
14041, 45, 133, 48, 139letrd 10804 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ≤ ((𝑀 + 𝑁) + 1))
141 elfz4 12915 . . . . . . . . . 10 (((0 ∈ ℤ ∧ ((𝑀 + 𝑁) + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ) ∧ (0 ≤ 𝑗𝑗 ≤ ((𝑀 + 𝑁) + 1))) → 𝑗 ∈ (0...((𝑀 + 𝑁) + 1)))
1424, 131, 3, 132, 140, 141syl32anc 1375 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...((𝑀 + 𝑁) + 1)))
143 fzosplit 13085 . . . . . . . . 9 (𝑗 ∈ (0...((𝑀 + 𝑁) + 1)) → (0..^((𝑀 + 𝑁) + 1)) = ((0..^𝑗) ∪ (𝑗..^((𝑀 + 𝑁) + 1))))
144142, 143syl 17 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (0..^((𝑀 + 𝑁) + 1)) = ((0..^𝑗) ∪ (𝑗..^((𝑀 + 𝑁) + 1))))
145 fzval3 13121 . . . . . . . . 9 ((𝑀 + 𝑁) ∈ ℤ → (0...(𝑀 + 𝑁)) = (0..^((𝑀 + 𝑁) + 1)))
14639, 145syl 17 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑀 + 𝑁)) = (0..^((𝑀 + 𝑁) + 1)))
147127uneq2d 4093 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → ((0..^𝑗) ∪ (𝑗...(𝑀 + 𝑁))) = ((0..^𝑗) ∪ (𝑗..^((𝑀 + 𝑁) + 1))))
148144, 146, 1473eqtr4d 2843 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑀 + 𝑁)) = ((0..^𝑗) ∪ (𝑗...(𝑀 + 𝑁))))
149 fzfid 13356 . . . . . . . 8 (𝜑 → (0...(𝑀 + 𝑁)) ∈ Fin)
150149adantr 484 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑀 + 𝑁)) ∈ Fin)
151 simpl 486 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝜑)
1522adantrl 715 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝑗 ∈ (1...𝑁))
153 fz0ssnn0 13017 . . . . . . . . . 10 (0...(𝑀 + 𝑁)) ⊆ ℕ0
154 simprl 770 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝑘 ∈ (0...(𝑀 + 𝑁)))
155153, 154sseldi 3915 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝑘 ∈ ℕ0)
156151, 152, 155, 83syl21anc 836 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝐵 ∈ ℂ)
157156anass1rs 654 . . . . . . 7 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → 𝐵 ∈ ℂ)
158130, 148, 150, 157fsumsplit 15109 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵 = (Σ𝑘 ∈ (0..^𝑗)𝐵 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵))
159 fzsum2sub.4 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0..^𝑗)) → 𝐵 = 0)
160159sumeq2dv 15072 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (0..^𝑗)𝐵 = Σ𝑘 ∈ (0..^𝑗)0)
161 fzofi 13357 . . . . . . . . 9 (0..^𝑗) ∈ Fin
162 sumz 15091 . . . . . . . . . 10 (((0..^𝑗) ⊆ (ℤ‘0) ∨ (0..^𝑗) ∈ Fin) → Σ𝑘 ∈ (0..^𝑗)0 = 0)
163162olcs 873 . . . . . . . . 9 ((0..^𝑗) ∈ Fin → Σ𝑘 ∈ (0..^𝑗)0 = 0)
164161, 163ax-mp 5 . . . . . . . 8 Σ𝑘 ∈ (0..^𝑗)0 = 0
165160, 164eqtrdi 2849 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (0..^𝑗)𝐵 = 0)
166165oveq1d 7160 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0..^𝑗)𝐵 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵) = (0 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵))
16754, 84fsumcl 15102 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵 ∈ ℂ)
168167addid2d 10848 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (0 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵) = Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵)
169158, 166, 1683eqtrrd 2838 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
170125, 169eqtrd 2833 . . . 4 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
17127, 170eqtrd 2833 . . 3 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑖 ∈ (0...𝑀)𝐴 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
172171sumeq2dv 15072 . 2 (𝜑 → Σ𝑗 ∈ (1...𝑁𝑖 ∈ (0...𝑀)𝐴 = Σ𝑗 ∈ (1...𝑁𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
173 fzfid 13356 . . 3 (𝜑 → (0...𝑀) ∈ Fin)
174 fzfid 13356 . . 3 (𝜑 → (1...𝑁) ∈ Fin)
17525anasss 470 . . . 4 ((𝜑 ∧ (𝑗 ∈ (1...𝑁) ∧ 𝑖 ∈ (0...𝑀))) → 𝐴 ∈ ℂ)
176175ancom2s 649 . . 3 ((𝜑 ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (1...𝑁))) → 𝐴 ∈ ℂ)
177173, 174, 176fsumcom 15142 . 2 (𝜑 → Σ𝑖 ∈ (0...𝑀𝑗 ∈ (1...𝑁)𝐴 = Σ𝑗 ∈ (1...𝑁𝑖 ∈ (0...𝑀)𝐴)
178149, 174, 156fsumcom 15142 . 2 (𝜑 → Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑗 ∈ (1...𝑁)𝐵 = Σ𝑗 ∈ (1...𝑁𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
179172, 177, 1783eqtr4d 2843 1 (𝜑 → Σ𝑖 ∈ (0...𝑀𝑗 ∈ (1...𝑁)𝐴 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑗 ∈ (1...𝑁)𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ∀wral 3106   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4246   class class class wbr 5034  ‘cfv 6332  (class class class)co 7145  Fincfn 8510  ℂcc 10542  ℝcr 10543  0cc0 10544  1c1 10545   + caddc 10547   < clt 10682   ≤ cle 10683   − cmin 10877  -cneg 10878  ℕcn 11643  ℕ0cn0 11903  ℤcz 11989  ℤ≥cuz 12251  ...cfz 12905  ..^cfzo 13048  Σcsu 15054 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-inf2 9106  ax-cnex 10600  ax-resscn 10601  ax-1cn 10602  ax-icn 10603  ax-addcl 10604  ax-addrcl 10605  ax-mulcl 10606  ax-mulrcl 10607  ax-mulcom 10608  ax-addass 10609  ax-mulass 10610  ax-distr 10611  ax-i2m1 10612  ax-1ne0 10613  ax-1rid 10614  ax-rnegex 10615  ax-rrecex 10616  ax-cnre 10617  ax-pre-lttri 10618  ax-pre-lttrn 10619  ax-pre-ltadd 10620  ax-pre-mulgt0 10621  ax-pre-sup 10622 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-1o 8103  df-oadd 8107  df-er 8290  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-sup 8908  df-oi 8976  df-card 9370  df-pnf 10684  df-mnf 10685  df-xr 10686  df-ltxr 10687  df-le 10688  df-sub 10879  df-neg 10880  df-div 11305  df-nn 11644  df-2 11706  df-3 11707  df-n0 11904  df-z 11990  df-uz 12252  df-rp 12398  df-fz 12906  df-fzo 13049  df-seq 13385  df-exp 13446  df-hash 13707  df-cj 14470  df-re 14471  df-im 14472  df-sqrt 14606  df-abs 14607  df-clim 14857  df-sum 15055 This theorem is referenced by:  breprexplemc  32079
 Copyright terms: Public domain W3C validator