Metamath Proof Explorer

Theorem logdivle

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

Ref Expression
Assertion logdivle ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→A≤B↔log⁡BB≤log⁡AA

Proof

Step Hyp Ref Expression
1 logdivlt ⊢B∈ℝ∧e≤B∧A∈ℝ∧e≤A→B<A↔log⁡AA<log⁡BB
2 1 ancoms ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→B<A↔log⁡AA<log⁡BB
3 2 notbid ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→¬B<A↔¬log⁡AA<log⁡BB
4 simpll ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→A∈ℝ
5 simprl ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→B∈ℝ
6 4 5 lenltd ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→A≤B↔¬B<A
7 0red ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→0∈ℝ
8 ere ⊢e∈ℝ
9 8 a1i ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→e∈ℝ
10 epos ⊢0<e
11 10 a1i ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→0<e
12 simprr ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→e≤B
13 7 9 5 11 12 ltletrd ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→0<B
14 5 13 elrpd ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→B∈ℝ+
15 relogcl ⊢B∈ℝ+→log⁡B∈ℝ
16 14 15 syl ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→log⁡B∈ℝ
17 16 14 rerpdivcld ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→log⁡BB∈ℝ
18 simplr ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→e≤A
19 7 9 4 11 18 ltletrd ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→0<A
20 4 19 elrpd ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→A∈ℝ+
21 relogcl ⊢A∈ℝ+→log⁡A∈ℝ
22 20 21 syl ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→log⁡A∈ℝ
23 22 20 rerpdivcld ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→log⁡AA∈ℝ
24 17 23 lenltd ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→log⁡BB≤log⁡AA↔¬log⁡AA<log⁡BB
25 3 6 24 3bitr4d ⊢A∈ℝ∧e≤A∧B∈ℝ∧e≤B→A≤B↔log⁡BB≤log⁡AA