efle

Description: The exponential function on the reals is nondecreasing. (Contributed by Mario Carneiro, 11-Mar-2014)

		Ref	Expression
	Assertion	efle	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \leftrightarrow e^{A} \leq e^{B})$

Step	Hyp	Ref	Expression
1		eflt	$⊢ (B \in ℝ \land A \in ℝ) \to (B < A \leftrightarrow e^{B} < e^{A})$
2	1	ancoms	$⊢ (A \in ℝ \land B \in ℝ) \to (B < A \leftrightarrow e^{B} < e^{A})$
3	2	notbid	$⊢ (A \in ℝ \land B \in ℝ) \to (\neg B < A \leftrightarrow \neg e^{B} < e^{A})$
4		lenlt	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \leftrightarrow \neg B < A)$
5		reefcl	$⊢ A \in ℝ \to e^{A} \in ℝ$
6		reefcl	$⊢ B \in ℝ \to e^{B} \in ℝ$
7		lenlt	$⊢ (e^{A} \in ℝ \land e^{B} \in ℝ) \to (e^{A} \leq e^{B} \leftrightarrow \neg e^{B} < e^{A})$
8	5 6 7	syl2an	$⊢ (A \in ℝ \land B \in ℝ) \to (e^{A} \leq e^{B} \leftrightarrow \neg e^{B} < e^{A})$
9	3 4 8	3bitr4d	$⊢ (A \in ℝ \land B \in ℝ) \to (A \leq B \leftrightarrow e^{A} \leq e^{B})$

Metamath Proof Explorer