This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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