Theorem efgt0

Description: The exponential of a real number is greater than 0. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Assertion	efgt0	$$⊢A\in ℝ\to 0<{\mathrm{e}}^A$$

Proof

Step	Hyp	Ref	Expression
1		reefcl	$$⊢A\in ℝ\to {\mathrm{e}}^A\in ℝ$$
2		rehalfcl	$$⊢A\in ℝ\to \frac{A}{2}\in ℝ$$
3	2	reefcld	$$⊢A\in ℝ\to {\mathrm{e}}^{\frac{A}{2}}\in ℝ$$
4	3	sqge0d	$$⊢A\in ℝ\to 0\le {{\mathrm{e}}^{\frac{A}{2}}}^2$$
5	2	recnd	$$⊢A\in ℝ\to \frac{A}{2}\in ℂ$$
6		2z	$$⊢2\in \mathbb{Z}$$
7		efexp	$$⊢\left(\frac{A}{2}\in ℂ\wedge 2\in \mathbb{Z}\right)\to {\mathrm{e}}^{2\left(\frac{A}{2}\right)}={{\mathrm{e}}^{\frac{A}{2}}}^2$$
8	5 6 7	sylancl	$$⊢A\in ℝ\to {\mathrm{e}}^{2\left(\frac{A}{2}\right)}={{\mathrm{e}}^{\frac{A}{2}}}^2$$
9		recn	$$⊢A\in ℝ\to A\in ℂ$$
10		2cn	$$⊢2\in ℂ$$
11		2ne0	$$⊢2\ne 0$$
12		divcan2	$$⊢\left(A\in ℂ\wedge 2\in ℂ\wedge 2\ne 0\right)\to 2\left(\frac{A}{2}\right)=A$$
13	10 11 12	mp3an23	$$⊢A\in ℂ\to 2\left(\frac{A}{2}\right)=A$$
14	9 13	syl	$$⊢A\in ℝ\to 2\left(\frac{A}{2}\right)=A$$
15	14	fveq2d	$$⊢A\in ℝ\to {\mathrm{e}}^{2\left(\frac{A}{2}\right)}={\mathrm{e}}^A$$
16	8 15	eqtr3d	$$⊢A\in ℝ\to {{\mathrm{e}}^{\frac{A}{2}}}^2={\mathrm{e}}^A$$
17	4 16	breqtrd	$$⊢A\in ℝ\to 0\le {\mathrm{e}}^A$$
18		efne0	$$⊢A\in ℂ\to {\mathrm{e}}^A\ne 0$$
19	9 18	syl	$$⊢A\in ℝ\to {\mathrm{e}}^A\ne 0$$
20	1 17 19	ne0gt0d	$$⊢A\in ℝ\to 0<{\mathrm{e}}^A$$