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={\mathbb{Z}}_{\ge M}$$
	isumrecl.2	$$⊢\phi \to M\in \mathbb{Z}$$
	isumrecl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	isumrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
	isumrecl.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	isumrecl	$$⊢\phi \to \sum _{k\in Z}A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		isumrecl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumrecl.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isumrecl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
4		isumrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
5		isumrecl.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6	4	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
7	1 2 3 6 5	isumclim2	$$⊢\phi \to seqM\left(+,F\right)⇝\sum _{k\in Z}A$$
8	3 4	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
9	1 2 8	serfre	$$⊢\phi \to seqM\left(+,F\right):Z⟶ℝ$$
10	9	ffvelcdmda	$$⊢\left(\phi \wedge j\in Z\right)\to seqM\left(+,F\right)\left(j\right)\in ℝ$$
11	1 2 7 10	climrecl	$$⊢\phi \to \sum _{k\in Z}A\in ℝ$$