Metamath Proof Explorer


Definition df-logb

Description: Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as ( B logb X ) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition is according to Wikipedia "Complex logarithm": https://en.wikipedia.org/wiki/Complex_logarithm#Logarithms_to_other_bases (10-Jun-2020). (Contributed by David A. Wheeler, 21-Jan-2017)

Ref Expression
Assertion df-logb logb = x 0 1 , y 0 log y log x

Detailed syntax breakdown

Step Hyp Ref Expression
0 clogb class logb
1 vx setvar x
2 cc class
3 cc0 class 0
4 c1 class 1
5 3 4 cpr class 0 1
6 2 5 cdif class 0 1
7 vy setvar y
8 3 csn class 0
9 2 8 cdif class 0
10 clog class log
11 7 cv setvar y
12 11 10 cfv class log y
13 cdiv class ÷
14 1 cv setvar x
15 14 10 cfv class log x
16 12 15 13 co class log y log x
17 1 7 6 9 16 cmpo class x 0 1 , y 0 log y log x
18 0 17 wceq wff logb = x 0 1 , y 0 log y log x