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 ⁡ B B ≤ log ⁡ A A

Proof

Step Hyp Ref Expression
1 logdivlt ⊢ B ∈ ℝ ∧ e ≤ B ∧ A ∈ ℝ ∧ e ≤ A → B < A ↔ log ⁡ A A < log ⁡ B B
2 1 ancoms ⊢ A ∈ ℝ ∧ e ≤ A ∧ B ∈ ℝ ∧ e ≤ B → B < A ↔ log ⁡ A A < log ⁡ B B
3 2 notbid ⊢ A ∈ ℝ ∧ e ≤ A ∧ B ∈ ℝ ∧ e ≤ B → ¬ B < A ↔ ¬ log ⁡ A A < log ⁡ B B
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 ⁡ B B ∈ ℝ
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 ⁡ A A ∈ ℝ
24 17 23 lenltd ⊢ A ∈ ℝ ∧ e ≤ A ∧ B ∈ ℝ ∧ e ≤ B → log ⁡ B B ≤ log ⁡ A A ↔ ¬ log ⁡ A A < log ⁡ B B
25 3 6 24 3bitr4d ⊢ A ∈ ℝ ∧ e ≤ A ∧ B ∈ ℝ ∧ e ≤ B → A ≤ B ↔ log ⁡ B B ≤ log ⁡ A A