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	⊢ ( 𝐴 ∈ ℝ+ → 1 < ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		1red	⊢ ( 𝐴 ∈ ℝ+ → 1 ∈ ℝ )
2		1re	⊢ 1 ∈ ℝ
3		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
4		readdcl	⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 1 + 𝐴 ) ∈ ℝ )
5	2 3 4	sylancr	⊢ ( 𝐴 ∈ ℝ+ → ( 1 + 𝐴 ) ∈ ℝ )
6	3	reefcld	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ 𝐴 ) ∈ ℝ )
7		ltaddrp	⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → 1 < ( 1 + 𝐴 ) )
8	2 7	mpan	⊢ ( 𝐴 ∈ ℝ+ → 1 < ( 1 + 𝐴 ) )
9		efgt1p	⊢ ( 𝐴 ∈ ℝ+ → ( 1 + 𝐴 ) < ( exp ‘ 𝐴 ) )
10	1 5 6 8 9	lttrd	⊢ ( 𝐴 ∈ ℝ+ → 1 < ( exp ‘ 𝐴 ) )