Metamath Proof Explorer


Theorem logbfval

Description: The general logarithm of a complex number to a fixed base. (Contributed by AV, 11-Jun-2020)

Ref Expression
Assertion logbfval B B 0 B 1 X 0 curry logb B X = log B X

Proof

Step Hyp Ref Expression
1 df-logb logb = x 0 1 , y 0 log y log x
2 ovexd B B 0 B 1 X 0 x 0 1 y 0 log y log x V
3 2 ralrimivva B B 0 B 1 X 0 x 0 1 y 0 log y log x V
4 cnex V
5 difexg V 0 V
6 4 5 mp1i B B 0 B 1 X 0 0 V
7 eldifpr B 0 1 B B 0 B 1
8 7 biimpri B B 0 B 1 B 0 1
9 8 adantr B B 0 B 1 X 0 B 0 1
10 simpr B B 0 B 1 X 0 X 0
11 1 3 6 9 10 fvmpocurryd B B 0 B 1 X 0 curry logb B X = log B X