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