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⁡BB<log⁡AA

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→BA∈ℝ+
22 relogcl ⊢BA∈ℝ+→log⁡BA∈ℝ
23 21 22 syl ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡BA∈ℝ
24 1 20 rerpdivcld ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA∈ℝ
25 1re ⊢1∈ℝ
26 resubcl ⊢BA∈ℝ∧1∈ℝ→BA−1∈ℝ
27 24 25 26 sylancl ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA−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→BA−1⁢log⁡A∈ℝ
31 reeflog ⊢BA∈ℝ+→elog⁡BA=BA
32 21 31 syl ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→elog⁡BA=BA
33 ax-1cn ⊢1∈ℂ
34 24 recnd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA∈ℂ
35 pncan3 ⊢1∈ℂ∧BA∈ℂ→1+BA-1=BA
36 33 34 35 sylancr ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1+BA-1=BA
37 32 36 eqtr4d ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→elog⁡BA=1+BA-1
38 5 recnd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→A∈ℂ
39 38 mullidd ⊢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<BA
43 41 1 5 19 42 syl112anc ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1⁢A<B↔1<BA
44 40 43 mpbid ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1<BA
45 difrp ⊢1∈ℝ∧BA∈ℝ→1<BA↔BA−1∈ℝ+
46 25 24 45 sylancr ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1<BA↔BA−1∈ℝ+
47 44 46 mpbid ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA−1∈ℝ+
48 efgt1p ⊢BA−1∈ℝ+→1+BA-1<eBA−1
49 47 48 syl ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1+BA-1<eBA−1
50 37 49 eqbrtrd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→elog⁡BA<eBA−1
51 eflt ⊢log⁡BA∈ℝ∧BA−1∈ℝ→log⁡BA<BA−1↔elog⁡BA<eBA−1
52 23 27 51 syl2anc ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡BA<BA−1↔elog⁡BA<eBA−1
53 50 52 mpbird ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡BA<BA−1
54 27 recnd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA−1∈ℂ
55 54 mulridd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA−1⋅1=BA−1
56 df-e ⊢e=e1
57 reeflog ⊢A∈ℝ+→elog⁡A=A
58 20 57 syl ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→elog⁡A=A
59 2 58 breqtrrd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→e≤elog⁡A
60 56 59 eqbrtrrid ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→e1≤elog⁡A
61 efle ⊢1∈ℝ∧log⁡A∈ℝ→1≤log⁡A↔e1≤elog⁡A
62 25 29 61 sylancr ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1≤log⁡A↔e1≤elog⁡A
63 60 62 mpbird ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1≤log⁡A
64 posdif ⊢1∈ℝ∧BA∈ℝ→1<BA↔0<BA−1
65 25 24 64 sylancr ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1<BA↔0<BA−1
66 44 65 mpbid ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→0<BA−1
67 lemul2 ⊢1∈ℝ∧log⁡A∈ℝ∧BA−1∈ℝ∧0<BA−1→1≤log⁡A↔BA−1⋅1≤BA−1⁢log⁡A
68 41 29 27 66 67 syl112anc ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1≤log⁡A↔BA−1⋅1≤BA−1⁢log⁡A
69 63 68 mpbid ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA−1⋅1≤BA−1⁢log⁡A
70 55 69 eqbrtrrd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA−1≤BA−1⁢log⁡A
71 23 27 30 53 70 ltletrd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡BA<BA−1⁢log⁡A
72 relogdiv ⊢B∈ℝ+∧A∈ℝ+→log⁡BA=log⁡B−log⁡A
73 15 20 72 syl2anc ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡BA=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→BA−1⁢log⁡A=BA⁢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→BA⁢log⁡A=B⁢log⁡AA
80 75 mullidd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→1⁢log⁡A=log⁡A
81 79 80 oveq12d ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA⁢log⁡A−1⁢log⁡A=B⁢log⁡AA−log⁡A
82 76 81 eqtrd ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→BA−1⁢log⁡A=B⁢log⁡AA−log⁡A
83 71 73 82 3brtr3d ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡B−log⁡A<B⁢log⁡AA−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⁡AA∈ℝ
87 1 86 remulcld ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→B⁢log⁡AA∈ℝ
88 85 87 29 ltsub1d ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡B<B⁢log⁡AA↔log⁡B−log⁡A<B⁢log⁡AA−log⁡A
89 83 88 mpbird ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡B<B⁢log⁡AA
90 85 86 15 ltdivmuld ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡BB<log⁡AA↔log⁡B<B⁢log⁡AA
91 89 90 mpbird ⊢A∈ℝ∧B∈ℝ∧e≤A∧A<B→log⁡BB<log⁡AA