Theorem clim2ser2

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

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

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		clim2ser.2	⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
3		clim2ser.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
4		clim2ser2.5	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( + , 𝐹 ) ⇝ 𝐴 )
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	ffvelcdmd	⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
15		seqex	⊢ seq 𝑀 ( + , 𝐹 ) ∈ V
16	15	a1i	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ V )
17	8 1	eleqtrrdi	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ 𝑍 )
18	1	uztrn2	⊢ ( ( ( 𝑁 + 1 ) ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
19	17 18	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑘 ∈ 𝑍 )
20	19 3	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
21	5 10 20	serf	⊢ ( 𝜑 → seq ( 𝑁 + 1 ) ( + , 𝐹 ) : ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⟶ ℂ )
22	21	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℂ )
23	14	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℂ )
24		addcl	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
25	24	adantl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ) ) → ( 𝑘 + 𝑥 ) ∈ ℂ )
26		addass	⊢ ( ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑘 + 𝑥 ) + 𝑦 ) = ( 𝑘 + ( 𝑥 + 𝑦 ) ) )
27	26	adantl	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ ( 𝑘 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( ( 𝑘 + 𝑥 ) + 𝑦 ) = ( 𝑘 + ( 𝑥 + 𝑦 ) ) )
28		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
29	6	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
30		elfzuz	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
31	30 1	eleqtrrdi	⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑗 ) → 𝑘 ∈ 𝑍 )
32	31 3	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
33	32	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
34	25 27 28 29 33	seqsplit	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) + ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) ) )
35	23 22 34	comraddd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) = ( ( seq ( 𝑁 + 1 ) ( + , 𝐹 ) ‘ 𝑗 ) + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
36	5 10 4 14 16 22 35	climaddc1	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( 𝐴 + ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )