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 syl5eq B B 0 B 1 log 1 log B = 0
17 8 16 eqtrd B B 0 B 1 log B 1 = 0