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