Theorem efgt1

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

	Ref	Expression
Assertion	efgt1	$$⊢A\in {ℝ}^{+}\to 1<{\mathrm{e}}^A$$

Proof

Step	Hyp	Ref	Expression
1		1red	$$⊢A\in {ℝ}^{+}\to 1\in ℝ$$
2		1re	$$⊢1\in ℝ$$
3		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
4		readdcl	$$⊢\left(1\in ℝ\wedge A\in ℝ\right)\to 1+A\in ℝ$$
5	2 3 4	sylancr	$$⊢A\in {ℝ}^{+}\to 1+A\in ℝ$$
6	3	reefcld	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^A\in ℝ$$
7		ltaddrp	$$⊢\left(1\in ℝ\wedge A\in {ℝ}^{+}\right)\to 1<1+A$$
8	2 7	mpan	$$⊢A\in {ℝ}^{+}\to 1<1+A$$
9		efgt1p	$$⊢A\in {ℝ}^{+}\to 1+A<{\mathrm{e}}^A$$
10	1 5 6 8 9	lttrd	$$⊢A\in {ℝ}^{+}\to 1<{\mathrm{e}}^A$$