Theorem 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	$$⊢\left(\left(A\in ℝ\wedge \mathrm{e}\le A\right)\wedge \left(B\in ℝ\wedge \mathrm{e}\le B\right)\right)\to \left(A<B\leftrightarrow \frac{\log B}{B}<\frac{\log A}{A}\right)$$

Proof

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