Metamath Proof Explorer


Theorem reglogbas

Description: General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use logbid1 instead.

Ref Expression
Assertion reglogbas C + C 1 log C log C = 1

Proof

Step Hyp Ref Expression
1 relogcl C + log C
2 1 recnd C + log C
3 2 adantr C + C 1 log C
4 logne0 C + C 1 log C 0
5 3 4 dividd C + C 1 log C log C = 1