Theorem isumrecl

Description: The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		isumrecl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumrecl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumrecl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumrecl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
5		isumrecl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6	4	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
7	1 2 3 6 5	isumclim2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )
8	3 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
9	1 2 8	serfre	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
10	9	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
11	1 2 7 10	climrecl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ∈ ℝ )