Metamath Proof Explorer

Theorem logb2aval

Description: Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb <. B , X >. (Contributed by David A. Wheeler, 21-Jan-2017) (Revised by David A. Wheeler, 16-Jul-2017)

		Ref	Expression
	Assertion	logb2aval	\|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( logb ` <. B , X >. ) = ( ( log ` X ) / ( log ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ov	\|- ( B logb X ) = ( logb ` <. B , X >. )
2		logbval	\|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
3	1 2	eqtr3id	\|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( logb ` <. B , X >. ) = ( ( log ` X ) / ( log ` B ) ) )

Step

Hyp

Ref

Expression

df-ov

 |-  ( B logb X ) = ( logb ` <. B , X >. )

logbval

 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )

1 2

eqtr3id

 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( logb ` <. B , X >. ) = ( ( log ` X ) / ( log ` B ) ) )