Metamath Proof Explorer


Theorem rege1logbzge0

Description: The general logarithm, with an integer base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion rege1logbzge0 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑋 ∈ ( 1 [,) +∞ ) ) → 0 ≤ ( 𝐵 logb 𝑋 ) )

Proof

Step Hyp Ref Expression
1 zre ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
2 1 3ad2ant2 ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 2 ≤ 𝐵 ) → 𝐵 ∈ ℝ )
3 1lt2 1 < 2
4 1re 1 ∈ ℝ
5 4 a1i ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 1 ∈ ℝ )
6 2re 2 ∈ ℝ
7 6 a1i ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 2 ∈ ℝ )
8 1 adantl ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℝ )
9 ltletr ( ( 1 ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 1 < 2 ∧ 2 ≤ 𝐵 ) → 1 < 𝐵 ) )
10 5 7 8 9 syl3anc ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 1 < 2 ∧ 2 ≤ 𝐵 ) → 1 < 𝐵 ) )
11 3 10 mpani ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 2 ≤ 𝐵 → 1 < 𝐵 ) )
12 11 3impia ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 2 ≤ 𝐵 ) → 1 < 𝐵 )
13 2 12 jca ( ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 2 ≤ 𝐵 ) → ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) )
14 eluz2 ( 𝐵 ∈ ( ℤ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 2 ≤ 𝐵 ) )
15 1xr 1 ∈ ℝ*
16 elioopnf ( 1 ∈ ℝ* → ( 𝐵 ∈ ( 1 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) )
17 15 16 ax-mp ( 𝐵 ∈ ( 1 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) )
18 13 14 17 3imtr4i ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ( 1 (,) +∞ ) )
19 rege1logbrege0 ( ( 𝐵 ∈ ( 1 (,) +∞ ) ∧ 𝑋 ∈ ( 1 [,) +∞ ) ) → 0 ≤ ( 𝐵 logb 𝑋 ) )
20 18 19 sylan ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝑋 ∈ ( 1 [,) +∞ ) ) → 0 ≤ ( 𝐵 logb 𝑋 ) )