Theorem eftlcvg

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

	Ref	Expression
Hypothesis	eftl.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	eftlcvg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )

Proof

Step	Hyp	Ref	Expression
1		eftl.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2	1	efcllem	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
3	2	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
4		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
6	1	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
7	6	adantl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
8		eftcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
9	8	adantlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
10	7 9	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
11	4 5 10	iserex	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( seq 0 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ) )
12	3 11	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )