Metamath Proof Explorer

Theorem reeftlcl

Description: Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

		Ref	Expression
	Hypothesis	eftl.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	Assertion	reeftlcl	$⊢ (A \in ℝ \land M \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq M}} F (k) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		eftl.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
2		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
3		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
4	3	adantl	$⊢ (A \in ℝ \land M \in ℕ_{0}) \to M \in ℤ$
5		eqidd	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land k \in ℤ_{\geq M}) \to F (k) = F (k)$
6		eluznn0	$⊢ (M \in ℕ_{0} \land k \in ℤ_{\geq M}) \to k \in ℕ_{0}$
7	6	adantll	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land k \in ℤ_{\geq M}) \to k \in ℕ_{0}$
8	1	eftval	$⊢ k \in ℕ_{0} \to F (k) = \frac{A^{k}}{k!}$
9	7 8	syl	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land k \in ℤ_{\geq M}) \to F (k) = \frac{A^{k}}{k!}$
10		simpll	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land k \in ℤ_{\geq M}) \to A \in ℝ$
11		reeftcl	$⊢ (A \in ℝ \land k \in ℕ_{0}) \to \frac{A^{k}}{k!} \in ℝ$
12	10 7 11	syl2anc	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land k \in ℤ_{\geq M}) \to \frac{A^{k}}{k!} \in ℝ$
13	9 12	eqeltrd	$⊢ ((A \in ℝ \land M \in ℕ_{0}) \land k \in ℤ_{\geq M}) \to F (k) \in ℝ$
14		recn	$⊢ A \in ℝ \to A \in ℂ$
15	1	eftlcvg	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to seq M (+ F) \in dom ⇝$
16	14 15	sylan	$⊢ (A \in ℝ \land M \in ℕ_{0}) \to seq M (+ F) \in dom ⇝$
17	2 4 5 13 16	isumrecl	$⊢ (A \in ℝ \land M \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq M}} F (k) \in ℝ$