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 ‘ 𝐴 ) / 𝐴 ) ) )