Step |
Hyp |
Ref |
Expression |
1 |
|
1xr |
⊢ 1 ∈ ℝ* |
2 |
|
elioopnf |
⊢ ( 1 ∈ ℝ* → ( 𝐵 ∈ ( 1 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ) |
4 |
3
|
simprbi |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) → 1 < 𝐵 ) |
5 |
|
log1 |
⊢ ( log ‘ 1 ) = 0 |
6 |
5
|
eqcomi |
⊢ 0 = ( log ‘ 1 ) |
7 |
6
|
a1i |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) → 0 = ( log ‘ 1 ) ) |
8 |
7
|
breq1d |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) → ( 0 < ( log ‘ 𝐵 ) ↔ ( log ‘ 1 ) < ( log ‘ 𝐵 ) ) ) |
9 |
|
1rp |
⊢ 1 ∈ ℝ+ |
10 |
|
0lt1 |
⊢ 0 < 1 |
11 |
|
0red |
⊢ ( 𝐵 ∈ ℝ → 0 ∈ ℝ ) |
12 |
|
1red |
⊢ ( 𝐵 ∈ ℝ → 1 ∈ ℝ ) |
13 |
|
id |
⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ ) |
14 |
|
lttr |
⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝐵 ) → 0 < 𝐵 ) ) |
15 |
11 12 13 14
|
syl3anc |
⊢ ( 𝐵 ∈ ℝ → ( ( 0 < 1 ∧ 1 < 𝐵 ) → 0 < 𝐵 ) ) |
16 |
10 15
|
mpani |
⊢ ( 𝐵 ∈ ℝ → ( 1 < 𝐵 → 0 < 𝐵 ) ) |
17 |
16
|
imdistani |
⊢ ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) → ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) |
18 |
|
elrp |
⊢ ( 𝐵 ∈ ℝ+ ↔ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) |
19 |
17 3 18
|
3imtr4i |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) → 𝐵 ∈ ℝ+ ) |
20 |
|
logltb |
⊢ ( ( 1 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ) → ( 1 < 𝐵 ↔ ( log ‘ 1 ) < ( log ‘ 𝐵 ) ) ) |
21 |
9 19 20
|
sylancr |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) → ( 1 < 𝐵 ↔ ( log ‘ 1 ) < ( log ‘ 𝐵 ) ) ) |
22 |
8 21
|
bitr4d |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) → ( 0 < ( log ‘ 𝐵 ) ↔ 1 < 𝐵 ) ) |
23 |
4 22
|
mpbird |
⊢ ( 𝐵 ∈ ( 1 (,) +∞ ) → 0 < ( log ‘ 𝐵 ) ) |