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

Metamath Proof Explorer

Theorem logb1

Description: The logarithm of 1 to an arbitrary base B is 0. Property 1(b) of Cohen4 p. 361. See log1 . (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

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

Proof

Step Hyp Ref Expression
1 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
2 ax-1cn 
 |-  1 e. CC
3 ax-1ne0 
 |-  1 =/= 0
4 eldifsn 
 |-  ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ 1 =/= 0 ) )
5 2 3 4 mpbir2an 
 |-  1 e. ( CC \ { 0 } )
6 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ 1 e. ( CC \ { 0 } ) ) -> ( B logb 1 ) = ( ( log ` 1 ) / ( log ` B ) ) )
7 5 6 mpan2 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( B logb 1 ) = ( ( log ` 1 ) / ( log ` B ) ) )
8 1 7 sylbir 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B logb 1 ) = ( ( log ` 1 ) / ( log ` B ) ) )
9 log1 
 |-  ( log ` 1 ) = 0
10 9 oveq1i 
 |-  ( ( log ` 1 ) / ( log ` B ) ) = ( 0 / ( log ` B ) )
11 simp1 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> B e. CC )
12 simp2 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> B =/= 0 )
13 11 12 logcld 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) e. CC )
14 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
15 13 14 div0d 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( 0 / ( log ` B ) ) = 0 )
16 10 15 eqtrid 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( ( log ` 1 ) / ( log ` B ) ) = 0 )
17 8 16 eqtrd 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B logb 1 ) = 0 )