Metamath Proof Explorer

Theorem clim2ser

Description: The limit of an infinite series with an initial segment removed. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 clim2ser.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3 clim2ser.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4 clim2ser.5 ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
5 eqid ⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) )
6 2 1 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
7 peano2uz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
8 6 7 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
9 eluzelz ⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 + 1 ) ∈ ℤ )
10 8 9 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
11 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
12 6 11 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
13 1 12 3 serf ⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
14 13 2 ffvelrnd ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
15 seqex ⊢ seq ( 𝑁 + 1 ) ( + , 𝐹 ) ∈ V
16 15 a1i ⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( + , 𝐹 ) ∈ V )
17 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℂ )
18 8 1 eleqtrrdi ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ 𝑍 )
19 1 uztrn2 ⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
20 18 19 sylan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ 𝑍 )
21 17 20 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
22 addcl ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
24 addass ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑘 + 𝑥 ) + 𝑦 ) = ( 𝑘 + ( 𝑥 + 𝑦 ) ) )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑘 + 𝑥 ) + 𝑦 ) = ( 𝑘 + ( 𝑥 + 𝑦 ) ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
27 6 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
28 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
29 28 1 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
30 29 3 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
31 30 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
32 23 25 26 27 31 seqsplit ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ) )
33 32 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
34 14 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
35 1 uztrn2 ⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
36 18 35 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
37 36 3 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
38 5 10 37 serf ⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( + , 𝐹 ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ )
39 38 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
40 34 39 pncan2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) = ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) )
41 33 40 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
42 5 10 4 14 16 21 41 climsubc1 ⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( + , 𝐹 ) ⇝ ( 𝐴 − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )