Metamath Proof Explorer

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 = M
serf.2 φ M
serfre.3 φ k Z F k
Assertion serfre φ seq M + F : Z


Step Hyp Ref Expression
1 serf.1 Z = M
2 serf.2 φ M
3 serfre.3 φ k Z F k
4 readdcl k x k + x
5 4 adantl φ k x k + x
6 1 2 3 5 seqf φ seq M + F : Z