eflt

Description: The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 17-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		tru	$⊢ ⊤$
2		fveq2	$⊢ x = y \to e^{x} = e^{y}$
3		fveq2	$⊢ x = A \to e^{x} = e^{A}$
4		fveq2	$⊢ x = B \to e^{x} = e^{B}$
5		ssid	$⊢ ℝ \subseteq ℝ$
6		reefcl	$⊢ x \in ℝ \to e^{x} \in ℝ$
7	6	adantl	$⊢ (⊤ \land x \in ℝ) \to e^{x} \in ℝ$
8		simp2	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to y \in ℝ$
9		simp1	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to x \in ℝ$
10	8 9	resubcld	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to y - x \in ℝ$
11		posdif	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \leftrightarrow 0 < y - x)$
12	11	biimp3a	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to 0 < y - x$
13	10 12	elrpd	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to y - x \in ℝ^{+}$
14		efgt1	$⊢ y - x \in ℝ^{+} \to 1 < e^{y - x}$
15	13 14	syl	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to 1 < e^{y - x}$
16	9	reefcld	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to e^{x} \in ℝ$
17	10	reefcld	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to e^{y - x} \in ℝ$
18		efgt0	$⊢ x \in ℝ \to 0 < e^{x}$
19	9 18	syl	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to 0 < e^{x}$
20		ltmulgt11	$⊢ (e^{x} \in ℝ \land e^{y - x} \in ℝ \land 0 < e^{x}) \to (1 < e^{y - x} \leftrightarrow e^{x} < e^{x} e^{y - x})$
21	16 17 19 20	syl3anc	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to (1 < e^{y - x} \leftrightarrow e^{x} < e^{x} e^{y - x})$
22	15 21	mpbid	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to e^{x} < e^{x} e^{y - x}$
23	9	recnd	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to x \in ℂ$
24	10	recnd	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to y - x \in ℂ$
25		efadd	$⊢ (x \in ℂ \land y - x \in ℂ) \to e^{x + y - x} = e^{x} e^{y - x}$
26	23 24 25	syl2anc	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to e^{x + y - x} = e^{x} e^{y - x}$
27	8	recnd	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to y \in ℂ$
28	23 27	pncan3d	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to x + y - x = y$
29	28	fveq2d	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to e^{x + y - x} = e^{y}$
30	26 29	eqtr3d	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to e^{x} e^{y - x} = e^{y}$
31	22 30	breqtrd	$⊢ (x \in ℝ \land y \in ℝ \land x < y) \to e^{x} < e^{y}$
32	31	3expia	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \to e^{x} < e^{y})$
33	32	adantl	$⊢ (⊤ \land (x \in ℝ \land y \in ℝ)) \to (x < y \to e^{x} < e^{y})$
34	2 3 4 5 7 33	ltord1	$⊢ (⊤ \land (A \in ℝ \land B \in ℝ)) \to (A < B \leftrightarrow e^{A} < e^{B})$
35	1 34	mpan	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow e^{A} < e^{B})$

Metamath Proof Explorer

Theorem eflt

Proof