This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ℤ_{\geq M}$
	serf.2	$⊢ φ \to M \in ℤ$
	serfre.3	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
Assertion	serfre	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$

Proof

Step	Hyp	Ref	Expression
1		serf.1	$⊢ Z = ℤ_{\geq M}$
2		serf.2	$⊢ φ \to M \in ℤ$
3		serfre.3	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
4		readdcl	$⊢ (k \in ℝ \land x \in ℝ) \to k + x \in ℝ$
5	4	adantl	$⊢ (φ \land (k \in ℝ \land x \in ℝ)) \to k + x \in ℝ$
6	1 2 3 5	seqf	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$