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