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