eftlcvg

Description: The tail series of the exponential function are convergent. (Contributed by Mario Carneiro, 29-Apr-2014)

		Ref	Expression
	Hypothesis	eftl.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	Assertion	eftlcvg	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to seq M (+ F) \in dom ⇝$

Step	Hyp	Ref	Expression
1		eftl.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
2	1	efcllem	$⊢ A \in ℂ \to seq 0 (+ F) \in dom ⇝$
3	2	adantr	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to seq 0 (+ F) \in dom ⇝$
4		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
5		simpr	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to M \in ℕ_{0}$
6	1	eftval	$⊢ k \in ℕ_{0} \to F (k) = \frac{A^{k}}{k!}$
7	6	adantl	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) = \frac{A^{k}}{k!}$
8		eftcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to \frac{A^{k}}{k!} \in ℂ$
9	8	adantlr	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to \frac{A^{k}}{k!} \in ℂ$
10	7 9	eqeltrd	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to F (k) \in ℂ$
11	4 5 10	iserex	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to (seq 0 (+ F) \in dom ⇝ \leftrightarrow seq M (+ F) \in dom ⇝)$
12	3 11	mpbid	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to seq M (+ F) \in dom ⇝$

Metamath Proof Explorer