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

Proof

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