Metamath Proof Explorer

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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ e ≤ A ∧ A < B → log ⁡ B B < log ⁡ A A

Proof

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