Metamath Proof Explorer


Theorem logbleb

Description: The general logarithm function is monotone/increasing. See logleb . (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by AV, 31-May-2020)

Ref Expression
Assertion logbleb ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑋 ∈ ℝ+𝑌 ∈ ℝ+ ) → ( 𝑋𝑌 ↔ ( 𝐵 logb 𝑋 ) ≤ ( 𝐵 logb 𝑌 ) ) )

Proof

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 𝑌 ) ) )