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 < e^{A}$

Proof

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

Metamath Proof Explorer

Theorem efgt0

Proof