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 e. RR+ /\ C =/= 1 ) -> ( ( log ` C ) / ( log ` C ) ) = 1 )

Proof

Step Hyp Ref Expression
1 relogcl
 |-  ( C e. RR+ -> ( log ` C ) e. RR )
2 1 recnd
 |-  ( C e. RR+ -> ( log ` C ) e. CC )
3 2 adantr
 |-  ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) e. CC )
4 logne0
 |-  ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) =/= 0 )
5 3 4 dividd
 |-  ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` C ) / ( log ` C ) ) = 1 )