Description: Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017) (Revised by David A. Wheeler, 16-Jul-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | logbval | |- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fveq2 | |- ( x = B -> ( log ` x ) = ( log ` B ) ) |
|
| 2 | 1 | oveq2d | |- ( x = B -> ( ( log ` y ) / ( log ` x ) ) = ( ( log ` y ) / ( log ` B ) ) ) |
| 3 | fveq2 | |- ( y = X -> ( log ` y ) = ( log ` X ) ) |
|
| 4 | 3 | oveq1d | |- ( y = X -> ( ( log ` y ) / ( log ` B ) ) = ( ( log ` X ) / ( log ` B ) ) ) |
| 5 | df-logb | |- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) ) |
|
| 6 | ovex | |- ( ( log ` X ) / ( log ` B ) ) e. _V |
|
| 7 | 2 4 5 6 | ovmpo | |- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) ) |