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 ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log B 1 = 0

Proof

Step Hyp Ref Expression
1 eldifpr ⊢ B ∈ ℂ ∖ 0 1 ↔ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 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 ⊢ B ∈ ℂ ∖ 0 1 ∧ 1 ∈ ℂ ∖ 0 → log B 1 = log ⁡ 1 log ⁡ B
7 5 6 mpan2 ⊢ B ∈ ℂ ∖ 0 1 → log B 1 = log ⁡ 1 log ⁡ B
8 1 7 sylbir ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log B 1 = log ⁡ 1 log ⁡ B
9 log1 ⊢ log ⁡ 1 = 0
10 9 oveq1i ⊢ log ⁡ 1 log ⁡ B = 0 log ⁡ B
11 simp1 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → B ∈ ℂ
12 simp2 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → B ≠ 0
13 11 12 logcld ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log ⁡ B ∈ ℂ
14 logccne0 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log ⁡ B ≠ 0
15 13 14 div0d ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → 0 log ⁡ B = 0
16 10 15 eqtrid ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log ⁡ 1 log ⁡ B = 0
17 8 16 eqtrd ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log B 1 = 0