Step |
Hyp |
Ref |
Expression |
1 |
|
logcl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC ) |
2 |
1
|
3adant3 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` A ) e. CC ) |
3 |
|
relogcl |
|- ( B e. RR+ -> ( log ` B ) e. RR ) |
4 |
3
|
3ad2ant3 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` B ) e. RR ) |
5 |
4
|
recnd |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` B ) e. CC ) |
6 |
|
efsub |
|- ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) ) |
7 |
2 5 6
|
syl2anc |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) ) |
8 |
|
eflog |
|- ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A ) |
9 |
8
|
3adant3 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( log ` A ) ) = A ) |
10 |
|
reeflog |
|- ( B e. RR+ -> ( exp ` ( log ` B ) ) = B ) |
11 |
10
|
3ad2ant3 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( log ` B ) ) = B ) |
12 |
9 11
|
oveq12d |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( exp ` ( log ` A ) ) / ( exp ` ( log ` B ) ) ) = ( A / B ) ) |
13 |
7 12
|
eqtrd |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( exp ` ( ( log ` A ) - ( log ` B ) ) ) = ( A / B ) ) |
14 |
13
|
fveq2d |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( exp ` ( ( log ` A ) - ( log ` B ) ) ) ) = ( log ` ( A / B ) ) ) |
15 |
2 5
|
negsubd |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( log ` A ) + -u ( log ` B ) ) = ( ( log ` A ) - ( log ` B ) ) ) |
16 |
|
logrncl |
|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log ) |
17 |
16
|
3adant3 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` A ) e. ran log ) |
18 |
4
|
renegcld |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> -u ( log ` B ) e. RR ) |
19 |
|
logrnaddcl |
|- ( ( ( log ` A ) e. ran log /\ -u ( log ` B ) e. RR ) -> ( ( log ` A ) + -u ( log ` B ) ) e. ran log ) |
20 |
17 18 19
|
syl2anc |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( log ` A ) + -u ( log ` B ) ) e. ran log ) |
21 |
15 20
|
eqeltrrd |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( ( log ` A ) - ( log ` B ) ) e. ran log ) |
22 |
|
logef |
|- ( ( ( log ` A ) - ( log ` B ) ) e. ran log -> ( log ` ( exp ` ( ( log ` A ) - ( log ` B ) ) ) ) = ( ( log ` A ) - ( log ` B ) ) ) |
23 |
21 22
|
syl |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( exp ` ( ( log ` A ) - ( log ` B ) ) ) ) = ( ( log ` A ) - ( log ` B ) ) ) |
24 |
14 23
|
eqtr3d |
|- ( ( A e. CC /\ A =/= 0 /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) ) |