Step |
Hyp |
Ref |
Expression |
1 |
|
rpcndif0 |
|- ( x e. RR+ -> x e. ( CC \ { 0 } ) ) |
2 |
1
|
adantl |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> x e. ( CC \ { 0 } ) ) |
3 |
|
rpcn |
|- ( B e. RR+ -> B e. CC ) |
4 |
3
|
adantr |
|- ( ( B e. RR+ /\ 1 < B ) -> B e. CC ) |
5 |
|
rpne0 |
|- ( B e. RR+ -> B =/= 0 ) |
6 |
5
|
adantr |
|- ( ( B e. RR+ /\ 1 < B ) -> B =/= 0 ) |
7 |
|
animorr |
|- ( ( B e. RR+ /\ 1 < B ) -> ( B < 1 \/ 1 < B ) ) |
8 |
|
rpre |
|- ( B e. RR+ -> B e. RR ) |
9 |
|
1red |
|- ( 1 < B -> 1 e. RR ) |
10 |
|
lttri2 |
|- ( ( B e. RR /\ 1 e. RR ) -> ( B =/= 1 <-> ( B < 1 \/ 1 < B ) ) ) |
11 |
8 9 10
|
syl2an |
|- ( ( B e. RR+ /\ 1 < B ) -> ( B =/= 1 <-> ( B < 1 \/ 1 < B ) ) ) |
12 |
7 11
|
mpbird |
|- ( ( B e. RR+ /\ 1 < B ) -> B =/= 1 ) |
13 |
4 6 12
|
3jca |
|- ( ( B e. RR+ /\ 1 < B ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) ) |
14 |
|
logbmpt |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) ) |
15 |
13 14
|
syl |
|- ( ( B e. RR+ /\ 1 < B ) -> ( curry logb ` B ) = ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) ) |
16 |
15
|
dmeqd |
|- ( ( B e. RR+ /\ 1 < B ) -> dom ( curry logb ` B ) = dom ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) ) |
17 |
|
ovexd |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. ( CC \ { 0 } ) ) -> ( ( log ` x ) / ( log ` B ) ) e. _V ) |
18 |
17
|
ralrimiva |
|- ( ( B e. RR+ /\ 1 < B ) -> A. x e. ( CC \ { 0 } ) ( ( log ` x ) / ( log ` B ) ) e. _V ) |
19 |
|
dmmptg |
|- ( A. x e. ( CC \ { 0 } ) ( ( log ` x ) / ( log ` B ) ) e. _V -> dom ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) = ( CC \ { 0 } ) ) |
20 |
18 19
|
syl |
|- ( ( B e. RR+ /\ 1 < B ) -> dom ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` B ) ) ) = ( CC \ { 0 } ) ) |
21 |
16 20
|
eqtrd |
|- ( ( B e. RR+ /\ 1 < B ) -> dom ( curry logb ` B ) = ( CC \ { 0 } ) ) |
22 |
21
|
adantr |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> dom ( curry logb ` B ) = ( CC \ { 0 } ) ) |
23 |
2 22
|
eleqtrrd |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> x e. dom ( curry logb ` B ) ) |
24 |
|
logbfval |
|- ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ x e. ( CC \ { 0 } ) ) -> ( ( curry logb ` B ) ` x ) = ( B logb x ) ) |
25 |
13 1 24
|
syl2an |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( ( curry logb ` B ) ` x ) = ( B logb x ) ) |
26 |
|
simpll |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> B e. RR+ ) |
27 |
|
simpr |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> x e. RR+ ) |
28 |
12
|
adantr |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> B =/= 1 ) |
29 |
26 27 28
|
3jca |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( B e. RR+ /\ x e. RR+ /\ B =/= 1 ) ) |
30 |
|
relogbcl |
|- ( ( B e. RR+ /\ x e. RR+ /\ B =/= 1 ) -> ( B logb x ) e. RR ) |
31 |
29 30
|
syl |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( B logb x ) e. RR ) |
32 |
25 31
|
eqeltrd |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( ( curry logb ` B ) ` x ) e. RR ) |
33 |
23 32
|
jca |
|- ( ( ( B e. RR+ /\ 1 < B ) /\ x e. RR+ ) -> ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) ) |
34 |
33
|
ralrimiva |
|- ( ( B e. RR+ /\ 1 < B ) -> A. x e. RR+ ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) ) |
35 |
|
logbf |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) : ( CC \ { 0 } ) --> CC ) |
36 |
13 35
|
syl |
|- ( ( B e. RR+ /\ 1 < B ) -> ( curry logb ` B ) : ( CC \ { 0 } ) --> CC ) |
37 |
|
ffun |
|- ( ( curry logb ` B ) : ( CC \ { 0 } ) --> CC -> Fun ( curry logb ` B ) ) |
38 |
|
ffvresb |
|- ( Fun ( curry logb ` B ) -> ( ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR <-> A. x e. RR+ ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) ) ) |
39 |
36 37 38
|
3syl |
|- ( ( B e. RR+ /\ 1 < B ) -> ( ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR <-> A. x e. RR+ ( x e. dom ( curry logb ` B ) /\ ( ( curry logb ` B ) ` x ) e. RR ) ) ) |
40 |
34 39
|
mpbird |
|- ( ( B e. RR+ /\ 1 < B ) -> ( ( curry logb ` B ) |` RR+ ) : RR+ --> RR ) |