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

Metamath Proof Explorer

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 ⇝ )