Step |
Hyp |
Ref |
Expression |
1 |
|
simp2 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝑋 ∈ ℝ+ ) |
2 |
1
|
relogcld |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( log ‘ 𝑋 ) ∈ ℝ ) |
3 |
|
simp3 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝑌 ∈ ℝ+ ) |
4 |
3
|
relogcld |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( log ‘ 𝑌 ) ∈ ℝ ) |
5 |
|
eluzelre |
⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ ) |
6 |
5
|
3ad2ant1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝐵 ∈ ℝ ) |
7 |
|
1z |
⊢ 1 ∈ ℤ |
8 |
|
simp1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) |
9 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
10 |
9
|
fveq2i |
⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) = ( ℤ≥ ‘ 2 ) |
11 |
8 10
|
eleqtrrdi |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝐵 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) |
12 |
|
eluzp1l |
⊢ ( ( 1 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 1 < 𝐵 ) |
13 |
7 11 12
|
sylancr |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 1 < 𝐵 ) |
14 |
6 13
|
rplogcld |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℝ+ ) |
15 |
2 4 14
|
lediv1d |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( ( log ‘ 𝑋 ) ≤ ( log ‘ 𝑌 ) ↔ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ≤ ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) ) ) |
16 |
|
logleb |
⊢ ( ( 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝑋 ≤ 𝑌 ↔ ( log ‘ 𝑋 ) ≤ ( log ‘ 𝑌 ) ) ) |
17 |
16
|
3adant1 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝑋 ≤ 𝑌 ↔ ( log ‘ 𝑋 ) ≤ ( log ‘ 𝑌 ) ) ) |
18 |
|
relogbval |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) |
19 |
18
|
3adant3 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ) |
20 |
|
relogbval |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑌 ∈ ℝ+ ) → ( 𝐵 logb 𝑌 ) = ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) ) |
21 |
20
|
3adant2 |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝐵 logb 𝑌 ) = ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) ) |
22 |
19 21
|
breq12d |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( ( 𝐵 logb 𝑋 ) ≤ ( 𝐵 logb 𝑌 ) ↔ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ≤ ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) ) ) |
23 |
15 17 22
|
3bitr4d |
⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝐵 logb 𝑋 ) ≤ ( 𝐵 logb 𝑌 ) ) ) |