Metamath Proof Explorer

Theorem logdivlt

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

Proof

Step Hyp Ref Expression
1 logdivlti ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐴 < 𝐵 ) → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) )
2 1 ex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ e ≤ 𝐴 ) → ( 𝐴 < 𝐵 → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
3 2 3expa ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ e ≤ 𝐴 ) → ( 𝐴 < 𝐵 → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
4 3 an32s ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
5 4 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( 𝐴 < 𝐵 → ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
6 fveq2 ⊢ ( 𝐴 = 𝐵 → ( log ‘ 𝐴 ) = ( log ‘ 𝐵 ) )
7 id ⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
8 6 7 oveq12d ⊢ ( 𝐴 = 𝐵 → ( ( log ‘ 𝐴 ) / 𝐴 ) = ( ( log ‘ 𝐵 ) / 𝐵 ) )
9 8 eqcomd ⊢ ( 𝐴 = 𝐵 → ( ( log ‘ 𝐵 ) / 𝐵 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) )
10 9 a1i ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( 𝐴 = 𝐵 → ( ( log ‘ 𝐵 ) / 𝐵 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
11 logdivlti ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ e ≤ 𝐵 ) ∧ 𝐵 < 𝐴 ) → ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) )
12 11 ex ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ e ≤ 𝐵 ) → ( 𝐵 < 𝐴 → ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) )
13 12 3expa ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ e ≤ 𝐵 ) → ( 𝐵 < 𝐴 → ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) )
14 13 an32s ⊢ ( ( ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐵 < 𝐴 → ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) )
15 14 adantrr ⊢ ( ( ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ) → ( 𝐵 < 𝐴 → ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) )
16 15 ancoms ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( 𝐵 < 𝐴 → ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) )
17 10 16 orim12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) → ( ( ( log ‘ 𝐵 ) / 𝐵 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) ∨ ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) ) )
18 17 con3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( ¬ ( ( ( log ‘ 𝐵 ) / 𝐵 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) ∨ ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) → ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) )
19 simpl ⊢ ( ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) → 𝐵 ∈ ℝ )
20 epos ⊢ 0 < e
21 0re ⊢ 0 ∈ ℝ
22 ere ⊢ e ∈ ℝ
23 ltletr ⊢ ( ( 0 ∈ ℝ ∧ e ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < e ∧ e ≤ 𝐵 ) → 0 < 𝐵 ) )
24 21 22 23 mp3an12 ⊢ ( 𝐵 ∈ ℝ → ( ( 0 < e ∧ e ≤ 𝐵 ) → 0 < 𝐵 ) )
25 20 24 mpani ⊢ ( 𝐵 ∈ ℝ → ( e ≤ 𝐵 → 0 < 𝐵 ) )
26 25 imp ⊢ ( ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) → 0 < 𝐵 )
27 19 26 elrpd ⊢ ( ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) → 𝐵 ∈ ℝ+ )
28 relogcl ⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
29 rerpdivcl ⊢ ( ( ( log ‘ 𝐵 ) ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝐵 ) / 𝐵 ) ∈ ℝ )
30 28 29 mpancom ⊢ ( 𝐵 ∈ ℝ+ → ( ( log ‘ 𝐵 ) / 𝐵 ) ∈ ℝ )
31 27 30 syl ⊢ ( ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) → ( ( log ‘ 𝐵 ) / 𝐵 ) ∈ ℝ )
32 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) → 𝐴 ∈ ℝ )
33 ltletr ⊢ ( ( 0 ∈ ℝ ∧ e ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 0 < e ∧ e ≤ 𝐴 ) → 0 < 𝐴 ) )
34 21 22 33 mp3an12 ⊢ ( 𝐴 ∈ ℝ → ( ( 0 < e ∧ e ≤ 𝐴 ) → 0 < 𝐴 ) )
35 20 34 mpani ⊢ ( 𝐴 ∈ ℝ → ( e ≤ 𝐴 → 0 < 𝐴 ) )
36 35 imp ⊢ ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) → 0 < 𝐴 )
37 32 36 elrpd ⊢ ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
38 relogcl ⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
39 rerpdivcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ 𝐴 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℝ )
40 38 39 mpancom ⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℝ )
41 37 40 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) → ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℝ )
42 axlttri ⊢ ( ( ( ( log ‘ 𝐵 ) / 𝐵 ) ∈ ℝ ∧ ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℝ ) → ( ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ↔ ¬ ( ( ( log ‘ 𝐵 ) / 𝐵 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) ∨ ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) ) )
43 31 41 42 syl2anr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ↔ ¬ ( ( ( log ‘ 𝐵 ) / 𝐵 ) = ( ( log ‘ 𝐴 ) / 𝐴 ) ∨ ( ( log ‘ 𝐴 ) / 𝐴 ) < ( ( log ‘ 𝐵 ) / 𝐵 ) ) ) )
44 axlttri ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) )
45 44 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( 𝐴 < 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 < 𝐴 ) ) )
46 18 43 45 3imtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) → 𝐴 < 𝐵 ) )
47 5 46 impbid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ e ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ e ≤ 𝐵 ) ) → ( 𝐴 < 𝐵 ↔ ( ( log ‘ 𝐵 ) / 𝐵 ) < ( ( log ‘ 𝐴 ) / 𝐴 ) ) )