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 < 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	$⊢ (1 \in ℝ \land A \in ℝ) \to 1 + A \in ℝ$
5	2 3 4	sylancr	$⊢ A \in ℝ^{+} \to 1 + A \in ℝ$
6	3	reefcld	$⊢ A \in ℝ^{+} \to e^{A} \in ℝ$
7		ltaddrp	$⊢ (1 \in ℝ \land A \in ℝ^{+}) \to 1 < 1 + A$
8	2 7	mpan	$⊢ A \in ℝ^{+} \to 1 < 1 + A$
9		efgt1p	$⊢ A \in ℝ^{+} \to 1 + A < e^{A}$
10	1 5 6 8 9	lttrd	$⊢ A \in ℝ^{+} \to 1 < e^{A}$

Metamath Proof Explorer

Theorem efgt1

Proof