Metamath Proof Explorer


Theorem regt1loggt0

Description: The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion regt1loggt0 ( 𝐵 ∈ ( 1 (,) +∞ ) → 0 < ( log ‘ 𝐵 ) )

Proof

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 ‘ 𝐵 ) )