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 ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 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 eqtrid ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( ( log ‘ 1 ) / ( log ‘ 𝐵 ) ) = 0 )
17 8 16 eqtrd ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 1 ) = 0 )