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

Metamath Proof Explorer

Theorem reefcl

Description: The exponential function is real if its argument is real. (Contributed by NM, 27-Apr-2005) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion reefcl ⊢ A ∈ ℝ → e A ∈ ℝ

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 efval ⊢ A ∈ ℂ → e A = ∑ k ∈ ℕ 0 A k k !
3 1 2 syl ⊢ A ∈ ℝ → e A = ∑ k ∈ ℕ 0 A k k !
4 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
5 0zd ⊢ A ∈ ℝ → 0 ∈ ℤ
6 eqid ⊢ n ∈ ℕ 0 ⟼ A n n ! = n ∈ ℕ 0 ⟼ A n n !
7 6 eftval ⊢ k ∈ ℕ 0 → n ∈ ℕ 0 ⟼ A n n ! ⁡ k = A k k !
8 7 adantl ⊢ A ∈ ℝ ∧ k ∈ ℕ 0 → n ∈ ℕ 0 ⟼ A n n ! ⁡ k = A k k !
9 reeftcl ⊢ A ∈ ℝ ∧ k ∈ ℕ 0 → A k k ! ∈ ℝ
10 6 efcllem ⊢ A ∈ ℂ → seq 0 + n ∈ ℕ 0 ⟼ A n n ! ∈ dom ⁡ ⇝
11 1 10 syl ⊢ A ∈ ℝ → seq 0 + n ∈ ℕ 0 ⟼ A n n ! ∈ dom ⁡ ⇝
12 4 5 8 9 11 isumrecl ⊢ A ∈ ℝ → ∑ k ∈ ℕ 0 A k k ! ∈ ℝ
13 3 12 eqeltrd ⊢ A ∈ ℝ → e A ∈ ℝ