Theorem logge0b

Description: The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	logge0b	⊢ ( 𝐴 ∈ ℝ+ → ( 0 ≤ ( log ‘ 𝐴 ) ↔ 1 ≤ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		1rp	⊢ 1 ∈ ℝ+
2	1	a1i	⊢ ( 𝐴 ∈ ℝ+ → 1 ∈ ℝ+ )
3		id	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ+ )
4	2 3	logled	⊢ ( 𝐴 ∈ ℝ+ → ( 1 ≤ 𝐴 ↔ ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ) )
5		log1	⊢ ( log ‘ 1 ) = 0
6	5	a1i	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 1 ) = 0 )
7	6	breq1d	⊢ ( 𝐴 ∈ ℝ+ → ( ( log ‘ 1 ) ≤ ( log ‘ 𝐴 ) ↔ 0 ≤ ( log ‘ 𝐴 ) ) )
8	4 7	bitr2d	⊢ ( 𝐴 ∈ ℝ+ → ( 0 ≤ ( log ‘ 𝐴 ) ↔ 1 ≤ 𝐴 ) )