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