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 ⊢ B ∈ ℤ ≥ 2 ∧ X ∈ 1 +∞ → 0 ≤ log B X

Proof

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