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\in ℝ\to {\mathrm{e}}^A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		efval	$$⊢A\in ℂ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
3	1 2	syl	$$⊢A\in ℝ\to {\mathrm{e}}^A=\sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)$$
4		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
5		0zd	$$⊢A\in ℝ\to 0\in \mathbb{Z}$$
6		eqid	$$⊢\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
7	6	eftval	$$⊢k\in {\mathbb{N}}_0\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(k\right)=\frac{A^k}{k!}$$
8	7	adantl	$$⊢\left(A\in ℝ\wedge k\in {\mathbb{N}}_0\right)\to \left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\left(k\right)=\frac{A^k}{k!}$$
9		reeftcl	$$⊢\left(A\in ℝ\wedge k\in {\mathbb{N}}_0\right)\to \frac{A^k}{k!}\in ℝ$$
10	6	efcllem	$$⊢A\in ℂ\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\in \mathrm{dom}⇝$$
11	1 10	syl	$$⊢A\in ℝ\to seq0\left(+,\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)\right)\in \mathrm{dom}⇝$$
12	4 5 8 9 11	isumrecl	$$⊢A\in ℝ\to \sum _{k\in {\mathbb{N}}_0}\left(\frac{A^k}{k!}\right)\in ℝ$$
13	3 12	eqeltrd	$$⊢A\in ℝ\to {\mathrm{e}}^A\in ℝ$$