This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ∈ ℝ )