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