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	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 1 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		eldifpr	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
2		ax-1cn	⊢ 1 ∈ ℂ
3		ax-1ne0	⊢ 1 ≠ 0
4		eldifsn	⊢ ( 1 ∈ ( ℂ ∖ { 0 } ) ↔ ( 1 ∈ ℂ ∧ 1 ≠ 0 ) )
5	2 3 4	mpbir2an	⊢ 1 ∈ ( ℂ ∖ { 0 } )
6		logbval	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 1 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 1 ) = ( ( log ‘ 1 ) / ( log ‘ 𝐵 ) ) )
7	5 6	mpan2	⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) → ( 𝐵 logb 1 ) = ( ( log ‘ 1 ) / ( log ‘ 𝐵 ) ) )
8	1 7	sylbir	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 1 ) = ( ( log ‘ 1 ) / ( log ‘ 𝐵 ) ) )
9		log1	⊢ ( log ‘ 1 ) = 0
10	9	oveq1i	⊢ ( ( log ‘ 1 ) / ( log ‘ 𝐵 ) ) = ( 0 / ( log ‘ 𝐵 ) )
11		simp1	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ℂ )
12		simp2	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 0 )
13	11 12	logcld	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ∈ ℂ )
14		logccne0	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
15	13 14	div0d	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 0 / ( log ‘ 𝐵 ) ) = 0 )
16	10 15	syl5eq	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( ( log ‘ 1 ) / ( log ‘ 𝐵 ) ) = 0 )
17	8 16	eqtrd	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 1 ) = 0 )