Theorem logbval

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

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝐵 → ( log ‘ 𝑥 ) = ( log ‘ 𝐵 ) )
2	1	oveq2d	⊢ ( 𝑥 = 𝐵 → ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) )
3		fveq2	⊢ ( 𝑦 = 𝑋 → ( log ‘ 𝑦 ) = ( log ‘ 𝑋 ) )
4	3	oveq1d	⊢ ( 𝑦 = 𝑋 → ( ( log ‘ 𝑦 ) / ( log ‘ 𝐵 ) ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )
5		df-logb	⊢ logb = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )
6		ovex	⊢ ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) ∈ V
7	2 4 5 6	ovmpo	⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑋 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb 𝑋 ) = ( ( log ‘ 𝑋 ) / ( log ‘ 𝐵 ) ) )