This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )