Metamath Proof Explorer

Theorem isumsplit

Description: Split off the first N terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumsplit.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isumsplit.2 ⊢ 𝑊 = ( ℤ≥ ‘ 𝑁 )
isumsplit.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
isumsplit.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
isumsplit.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
isumsplit.6 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion isumsplit ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + Σ 𝑘 ∈ 𝑊 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isumsplit.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isumsplit.2 ⊢ 𝑊 = ( ℤ≥ ‘ 𝑁 )
3 isumsplit.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
4 isumsplit.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5 isumsplit.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
6 isumsplit.6 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
7 3 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
8 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
9 7 8 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
10 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
11 7 10 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
12 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
13 7 12 syl ⊢ ( 𝜑 → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
14 13 2 1 3sstr4g ⊢ ( 𝜑 → 𝑊 ⊆ 𝑍 )
15 14 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝑘 ∈ 𝑍 )
16 15 4 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
17 15 5 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → 𝐴 ∈ ℂ )
18 4 5 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
19 1 3 18 iserex ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ ) )
20 6 19 mpbid ⊢ ( 𝜑 → seq 𝑁 ( + , 𝐹 ) ∈ dom ⇝ )
21 2 11 16 17 20 isumclim2 ⊢ ( 𝜑 → seq 𝑁 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑊 𝐴 )
22 fzfid ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 − 1 ) ) ∈ Fin )
23 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
24 23 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ 𝑍 )
25 24 5 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
26 22 25 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 ∈ ℂ )
27 15 18 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
28 2 11 27 serf ⊢ ( 𝜑 → seq 𝑁 ( + , 𝐹 ) : 𝑊 ⟶ ℂ )
29 28 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
30 9 zred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
31 30 ltm1d ⊢ ( 𝜑 → ( 𝑀 − 1 ) < 𝑀 )
32 peano2zm ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 − 1 ) ∈ ℤ )
33 fzn ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 − 1 ) ∈ ℤ ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
34 9 32 33 syl2anc2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ ) )
35 31 34 mpbid ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑀 − 1 ) ) = ∅ )
36 35 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 = Σ 𝑘 ∈ ∅ 𝐴 )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 = Σ 𝑘 ∈ ∅ 𝐴 )
38 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐴 = 0
39 37 38 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 = 0 )
40 39 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( 0 + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) )
41 14 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → 𝑗 ∈ 𝑍 )
42 1 9 18 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
43 42 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
44 41 43 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
45 44 addid2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( 0 + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) )
46 40 45 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) )
47 oveq1 ⊢ ( 𝑁 = 𝑀 → ( 𝑁 − 1 ) = ( 𝑀 − 1 ) )
48 47 oveq2d ⊢ ( 𝑁 = 𝑀 → ( 𝑀 ... ( 𝑁 − 1 ) ) = ( 𝑀 ... ( 𝑀 − 1 ) ) )
49 48 sumeq1d ⊢ ( 𝑁 = 𝑀 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 )
50 seqeq1 ⊢ ( 𝑁 = 𝑀 → seq 𝑁 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐹 ) )
51 50 fveq1d ⊢ ( 𝑁 = 𝑀 → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) )
52 49 51 oveq12d ⊢ ( 𝑁 = 𝑀 → ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) )
53 52 eqeq2d ⊢ ( 𝑁 = 𝑀 → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑀 − 1 ) ) 𝐴 + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ) ) )
54 46 53 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( 𝑁 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ) ) )
55 addcl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ) → ( 𝑘 + 𝑚 ) ∈ ℂ )
56 55 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ) ) → ( 𝑘 + 𝑚 ) ∈ ℂ )
57 addass ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 𝑘 + 𝑚 ) + 𝑥 ) = ( 𝑘 + ( 𝑚 + 𝑥 ) ) )
58 57 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑚 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( ( 𝑘 + 𝑚 ) + 𝑥 ) = ( 𝑘 + ( 𝑚 + 𝑥 ) ) )
59 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑗 ∈ 𝑊 )
60 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝜑 )
61 11 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
62 ax-1cn ⊢ 1 ∈ ℂ
63 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
64 61 62 63 sylancl ⊢ ( 𝜑 → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
65 64 eqcomd ⊢ ( 𝜑 → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
66 60 65 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 = ( ( 𝑁 − 1 ) + 1 ) )
67 66 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
68 2 67 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑊 = ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
69 59 68 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( ( 𝑁 − 1 ) + 1 ) ) )
70 9 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → 𝑀 ∈ ℤ )
71 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
72 70 71 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
73 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
74 73 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
75 60 74 18 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
76 56 58 69 72 75 seqsplit ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ) )
77 60 24 4 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
78 60 24 5 syl2an ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
79 77 72 78 fsumser ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 = ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) )
80 66 seqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → seq 𝑁 ( + , 𝐹 ) = seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) )
81 80 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) = ( seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) )
82 79 81 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( seq ( ( 𝑁 − 1 ) + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ) )
83 76 82 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ) )
84 83 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ) ) )
85 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
86 7 85 syl ⊢ ( 𝜑 → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
88 54 84 87 mpjaod ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑊 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑗 ) ) )
89 2 11 21 26 6 29 88 climaddc2 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + Σ 𝑘 ∈ 𝑊 𝐴 ) )
90 1 9 4 5 89 isumclim ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + Σ 𝑘 ∈ 𝑊 𝐴 ) )