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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	serf.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	serfre.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
Assertion	serfre	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		serf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		serf.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		serfre.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
4		readdcl	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 + 𝑥 ) ∈ ℝ )
5	4	adantl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) → ( 𝑘 + 𝑥 ) ∈ ℝ )
6	1 2 3 5	seqf	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )