logdivlt

Description: The log x / x function is strictly decreasing on the reals greater than _e . (Contributed by Mario Carneiro, 14-Mar-2014)

		Ref	Expression
	Assertion	logdivlt	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (A < B \leftrightarrow \frac{\log B}{B} < \frac{\log A}{A})$

Proof

Step	Hyp	Ref	Expression
1		logdivlti	$⊢ ((A \in ℝ \land B \in ℝ \land e \leq A) \land A < B) \to \frac{\log B}{B} < \frac{\log A}{A}$
2	1	ex	$⊢ (A \in ℝ \land B \in ℝ \land e \leq A) \to (A < B \to \frac{\log B}{B} < \frac{\log A}{A})$
3	2	3expa	$⊢ ((A \in ℝ \land B \in ℝ) \land e \leq A) \to (A < B \to \frac{\log B}{B} < \frac{\log A}{A})$
4	3	an32s	$⊢ ((A \in ℝ \land e \leq A) \land B \in ℝ) \to (A < B \to \frac{\log B}{B} < \frac{\log A}{A})$
5	4	adantrr	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (A < B \to \frac{\log B}{B} < \frac{\log A}{A})$
6		fveq2	$⊢ A = B \to \log A = \log B$
7		id	$⊢ A = B \to A = B$
8	6 7	oveq12d	$⊢ A = B \to \frac{\log A}{A} = \frac{\log B}{B}$
9	8	eqcomd	$⊢ A = B \to \frac{\log B}{B} = \frac{\log A}{A}$
10	9	a1i	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (A = B \to \frac{\log B}{B} = \frac{\log A}{A})$
11		logdivlti	$⊢ ((B \in ℝ \land A \in ℝ \land e \leq B) \land B < A) \to \frac{\log A}{A} < \frac{\log B}{B}$
12	11	ex	$⊢ (B \in ℝ \land A \in ℝ \land e \leq B) \to (B < A \to \frac{\log A}{A} < \frac{\log B}{B})$
13	12	3expa	$⊢ ((B \in ℝ \land A \in ℝ) \land e \leq B) \to (B < A \to \frac{\log A}{A} < \frac{\log B}{B})$
14	13	an32s	$⊢ ((B \in ℝ \land e \leq B) \land A \in ℝ) \to (B < A \to \frac{\log A}{A} < \frac{\log B}{B})$
15	14	adantrr	$⊢ ((B \in ℝ \land e \leq B) \land (A \in ℝ \land e \leq A)) \to (B < A \to \frac{\log A}{A} < \frac{\log B}{B})$
16	15	ancoms	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (B < A \to \frac{\log A}{A} < \frac{\log B}{B})$
17	10 16	orim12d	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to ((A = B \lor B < A) \to (\frac{\log B}{B} = \frac{\log A}{A} \lor \frac{\log A}{A} < \frac{\log B}{B}))$
18	17	con3d	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (\neg (\frac{\log B}{B} = \frac{\log A}{A} \lor \frac{\log A}{A} < \frac{\log B}{B}) \to \neg (A = B \lor B < A))$
19		simpl	$⊢ (B \in ℝ \land e \leq B) \to B \in ℝ$
20		epos	$⊢ 0 < e$
21		0re	$⊢ 0 \in ℝ$
22		ere	$⊢ e \in ℝ$
23		ltletr	$⊢ (0 \in ℝ \land e \in ℝ \land B \in ℝ) \to ((0 < e \land e \leq B) \to 0 < B)$
24	21 22 23	mp3an12	$⊢ B \in ℝ \to ((0 < e \land e \leq B) \to 0 < B)$
25	20 24	mpani	$⊢ B \in ℝ \to (e \leq B \to 0 < B)$
26	25	imp	$⊢ (B \in ℝ \land e \leq B) \to 0 < B$
27	19 26	elrpd	$⊢ (B \in ℝ \land e \leq B) \to B \in ℝ^{+}$
28		relogcl	$⊢ B \in ℝ^{+} \to \log B \in ℝ$
29		rerpdivcl	$⊢ (\log B \in ℝ \land B \in ℝ^{+}) \to \frac{\log B}{B} \in ℝ$
30	28 29	mpancom	$⊢ B \in ℝ^{+} \to \frac{\log B}{B} \in ℝ$
31	27 30	syl	$⊢ (B \in ℝ \land e \leq B) \to \frac{\log B}{B} \in ℝ$
32		simpl	$⊢ (A \in ℝ \land e \leq A) \to A \in ℝ$
33		ltletr	$⊢ (0 \in ℝ \land e \in ℝ \land A \in ℝ) \to ((0 < e \land e \leq A) \to 0 < A)$
34	21 22 33	mp3an12	$⊢ A \in ℝ \to ((0 < e \land e \leq A) \to 0 < A)$
35	20 34	mpani	$⊢ A \in ℝ \to (e \leq A \to 0 < A)$
36	35	imp	$⊢ (A \in ℝ \land e \leq A) \to 0 < A$
37	32 36	elrpd	$⊢ (A \in ℝ \land e \leq A) \to A \in ℝ^{+}$
38		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
39		rerpdivcl	$⊢ (\log A \in ℝ \land A \in ℝ^{+}) \to \frac{\log A}{A} \in ℝ$
40	38 39	mpancom	$⊢ A \in ℝ^{+} \to \frac{\log A}{A} \in ℝ$
41	37 40	syl	$⊢ (A \in ℝ \land e \leq A) \to \frac{\log A}{A} \in ℝ$
42		axlttri	$⊢ (\frac{\log B}{B} \in ℝ \land \frac{\log A}{A} \in ℝ) \to (\frac{\log B}{B} < \frac{\log A}{A} \leftrightarrow \neg (\frac{\log B}{B} = \frac{\log A}{A} \lor \frac{\log A}{A} < \frac{\log B}{B}))$
43	31 41 42	syl2anr	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (\frac{\log B}{B} < \frac{\log A}{A} \leftrightarrow \neg (\frac{\log B}{B} = \frac{\log A}{A} \lor \frac{\log A}{A} < \frac{\log B}{B}))$
44		axlttri	$⊢ (A \in ℝ \land B \in ℝ) \to (A < B \leftrightarrow \neg (A = B \lor B < A))$
45	44	ad2ant2r	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (A < B \leftrightarrow \neg (A = B \lor B < A))$
46	18 43 45	3imtr4d	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (\frac{\log B}{B} < \frac{\log A}{A} \to A < B)$
47	5 46	impbid	$⊢ ((A \in ℝ \land e \leq A) \land (B \in ℝ \land e \leq B)) \to (A < B \leftrightarrow \frac{\log B}{B} < \frac{\log A}{A})$

Metamath Proof Explorer

Theorem logdivlt

Proof