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 BB0B1logB1=0

Proof

Step Hyp Ref Expression
1 eldifpr B01BB0B1
2 ax-1cn 1
3 ax-1ne0 10
4 eldifsn 10110
5 2 3 4 mpbir2an 10
6 logbval B0110logB1=log1logB
7 5 6 mpan2 B01logB1=log1logB
8 1 7 sylbir BB0B1logB1=log1logB
9 log1 log1=0
10 9 oveq1i log1logB=0logB
11 simp1 BB0B1B
12 simp2 BB0B1B0
13 11 12 logcld BB0B1logB
14 logccne0 BB0B1logB0
15 13 14 div0d BB0B10logB=0
16 10 15 eqtrid BB0B1log1logB=0
17 8 16 eqtrd BB0B1logB1=0