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	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( logb ‘ ⟨ 𝐵 , 𝑋 ⟩ ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 𝐵 logb 𝑋 ) = ( logb ‘ ⟨ 𝐵 , 𝑋 ⟩ )
2		logbval	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
3	1 2	eqtr3id	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( logb ‘ ⟨ 𝐵 , 𝑋 ⟩ ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )