Metamath Proof Explorer

Theorem logblt1b

Description: The logarithm of a number is less than 1 iff the number is less than the base of the logarithm. (Contributed by AV, 30-May-2020)

Ref Expression
Assertion logblt1b ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( 𝐵 logb 𝑋 ) < 1 ↔ 𝑋 < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 relogbval ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
2 1 breq1d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( 𝐵 logb 𝑋 ) < 1 ↔ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) < 1 ) )
3 relogcl ⊢ ( 𝑋 ∈ ℝ+ → ( log ‘ 𝑋 ) ∈ ℝ )
4 3 adantl ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( log ‘ 𝑋 ) ∈ ℝ )
5 1red ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → 1 ∈ ℝ )
6 eluz2nn ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℕ )
7 6 nnrpd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ+ )
8 relogcl ⊢ ( 𝐵 ∈ ℝ+ → ( log ‘ 𝐵 ) ∈ ℝ )
9 7 8 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( log ‘ 𝐵 ) ∈ ℝ )
10 eluz2gt1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐵 )
11 loggt0b ⊢ ( 𝐵 ∈ ℝ+ → ( 0 < ( log ‘ 𝐵 ) ↔ 1 < 𝐵 ) )
12 7 11 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 0 < ( log ‘ 𝐵 ) ↔ 1 < 𝐵 ) )
13 10 12 mpbird ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 0 < ( log ‘ 𝐵 ) )
14 9 13 jca ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( ( log ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( log ‘ 𝐵 ) ) )
15 14 adantr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( log ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( log ‘ 𝐵 ) ) )
16 ltdivmul ⊢ ( ( ( log ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( log ‘ 𝐵 ) ∈ ℝ ∧ 0 < ( log ‘ 𝐵 ) ) ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) < 1 ↔ ( log ‘ 𝑋 ) < ( ( log ‘ 𝐵 ) · 1 ) ) )
17 4 5 15 16 syl3anc ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) < 1 ↔ ( log ‘ 𝑋 ) < ( ( log ‘ 𝐵 ) · 1 ) ) )
18 9 recnd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( log ‘ 𝐵 ) ∈ ℂ )
19 18 mulid1d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( ( log ‘ 𝐵 ) · 1 ) = ( log ‘ 𝐵 ) )
20 19 adantr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( log ‘ 𝐵 ) · 1 ) = ( log ‘ 𝐵 ) )
21 20 breq2d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( log ‘ 𝑋 ) < ( ( log ‘ 𝐵 ) · 1 ) ↔ ( log ‘ 𝑋 ) < ( log ‘ 𝐵 ) ) )
22 7 anim2i ⊢ ( ( 𝑋 ∈ ℝ+ ∧ 𝐵 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑋 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) )
23 22 ancoms ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( 𝑋 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) )
24 logltb ⊢ ( ( 𝑋 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 𝑋 < 𝐵 ↔ ( log ‘ 𝑋 ) < ( log ‘ 𝐵 ) ) )
25 24 bicomd ⊢ ( ( 𝑋 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( ( log ‘ 𝑋 ) < ( log ‘ 𝐵 ) ↔ 𝑋 < 𝐵 ) )
26 23 25 syl ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( log ‘ 𝑋 ) < ( log ‘ 𝐵 ) ↔ 𝑋 < 𝐵 ) )
27 21 26 bitrd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( log ‘ 𝑋 ) < ( ( log ‘ 𝐵 ) · 1 ) ↔ 𝑋 < 𝐵 ) )
28 17 27 bitrd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) < 1 ↔ 𝑋 < 𝐵 ) )
29 2 28 bitrd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑋 ∈ ℝ+ ) → ( ( 𝐵 logb 𝑋 ) < 1 ↔ 𝑋 < 𝐵 ) )