Theorem logdivlti

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	logdivlti	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ )
2		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → e ≤ 𝐴 )
3		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐴 < 𝐵 )
4		ere	⊢ e ∈ ℝ
5		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ )
6		lelttr	⊢ ( ( e ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( e ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → e < 𝐵 ) )
7	4 5 1 6	mp3an2i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( e ≤ 𝐴 ∧ 𝐴 < 𝐵 ) → e < 𝐵 ) )
8	2 3 7	mp2and	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → e < 𝐵 )
9		epos	⊢ 0 < e
10		0re	⊢ 0 ∈ ℝ
11		lttr	⊢ ( ( 0 ∈ ℝ ∧ e ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < e ∧ e < 𝐵 ) → 0 < 𝐵 ) )
12	10 4 1 11	mp3an12i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 0 < e ∧ e < 𝐵 ) → 0 < 𝐵 ) )
13	9 12	mpani	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( e < 𝐵 → 0 < 𝐵 ) )
14	8 13	mpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 0 < 𝐵 )
15	1 14	elrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℝ+ )
16		ltletr	⊢ ( ( 0 ∈ ℝ ∧ e ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 < e ∧ e ≤ 𝐴 ) → 0 < 𝐴 ) )
17	10 4 5 16	mp3an12i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 0 < e ∧ e ≤ 𝐴 ) → 0 < 𝐴 ) )
18	9 17	mpani	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( e ≤ 𝐴 → 0 < 𝐴 ) )
19	2 18	mpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 0 < 𝐴 )
20	5 19	elrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℝ+ )
21	15 20	rpdivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 / 𝐴 ) ∈ ℝ+ )
22		relogcl	⊢ ( ( 𝐵 / 𝐴 ) ∈ ℝ+ → ( log ‘ ( 𝐵 / 𝐴 ) ) ∈ ℝ )
23	21 22	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ ( 𝐵 / 𝐴 ) ) ∈ ℝ )
24	1 20	rerpdivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 / 𝐴 ) ∈ ℝ )
25		1re	⊢ 1 ∈ ℝ
26		resubcl	⊢ ( ( ( 𝐵 / 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ )
27	24 25 26	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ )
28		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
29	20 28	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ 𝐴 ) ∈ ℝ )
30	27 29	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) ∈ ℝ )
31		reeflog	⊢ ( ( 𝐵 / 𝐴 ) ∈ ℝ+ → ( exp ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) = ( 𝐵 / 𝐴 ) )
32	21 31	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( exp ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) = ( 𝐵 / 𝐴 ) )
33		ax-1cn	⊢ 1 ∈ ℂ
34	24	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 / 𝐴 ) ∈ ℂ )
35		pncan3	⊢ ( ( 1 ∈ ℂ ∧ ( 𝐵 / 𝐴 ) ∈ ℂ ) → ( 1 + ( ( 𝐵 / 𝐴 ) − 1 ) ) = ( 𝐵 / 𝐴 ) )
36	33 34 35	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 + ( ( 𝐵 / 𝐴 ) − 1 ) ) = ( 𝐵 / 𝐴 ) )
37	32 36	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( exp ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) = ( 1 + ( ( 𝐵 / 𝐴 ) − 1 ) ) )
38	5	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐴 ∈ ℂ )
39	38	mullidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 · 𝐴 ) = 𝐴 )
40	39 3	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 · 𝐴 ) < 𝐵 )
41		1red	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 1 ∈ ℝ )
42		ltmuldiv	⊢ ( ( 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( ( 1 · 𝐴 ) < 𝐵 ↔ 1 < ( 𝐵 / 𝐴 ) ) )
43	41 1 5 19 42	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 1 · 𝐴 ) < 𝐵 ↔ 1 < ( 𝐵 / 𝐴 ) ) )
44	40 43	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 1 < ( 𝐵 / 𝐴 ) )
45		difrp	⊢ ( ( 1 ∈ ℝ ∧ ( 𝐵 / 𝐴 ) ∈ ℝ ) → ( 1 < ( 𝐵 / 𝐴 ) ↔ ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ+ ) )
46	25 24 45	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 < ( 𝐵 / 𝐴 ) ↔ ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ+ ) )
47	44 46	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ+ )
48		efgt1p	⊢ ( ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ+ → ( 1 + ( ( 𝐵 / 𝐴 ) − 1 ) ) < ( exp ‘ ( ( 𝐵 / 𝐴 ) − 1 ) ) )
49	47 48	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 + ( ( 𝐵 / 𝐴 ) − 1 ) ) < ( exp ‘ ( ( 𝐵 / 𝐴 ) − 1 ) ) )
50	37 49	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( exp ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) < ( exp ‘ ( ( 𝐵 / 𝐴 ) − 1 ) ) )
51		eflt	⊢ ( ( ( log ‘ ( 𝐵 / 𝐴 ) ) ∈ ℝ ∧ ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ ) → ( ( log ‘ ( 𝐵 / 𝐴 ) ) < ( ( 𝐵 / 𝐴 ) − 1 ) ↔ ( exp ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) < ( exp ‘ ( ( 𝐵 / 𝐴 ) − 1 ) ) ) )
52	23 27 51	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ ( 𝐵 / 𝐴 ) ) < ( ( 𝐵 / 𝐴 ) − 1 ) ↔ ( exp ‘ ( log ‘ ( 𝐵 / 𝐴 ) ) ) < ( exp ‘ ( ( 𝐵 / 𝐴 ) − 1 ) ) ) )
53	50 52	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ ( 𝐵 / 𝐴 ) ) < ( ( 𝐵 / 𝐴 ) − 1 ) )
54	27	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℂ )
55	54	mulridd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 / 𝐴 ) − 1 ) · 1 ) = ( ( 𝐵 / 𝐴 ) − 1 ) )
56		df-e	⊢ e = ( exp ‘ 1 )
57		reeflog	⊢ ( 𝐴 ∈ ℝ+ → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
58	20 57	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
59	2 58	breqtrrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → e ≤ ( exp ‘ ( log ‘ 𝐴 ) ) )
60	56 59	eqbrtrrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( exp ‘ 1 ) ≤ ( exp ‘ ( log ‘ 𝐴 ) ) )
61		efle	⊢ ( ( 1 ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( 1 ≤ ( log ‘ 𝐴 ) ↔ ( exp ‘ 1 ) ≤ ( exp ‘ ( log ‘ 𝐴 ) ) ) )
62	25 29 61	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 ≤ ( log ‘ 𝐴 ) ↔ ( exp ‘ 1 ) ≤ ( exp ‘ ( log ‘ 𝐴 ) ) ) )
63	60 62	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 1 ≤ ( log ‘ 𝐴 ) )
64		posdif	⊢ ( ( 1 ∈ ℝ ∧ ( 𝐵 / 𝐴 ) ∈ ℝ ) → ( 1 < ( 𝐵 / 𝐴 ) ↔ 0 < ( ( 𝐵 / 𝐴 ) − 1 ) ) )
65	25 24 64	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 < ( 𝐵 / 𝐴 ) ↔ 0 < ( ( 𝐵 / 𝐴 ) − 1 ) ) )
66	44 65	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 0 < ( ( 𝐵 / 𝐴 ) − 1 ) )
67		lemul2	⊢ ( ( 1 ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ∧ ( ( ( 𝐵 / 𝐴 ) − 1 ) ∈ ℝ ∧ 0 < ( ( 𝐵 / 𝐴 ) − 1 ) ) ) → ( 1 ≤ ( log ‘ 𝐴 ) ↔ ( ( ( 𝐵 / 𝐴 ) − 1 ) · 1 ) ≤ ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) ) )
68	41 29 27 66 67	syl112anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 ≤ ( log ‘ 𝐴 ) ↔ ( ( ( 𝐵 / 𝐴 ) − 1 ) · 1 ) ≤ ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) ) )
69	63 68	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 / 𝐴 ) − 1 ) · 1 ) ≤ ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) )
70	55 69	eqbrtrrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 / 𝐴 ) − 1 ) ≤ ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) )
71	23 27 30 53 70	ltletrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ ( 𝐵 / 𝐴 ) ) < ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) )
72		relogdiv	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( log ‘ ( 𝐵 / 𝐴 ) ) = ( ( log ‘ 𝐵 ) − ( log ‘ 𝐴 ) ) )
73	15 20 72	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ ( 𝐵 / 𝐴 ) ) = ( ( log ‘ 𝐵 ) − ( log ‘ 𝐴 ) ) )
74		1cnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 1 ∈ ℂ )
75	29	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ 𝐴 ) ∈ ℂ )
76	34 74 75	subdird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) = ( ( ( 𝐵 / 𝐴 ) · ( log ‘ 𝐴 ) ) − ( 1 · ( log ‘ 𝐴 ) ) ) )
77	1	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐵 ∈ ℂ )
78	20	rpne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → 𝐴 ≠ 0 )
79	77 38 75 78	div32d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( 𝐵 / 𝐴 ) · ( log ‘ 𝐴 ) ) = ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
80	75	mullidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 1 · ( log ‘ 𝐴 ) ) = ( log ‘ 𝐴 ) )
81	79 80	oveq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 / 𝐴 ) · ( log ‘ 𝐴 ) ) − ( 1 · ( log ‘ 𝐴 ) ) ) = ( ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) − ( log ‘ 𝐴 ) ) )
82	76 81	eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( ( 𝐵 / 𝐴 ) − 1 ) · ( log ‘ 𝐴 ) ) = ( ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) − ( log ‘ 𝐴 ) ) )
83	71 73 82	3brtr3d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ 𝐵 ) − ( log ‘ 𝐴 ) ) < ( ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) − ( log ‘ 𝐴 ) ) )
84		relogcl	⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
85	15 84	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ 𝐵 ) ∈ ℝ )
86	29 20	rerpdivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℝ )
87	1 86	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) ∈ ℝ )
88	85 87 29	ltsub1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ 𝐵 ) < ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) ↔ ( ( log ‘ 𝐵 ) − ( log ‘ 𝐴 ) ) < ( ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) − ( log ‘ 𝐴 ) ) ) )
89	83 88	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( log ‘ 𝐵 ) < ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
90	85 86 15	ltdivmuld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ↔ ( log ‘ 𝐵 ) < ( 𝐵 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) ) )
91	89 90	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) )