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 = ( ZZ>= ` M )
	serf.2	|- ( ph -> M e. ZZ )
	serfre.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
Assertion	serfre	|- ( ph -> seq M ( + , F ) : Z --> RR )

Proof

Step	Hyp	Ref	Expression
1		serf.1	|- Z = ( ZZ>= ` M )
2		serf.2	|- ( ph -> M e. ZZ )
3		serfre.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
4		readdcl	|- ( ( k e. RR /\ x e. RR ) -> ( k + x ) e. RR )
5	4	adantl	|- ( ( ph /\ ( k e. RR /\ x e. RR ) ) -> ( k + x ) e. RR )
6	1 2 3 5	seqf	|- ( ph -> seq M ( + , F ) : Z --> RR )