Theorem serfre

Description: An infinite series of real numbers is a function from NN to RR . (Contributed by NM, 18-Apr-2005) (Revised by Mario Carneiro, 27-May-2014)

	Ref	Expression
Hypotheses	serf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	serf.2	$$⊢\phi \to M\in \mathbb{Z}$$
	serfre.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
Assertion	serfre	$$⊢\phi \to seqM\left(+,F\right):Z⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		serf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		serf.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		serfre.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
4		readdcl	$$⊢\left(k\in ℝ\wedge x\in ℝ\right)\to k+x\in ℝ$$
5	4	adantl	$$⊢\left(\phi \wedge \left(k\in ℝ\wedge x\in ℝ\right)\right)\to k+x\in ℝ$$
6	1 2 3 5	seqf	$$⊢\phi \to seqM\left(+,F\right):Z⟶ℝ$$