Theorem logge0

Description: The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	logge0	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( log ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		log1	⊢ ( log ‘ 1 ) = 0
2		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ 𝐴 )
3		1rp	⊢ 1 ∈ ℝ+
4		rpgecl	⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
5	3 4	mp3an1	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ )
6		logleb	⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
7	3 5 6	sylancr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
8	2 7	mpbid	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) )
9	1 8	eqbrtrrid	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( log ‘ 𝐴 ) )