Metamath Proof Explorer

Theorem logblt

Description: The general logarithm function is strictly monotone/increasing. Property 2 of Cohen4 p. 377. See logltb . (Contributed by Stefan O'Rear, 19-Oct-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion logblt ( ( 𝐵 ∈ ( ℤ≥ ‘ 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 simp1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝐵 ∈ ( ℤ≥ ‘ 2 ) )
6 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℤ )
7 5 6 syl ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝐵 ∈ ℤ )
8 7 zred ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
9 1z ⊢ 1 ∈ ℤ
10 1p1e2 ⊢ ( 1 + 1 ) = 2
11 10 fveq2i ⊢ ( ℤ≥ ‘ ( 1 + 1 ) ) = ( ℤ≥ ‘ 2 )
12 5 11 eleqtrrdi ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 𝐵 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) )
13 eluzp1l ⊢ ( ( 1 ∈ ℤ ∧ 𝐵 ∈ ( ℤ≥ ‘ ( 1 + 1 ) ) ) → 1 < 𝐵 )
14 9 12 13 sylancr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → 1 < 𝐵 )
15 8 14 rplogcld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( log ‘ 𝐵 ) ∈ ℝ+ )
16 2 4 15 ltdiv1d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( ( log ‘ 𝑋 ) < ( log ‘ 𝑌 ) ↔ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) < ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) ) )
17 logltb ⊢ ( ( 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝑋 < 𝑌 ↔ ( log ‘ 𝑋 ) < ( log ‘ 𝑌 ) ) )
18 17 3adant1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝑋 < 𝑌 ↔ ( log ‘ 𝑋 ) < ( log ‘ 𝑌 ) ) )
19 relogbval ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
20 19 3adant3 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
21 relogbval ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑌 ∈ ℝ+ ) → ( 𝐵 logb 𝑌 ) = ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) )
22 21 3adant2 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝐵 logb 𝑌 ) = ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) )
23 20 22 breq12d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( ( 𝐵 logb 𝑋 ) < ( 𝐵 logb 𝑌 ) ↔ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) < ( ( log ‘ 𝑌 ) / ( log ‘ 𝐵 ) ) ) )
24 16 18 23 3bitr4d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ∧ 𝑌 ∈ ℝ+ ) → ( 𝑋 < 𝑌 ↔ ( 𝐵 logb 𝑋 ) < ( 𝐵 logb 𝑌 ) ) )