Theorem logbid1

Description: General logarithm is 1 when base and arg match. Property 1(a) of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by David A. Wheeler, 22-Jul-2017)

	Ref	Expression
Assertion	logbid1	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A logb A ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		eldifpr	|- ( A e. ( CC \ { 0 , 1 } ) <-> ( A e. CC /\ A =/= 0 /\ A =/= 1 ) )
2	1	biimpri	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A e. ( CC \ { 0 , 1 } ) )
3		eldifsn	|- ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
4	3	biimpri	|- ( ( A e. CC /\ A =/= 0 ) -> A e. ( CC \ { 0 } ) )
5	4	3adant3	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A e. ( CC \ { 0 } ) )
6		logbval	|- ( ( A e. ( CC \ { 0 , 1 } ) /\ A e. ( CC \ { 0 } ) ) -> ( A logb A ) = ( ( log ` A ) / ( log ` A ) ) )
7	2 5 6	syl2anc	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A logb A ) = ( ( log ` A ) / ( log ` A ) ) )
8		logcl	|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
9	8	3adant3	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) e. CC )
10		logccne0	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 )
11	9 10	dividd	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( log ` A ) / ( log ` A ) ) = 1 )
12	7 11	eqtrd	|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A logb A ) = 1 )