Step |
Hyp |
Ref |
Expression |
1 |
|
logbval |
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) ) |
2 |
|
eldifsn |
|- ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) ) |
3 |
|
logcl |
|- ( ( X e. CC /\ X =/= 0 ) -> ( log ` X ) e. CC ) |
4 |
2 3
|
sylbi |
|- ( X e. ( CC \ { 0 } ) -> ( log ` X ) e. CC ) |
5 |
4
|
adantl |
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` X ) e. CC ) |
6 |
|
eldifi |
|- ( B e. ( CC \ { 0 , 1 } ) -> B e. CC ) |
7 |
|
eldifpr |
|- ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) ) |
8 |
7
|
simp2bi |
|- ( B e. ( CC \ { 0 , 1 } ) -> B =/= 0 ) |
9 |
6 8
|
logcld |
|- ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) e. CC ) |
10 |
9
|
adantr |
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) e. CC ) |
11 |
|
logccne0 |
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 ) |
12 |
7 11
|
sylbi |
|- ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) =/= 0 ) |
13 |
12
|
adantr |
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) =/= 0 ) |
14 |
5 10 13
|
divcld |
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( ( log ` X ) / ( log ` B ) ) e. CC ) |
15 |
1 14
|
eqeltrd |
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) e. CC ) |