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 ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2 efval ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
3 1 2 syl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
4 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5 0zd ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℤ )
6 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
7 6 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
8 7 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
9 reeftcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
10 6 efcllem ⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ dom ⇝ )
11 1 10 syl ⊢ ( 𝐴 ∈ ℝ → seq 0 ( + , ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) ) ∈ dom ⇝ )
12 4 5 8 9 11 isumrecl ⊢ ( 𝐴 ∈ ℝ → Σ 𝑘 ∈ ℕ0 ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
13 3 12 eqeltrd ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ 𝐴 ) ∈ ℝ )