Metamath Proof Explorer


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 A + 0 log A 1 A

Proof

Step Hyp Ref Expression
1 1rp 1 +
2 1 a1i A + 1 +
3 id A + A +
4 2 3 logled A + 1 A log 1 log A
5 log1 log 1 = 0
6 5 a1i A + log 1 = 0
7 6 breq1d A + log 1 log A 0 log A
8 4 7 bitr2d A + 0 log A 1 A