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 ) |
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 ) |