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

Metamath Proof Explorer

Theorem eftlcl

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	eftlcl	$⊢ (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		eftcl	$⊢ (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	1	eftlcvg	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to seq M (+ F) \in dom ⇝$
15	2 4 5 13 14	isumcl	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to \sum_{k \in ℤ_{\geq M}} F (k) \in ℂ$