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