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 = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clogb ⊢ logb
1 vx ⊢ 𝑥
2 cc ⊢ ℂ
3 cc0 ⊢ 0
4 c1 ⊢ 1
5 3 4 cpr ⊢ { 0 , 1 }
6 2 5 cdif ⊢ ( ℂ ∖ { 0 , 1 } )
7 vy ⊢ 𝑦
8 3 csn ⊢ { 0 }
9 2 8 cdif ⊢ ( ℂ ∖ { 0 } )
10 clog ⊢ log
11 7 cv ⊢ 𝑦
12 11 10 cfv ⊢ ( log ‘ 𝑦 )
13 cdiv ⊢ /
14 1 cv ⊢ 𝑥
15 14 10 cfv ⊢ ( log ‘ 𝑥 )
16 12 15 13 co ⊢ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) )
17 1 7 6 9 16 cmpo ⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )
18 0 17 wceq ⊢ logb = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )