Theorem reglog1

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

	Ref	Expression
Assertion	reglog1	|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` 1 ) / ( log ` C ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		log1	|- ( log ` 1 ) = 0
2	1	oveq1i	|- ( ( log ` 1 ) / ( log ` C ) ) = ( 0 / ( log ` C ) )
3		relogcl	|- ( C e. RR+ -> ( log ` C ) e. RR )
4	3	recnd	|- ( C e. RR+ -> ( log ` C ) e. CC )
5	4	adantr	|- ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) e. CC )
6		logne0	|- ( ( C e. RR+ /\ C =/= 1 ) -> ( log ` C ) =/= 0 )
7	5 6	div0d	|- ( ( C e. RR+ /\ C =/= 1 ) -> ( 0 / ( log ` C ) ) = 0 )
8	2 7	syl5eq	|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` 1 ) / ( log ` C ) ) = 0 )