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 ⊢ F = n ∈ ℕ 0 ⟼ A n n !
Assertion eftlcvg ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 → seq M + F ∈ dom ⁡ ⇝

Proof

Step Hyp Ref Expression
1 eftl.1 ⊢ F = n ∈ ℕ 0 ⟼ A n n !
2 1 efcllem ⊢ A ∈ ℂ → seq 0 + F ∈ dom ⁡ ⇝
3 2 adantr ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 → seq 0 + F ∈ dom ⁡ ⇝
4 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
5 simpr ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 → M ∈ ℕ 0
6 1 eftval ⊢ k ∈ ℕ 0 → F ⁡ k = A k k !
7 6 adantl ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 ∧ k ∈ ℕ 0 → F ⁡ k = A k k !
8 eftcl ⊢ A ∈ ℂ ∧ k ∈ ℕ 0 → A k k ! ∈ ℂ
9 8 adantlr ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 ∧ k ∈ ℕ 0 → A k k ! ∈ ℂ
10 7 9 eqeltrd ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 ∧ k ∈ ℕ 0 → F ⁡ k ∈ ℂ
11 4 5 10 iserex ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 → seq 0 + F ∈ dom ⁡ ⇝ ↔ seq M + F ∈ dom ⁡ ⇝
12 3 11 mpbid ⊢ A ∈ ℂ ∧ M ∈ ℕ 0 → seq M + F ∈ dom ⁡ ⇝