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 ⊢ Z = ℤ ≥ M
isumrecl.2 ⊢ φ → M ∈ ℤ
isumrecl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
isumrecl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
isumrecl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
Assertion isumrecl ⊢ φ → ∑ k ∈ Z A ∈ ℝ

Proof

Step Hyp Ref Expression
1 isumrecl.1 ⊢ Z = ℤ ≥ M
2 isumrecl.2 ⊢ φ → M ∈ ℤ
3 isumrecl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
4 isumrecl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
5 isumrecl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
6 4 recnd ⊢ φ ∧ k ∈ Z → A ∈ ℂ
7 1 2 3 6 5 isumclim2 ⊢ φ → seq M + F ⇝ ∑ k ∈ Z A
8 3 4 eqeltrd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
9 1 2 8 serfre ⊢ φ → seq M + F : Z ⟶ ℝ
10 9 ffvelcdmda ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ∈ ℝ
11 1 2 7 10 climrecl ⊢ φ → ∑ k ∈ Z A ∈ ℝ