Step |
Hyp |
Ref |
Expression |
1 |
|
df-logb |
|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) ) |
2 |
|
ovexd |
|- ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ ( x e. ( CC \ { 0 , 1 } ) /\ y e. ( CC \ { 0 } ) ) ) -> ( ( log ` y ) / ( log ` x ) ) e. _V ) |
3 |
2
|
ralrimivva |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> A. x e. ( CC \ { 0 , 1 } ) A. y e. ( CC \ { 0 } ) ( ( log ` y ) / ( log ` x ) ) e. _V ) |
4 |
|
ax-1cn |
|- 1 e. CC |
5 |
|
ax-1ne0 |
|- 1 =/= 0 |
6 |
|
elsng |
|- ( 1 e. CC -> ( 1 e. { 0 } <-> 1 = 0 ) ) |
7 |
4 6
|
ax-mp |
|- ( 1 e. { 0 } <-> 1 = 0 ) |
8 |
5 7
|
nemtbir |
|- -. 1 e. { 0 } |
9 |
|
eldif |
|- ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ -. 1 e. { 0 } ) ) |
10 |
4 8 9
|
mpbir2an |
|- 1 e. ( CC \ { 0 } ) |
11 |
10
|
ne0ii |
|- ( CC \ { 0 } ) =/= (/) |
12 |
11
|
a1i |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( CC \ { 0 } ) =/= (/) ) |
13 |
|
cnex |
|- CC e. _V |
14 |
13
|
difexi |
|- ( CC \ { 0 } ) e. _V |
15 |
14
|
a1i |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( CC \ { 0 } ) e. _V ) |
16 |
|
eldifpr |
|- ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) ) |
17 |
16
|
biimpri |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> B e. ( CC \ { 0 , 1 } ) ) |
18 |
1 3 12 15 17
|
mpocurryvald |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( y e. ( CC \ { 0 } ) |-> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) ) ) |
19 |
|
csbov2g |
|- ( B e. CC -> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) = ( ( log ` y ) / [_ B / x ]_ ( log ` x ) ) ) |
20 |
|
csbfv |
|- [_ B / x ]_ ( log ` x ) = ( log ` B ) |
21 |
20
|
a1i |
|- ( B e. CC -> [_ B / x ]_ ( log ` x ) = ( log ` B ) ) |
22 |
21
|
oveq2d |
|- ( B e. CC -> ( ( log ` y ) / [_ B / x ]_ ( log ` x ) ) = ( ( log ` y ) / ( log ` B ) ) ) |
23 |
19 22
|
eqtrd |
|- ( B e. CC -> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) = ( ( log ` y ) / ( log ` B ) ) ) |
24 |
23
|
3ad2ant1 |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) = ( ( log ` y ) / ( log ` B ) ) ) |
25 |
24
|
mpteq2dv |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( y e. ( CC \ { 0 } ) |-> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` B ) ) ) ) |
26 |
18 25
|
eqtrd |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` B ) ) ) ) |