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

Theorem fsum2dsub 34600
Description: Lemma for breprexp 34626- 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 simpr 484 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
21elfzelzd 13561 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℤ)
3 0zd 12622 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → 0 ∈ ℤ)
4 fzsum2sub.m . . . . . . 7 (𝜑𝑀 ∈ ℕ0)
54nn0zd 12636 . . . . . 6 (𝜑𝑀 ∈ ℤ)
65adantr 480 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℤ)
7 simpll 767 . . . . . 6 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝜑)
8 fz1ssnn 13591 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℕ
9 nnssnn0 12526 . . . . . . . . . . . 12 ℕ ⊆ ℕ0
108, 9sstri 4004 . . . . . . . . . . 11 (1...𝑁) ⊆ ℕ0
1110, 1sselid 3992 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ0)
12 nn0uz 12917 . . . . . . . . . 10 0 = (ℤ‘0)
1311, 12eleqtrdi 2848 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (ℤ‘0))
14 neg0 11552 . . . . . . . . . 10 -0 = 0
15 uzneg 12895 . . . . . . . . . 10 (𝑗 ∈ (ℤ‘0) → -0 ∈ (ℤ‘-𝑗))
1614, 15eqeltrrid 2843 . . . . . . . . 9 (𝑗 ∈ (ℤ‘0) → 0 ∈ (ℤ‘-𝑗))
17 fzss1 13599 . . . . . . . . 9 (0 ∈ (ℤ‘-𝑗) → (0...𝑀) ⊆ (-𝑗...𝑀))
1813, 16, 173syl 18 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (0...𝑀) ⊆ (-𝑗...𝑀))
19 fzssuz 13601 . . . . . . . 8 (-𝑗...𝑀) ⊆ (ℤ‘-𝑗)
2018, 19sstrdi 4007 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (0...𝑀) ⊆ (ℤ‘-𝑗))
2120sselda 3994 . . . . . 6 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (ℤ‘-𝑗))
221adantr 480 . . . . . 6 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝑗 ∈ (1...𝑁))
23 fzsum2sub.2 . . . . . 6 ((𝜑𝑖 ∈ (ℤ‘-𝑗) ∧ 𝑗 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
247, 21, 22, 23syl3anc 1370 . . . . 5 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (0...𝑀)) → 𝐴 ∈ ℂ)
25 fzsum2sub.1 . . . . 5 (𝑖 = (𝑘𝑗) → 𝐴 = 𝐵)
262, 3, 6, 24, 25fsumshft 15812 . . . 4 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑖 ∈ (0...𝑀)𝐴 = Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵)
274adantr 480 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℕ0)
288, 1sselid 3992 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ)
2928nnnn0d 12584 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℕ0)
3027, 29nn0addcld 12588 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ ℕ0)
3130nn0red 12585 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ ℝ)
3231ltp1d 12195 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) < ((𝑀 + 𝑗) + 1))
33 fzdisj 13587 . . . . . . . 8 ((𝑀 + 𝑗) < ((𝑀 + 𝑗) + 1) → ((𝑗...(𝑀 + 𝑗)) ∩ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) = ∅)
3432, 33syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝑗...(𝑀 + 𝑗)) ∩ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) = ∅)
35 fzsum2sub.n . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
3635nn0zd 12636 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℤ)
375, 36zaddcld 12723 . . . . . . . . . 10 (𝜑 → (𝑀 + 𝑁) ∈ ℤ)
3837adantr 480 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ∈ ℤ)
3930nn0zd 12636 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ ℤ)
4028nnred 12278 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℝ)
41 nn0addge2 12570 . . . . . . . . . 10 ((𝑗 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → 𝑗 ≤ (𝑀 + 𝑗))
4240, 27, 41syl2anc 584 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ≤ (𝑀 + 𝑗))
4335nn0red 12585 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℝ)
4443adantr 480 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℝ)
4527nn0red 12585 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℝ)
46 elfzle2 13564 . . . . . . . . . . 11 (𝑗 ∈ (1...𝑁) → 𝑗𝑁)
4746adantl 481 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗𝑁)
4840, 44, 45, 47leadd2dd 11875 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ≤ (𝑀 + 𝑁))
492, 38, 39, 42, 48elfzd 13551 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑗) ∈ (𝑗...(𝑀 + 𝑁)))
50 fzsplit 13586 . . . . . . . 8 ((𝑀 + 𝑗) ∈ (𝑗...(𝑀 + 𝑁)) → (𝑗...(𝑀 + 𝑁)) = ((𝑗...(𝑀 + 𝑗)) ∪ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))))
5149, 50syl 17 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑁)) = ((𝑗...(𝑀 + 𝑗)) ∪ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))))
52 fzfid 14010 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑁)) ∈ Fin)
53 simpll 767 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝜑)
541adantr 480 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑗 ∈ (1...𝑁))
5510, 54sselid 3992 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑗 ∈ ℕ0)
56 fz2ssnn0 32793 . . . . . . . . . 10 (𝑗 ∈ ℕ0 → (𝑗...(𝑀 + 𝑁)) ⊆ ℕ0)
5755, 56syl 17 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → (𝑗...(𝑀 + 𝑁)) ⊆ ℕ0)
58 simpr 484 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑘 ∈ (𝑗...(𝑀 + 𝑁)))
5957, 58sseldd 3995 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝑘 ∈ ℕ0)
6025eleq1d 2823 . . . . . . . . 9 (𝑖 = (𝑘𝑗) → (𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ))
61 simpll 767 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝜑)
62 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝑖 ∈ (ℤ‘-𝑗))
63 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (1...𝑁))
6461, 62, 63, 23syl3anc 1370 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (ℤ‘-𝑗)) ∧ 𝑗 ∈ (1...𝑁)) → 𝐴 ∈ ℂ)
6564an32s 652 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑖 ∈ (ℤ‘-𝑗)) → 𝐴 ∈ ℂ)
6665ralrimiva 3143 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → ∀𝑖 ∈ (ℤ‘-𝑗)𝐴 ∈ ℂ)
6766adantr 480 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → ∀𝑖 ∈ (ℤ‘-𝑗)𝐴 ∈ ℂ)
68 nnsscn 12268 . . . . . . . . . . . . 13 ℕ ⊆ ℂ
698, 68sstri 4004 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℂ
70 simplr 769 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ (1...𝑁))
7169, 70sselid 3992 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ ℂ)
72 simpr 484 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
7372nn0cnd 12586 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℂ)
7471, 73negsubdi2d 11633 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → -(𝑗𝑘) = (𝑘𝑗))
7570elfzelzd 13561 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ ℤ)
76 eluzmn 12882 . . . . . . . . . . . 12 ((𝑗 ∈ ℤ ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ (ℤ‘(𝑗𝑘)))
7775, 72, 76syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝑗 ∈ (ℤ‘(𝑗𝑘)))
78 uzneg 12895 . . . . . . . . . . 11 (𝑗 ∈ (ℤ‘(𝑗𝑘)) → -(𝑗𝑘) ∈ (ℤ‘-𝑗))
7977, 78syl 17 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → -(𝑗𝑘) ∈ (ℤ‘-𝑗))
8074, 79eqeltrrd 2839 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → (𝑘𝑗) ∈ (ℤ‘-𝑗))
8160, 67, 80rspcdva 3622 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈ ℂ)
8253, 54, 59, 81syl21anc 838 . . . . . . 7 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (𝑗...(𝑀 + 𝑁))) → 𝐵 ∈ ℂ)
8334, 51, 52, 82fsumsplit 15773 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵 = (Σ𝑘 ∈ (𝑗...(𝑀 + 𝑗))𝐵 + Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵))
842zcnd 12720 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ ℂ)
8584addlidd 11459 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → (0 + 𝑗) = 𝑗)
8685oveq1d 7445 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → ((0 + 𝑗)...(𝑀 + 𝑗)) = (𝑗...(𝑀 + 𝑗)))
8786eqcomd 2740 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑗)) = ((0 + 𝑗)...(𝑀 + 𝑗)))
8887sumeq1d 15732 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑗))𝐵 = Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵)
89 fzsum2sub.3 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))) → 𝐵 = 0)
9089sumeq2dv 15734 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵 = Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0)
91 fzfi 14009 . . . . . . . . 9 (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ∈ Fin
92 sumz 15754 . . . . . . . . . 10 (((((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ⊆ (ℤ‘0) ∨ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ∈ Fin) → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0 = 0)
9392olcs 876 . . . . . . . . 9 ((((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁)) ∈ Fin → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0 = 0)
9491, 93ax-mp 5 . . . . . . . 8 Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))0 = 0
9590, 94eqtrdi 2790 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵 = 0)
9688, 95oveq12d 7448 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (Σ𝑘 ∈ (𝑗...(𝑀 + 𝑗))𝐵 + Σ𝑘 ∈ (((𝑀 + 𝑗) + 1)...(𝑀 + 𝑁))𝐵) = (Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 + 0))
97 fzfid 14010 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → ((0 + 𝑗)...(𝑀 + 𝑗)) ∈ Fin)
98 simpll 767 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝜑)
991adantr 480 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑗 ∈ (1...𝑁))
100 elfzuz3 13557 . . . . . . . . . . . . . . . 16 (𝑗 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝑗))
101100adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ (ℤ𝑗))
102 eluzadd 12904 . . . . . . . . . . . . . . 15 ((𝑁 ∈ (ℤ𝑗) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ‘(𝑗 + 𝑀)))
103101, 6, 102syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑁 + 𝑀) ∈ (ℤ‘(𝑗 + 𝑀)))
10435nn0cnd 12586 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℂ)
105104adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ∈ ℂ)
106 zsscn 12618 . . . . . . . . . . . . . . . 16 ℤ ⊆ ℂ
107106, 6sselid 3992 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑀 ∈ ℂ)
108105, 107addcomd 11460 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑁 + 𝑀) = (𝑀 + 𝑁))
10984, 107addcomd 11460 . . . . . . . . . . . . . . 15 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗 + 𝑀) = (𝑀 + 𝑗))
110109fveq2d 6910 . . . . . . . . . . . . . 14 ((𝜑𝑗 ∈ (1...𝑁)) → (ℤ‘(𝑗 + 𝑀)) = (ℤ‘(𝑀 + 𝑗)))
111103, 108, 1103eltr3d 2852 . . . . . . . . . . . . 13 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ∈ (ℤ‘(𝑀 + 𝑗)))
112111adantr 480 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → (𝑀 + 𝑁) ∈ (ℤ‘(𝑀 + 𝑗)))
113 fzss2 13600 . . . . . . . . . . . 12 ((𝑀 + 𝑁) ∈ (ℤ‘(𝑀 + 𝑗)) → (𝑗...(𝑀 + 𝑗)) ⊆ (𝑗...(𝑀 + 𝑁)))
114112, 113syl 17 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → (𝑗...(𝑀 + 𝑗)) ⊆ (𝑗...(𝑀 + 𝑁)))
115 simpr 484 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗)))
11686adantr 480 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → ((0 + 𝑗)...(𝑀 + 𝑗)) = (𝑗...(𝑀 + 𝑗)))
117115, 116eleqtrd 2840 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ (𝑗...(𝑀 + 𝑗)))
118114, 117sseldd 3995 . . . . . . . . . 10 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ (𝑗...(𝑀 + 𝑁)))
11998, 99, 118, 59syl21anc 838 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝑘 ∈ ℕ0)
12098, 99, 119, 81syl21anc 838 . . . . . . . 8 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))) → 𝐵 ∈ ℂ)
12197, 120fsumcl 15765 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 ∈ ℂ)
122121addridd 11458 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 + 0) = Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵)
12383, 96, 1223eqtrrd 2779 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 = Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵)
124 fzval3 13769 . . . . . . . . . 10 ((𝑀 + 𝑁) ∈ ℤ → (𝑗...(𝑀 + 𝑁)) = (𝑗..^((𝑀 + 𝑁) + 1)))
12538, 124syl 17 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑗...(𝑀 + 𝑁)) = (𝑗..^((𝑀 + 𝑁) + 1)))
126125ineq2d 4227 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → ((0..^𝑗) ∩ (𝑗...(𝑀 + 𝑁))) = ((0..^𝑗) ∩ (𝑗..^((𝑀 + 𝑁) + 1))))
127 fzodisj 13729 . . . . . . . 8 ((0..^𝑗) ∩ (𝑗..^((𝑀 + 𝑁) + 1))) = ∅
128126, 127eqtrdi 2790 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → ((0..^𝑗) ∩ (𝑗...(𝑀 + 𝑁))) = ∅)
12938peano2zd 12722 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝑀 + 𝑁) + 1) ∈ ℤ)
13029nn0ge0d 12587 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 0 ≤ 𝑗)
131129zred 12719 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → ((𝑀 + 𝑁) + 1) ∈ ℝ)
13238zred 12719 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ∈ ℝ)
133 nn0addge2 12570 . . . . . . . . . . . . . 14 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℕ0) → 𝑁 ≤ (𝑀 + 𝑁))
13443, 4, 133syl2anc 584 . . . . . . . . . . . . 13 (𝜑𝑁 ≤ (𝑀 + 𝑁))
135134adantr 480 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ≤ (𝑀 + 𝑁))
136132lep1d 12196 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (1...𝑁)) → (𝑀 + 𝑁) ≤ ((𝑀 + 𝑁) + 1))
13744, 132, 131, 135, 136letrd 11415 . . . . . . . . . . 11 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑁 ≤ ((𝑀 + 𝑁) + 1))
13840, 44, 131, 47, 137letrd 11415 . . . . . . . . . 10 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ≤ ((𝑀 + 𝑁) + 1))
1393, 129, 2, 130, 138elfzd 13551 . . . . . . . . 9 ((𝜑𝑗 ∈ (1...𝑁)) → 𝑗 ∈ (0...((𝑀 + 𝑁) + 1)))
140 fzosplit 13728 . . . . . . . . 9 (𝑗 ∈ (0...((𝑀 + 𝑁) + 1)) → (0..^((𝑀 + 𝑁) + 1)) = ((0..^𝑗) ∪ (𝑗..^((𝑀 + 𝑁) + 1))))
141139, 140syl 17 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (0..^((𝑀 + 𝑁) + 1)) = ((0..^𝑗) ∪ (𝑗..^((𝑀 + 𝑁) + 1))))
142 fzval3 13769 . . . . . . . . 9 ((𝑀 + 𝑁) ∈ ℤ → (0...(𝑀 + 𝑁)) = (0..^((𝑀 + 𝑁) + 1)))
14338, 142syl 17 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑀 + 𝑁)) = (0..^((𝑀 + 𝑁) + 1)))
144125uneq2d 4177 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → ((0..^𝑗) ∪ (𝑗...(𝑀 + 𝑁))) = ((0..^𝑗) ∪ (𝑗..^((𝑀 + 𝑁) + 1))))
145141, 143, 1443eqtr4d 2784 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑀 + 𝑁)) = ((0..^𝑗) ∪ (𝑗...(𝑀 + 𝑁))))
146 fzfid 14010 . . . . . . . 8 (𝜑 → (0...(𝑀 + 𝑁)) ∈ Fin)
147146adantr 480 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → (0...(𝑀 + 𝑁)) ∈ Fin)
148 simpl 482 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝜑)
1491adantrl 716 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝑗 ∈ (1...𝑁))
150 fz0ssnn0 13658 . . . . . . . . . 10 (0...(𝑀 + 𝑁)) ⊆ ℕ0
151 simprl 771 . . . . . . . . . 10 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝑘 ∈ (0...(𝑀 + 𝑁)))
152150, 151sselid 3992 . . . . . . . . 9 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝑘 ∈ ℕ0)
153148, 149, 152, 81syl21anc 838 . . . . . . . 8 ((𝜑 ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑗 ∈ (1...𝑁))) → 𝐵 ∈ ℂ)
154153anass1rs 655 . . . . . . 7 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → 𝐵 ∈ ℂ)
155128, 145, 147, 154fsumsplit 15773 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵 = (Σ𝑘 ∈ (0..^𝑗)𝐵 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵))
156 fzsum2sub.4 . . . . . . . . 9 (((𝜑𝑗 ∈ (1...𝑁)) ∧ 𝑘 ∈ (0..^𝑗)) → 𝐵 = 0)
157156sumeq2dv 15734 . . . . . . . 8 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (0..^𝑗)𝐵 = Σ𝑘 ∈ (0..^𝑗)0)
158 fzofi 14011 . . . . . . . . 9 (0..^𝑗) ∈ Fin
159 sumz 15754 . . . . . . . . . 10 (((0..^𝑗) ⊆ (ℤ‘0) ∨ (0..^𝑗) ∈ Fin) → Σ𝑘 ∈ (0..^𝑗)0 = 0)
160159olcs 876 . . . . . . . . 9 ((0..^𝑗) ∈ Fin → Σ𝑘 ∈ (0..^𝑗)0 = 0)
161158, 160ax-mp 5 . . . . . . . 8 Σ𝑘 ∈ (0..^𝑗)0 = 0
162157, 161eqtrdi 2790 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (0..^𝑗)𝐵 = 0)
163162oveq1d 7445 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (Σ𝑘 ∈ (0..^𝑗)𝐵 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵) = (0 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵))
16452, 82fsumcl 15765 . . . . . . 7 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵 ∈ ℂ)
165164addlidd 11459 . . . . . 6 ((𝜑𝑗 ∈ (1...𝑁)) → (0 + Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵) = Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵)
166155, 163, 1653eqtrrd 2779 . . . . 5 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ (𝑗...(𝑀 + 𝑁))𝐵 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
167123, 166eqtrd 2774 . . . 4 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑘 ∈ ((0 + 𝑗)...(𝑀 + 𝑗))𝐵 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
16826, 167eqtrd 2774 . . 3 ((𝜑𝑗 ∈ (1...𝑁)) → Σ𝑖 ∈ (0...𝑀)𝐴 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
169168sumeq2dv 15734 . 2 (𝜑 → Σ𝑗 ∈ (1...𝑁𝑖 ∈ (0...𝑀)𝐴 = Σ𝑗 ∈ (1...𝑁𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
170 fzfid 14010 . . 3 (𝜑 → (0...𝑀) ∈ Fin)
171 fzfid 14010 . . 3 (𝜑 → (1...𝑁) ∈ Fin)
17224anasss 466 . . . 4 ((𝜑 ∧ (𝑗 ∈ (1...𝑁) ∧ 𝑖 ∈ (0...𝑀))) → 𝐴 ∈ ℂ)
173172ancom2s 650 . . 3 ((𝜑 ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑗 ∈ (1...𝑁))) → 𝐴 ∈ ℂ)
174170, 171, 173fsumcom 15807 . 2 (𝜑 → Σ𝑖 ∈ (0...𝑀𝑗 ∈ (1...𝑁)𝐴 = Σ𝑗 ∈ (1...𝑁𝑖 ∈ (0...𝑀)𝐴)
175146, 171, 153fsumcom 15807 . 2 (𝜑 → Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑗 ∈ (1...𝑁)𝐵 = Σ𝑗 ∈ (1...𝑁𝑘 ∈ (0...(𝑀 + 𝑁))𝐵)
176169, 174, 1753eqtr4d 2784 1 (𝜑 → Σ𝑖 ∈ (0...𝑀𝑗 ∈ (1...𝑁)𝐴 = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑗 ∈ (1...𝑁)𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1536  wcel 2105  wral 3058  cun 3960  cin 3961  wss 3962  c0 4338   class class class wbr 5147  cfv 6562  (class class class)co 7430  Fincfn 8983  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155   < clt 11292  cle 11293  cmin 11489  -cneg 11490  cn 12263  0cn0 12523  cz 12610  cuz 12875  ...cfz 13543  ..^cfzo 13690  Σcsu 15718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-n0 12524  df-z 12611  df-uz 12876  df-rp 13032  df-fz 13544  df-fzo 13691  df-seq 14039  df-exp 14099  df-hash 14366  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-clim 15520  df-sum 15719
This theorem is referenced by:  breprexplemc  34625
  Copyright terms: Public domain W3C validator