Step |
Hyp |
Ref |
Expression |
1 |
|
rpcn |
|- ( A e. RR+ -> A e. CC ) |
2 |
|
cxpcl |
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC ) |
3 |
1 2
|
sylan |
|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) e. CC ) |
4 |
|
rpreccl |
|- ( A e. RR+ -> ( 1 / A ) e. RR+ ) |
5 |
4
|
rpcnd |
|- ( A e. RR+ -> ( 1 / A ) e. CC ) |
6 |
|
cxpcl |
|- ( ( ( 1 / A ) e. CC /\ B e. CC ) -> ( ( 1 / A ) ^c B ) e. CC ) |
7 |
5 6
|
sylan |
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) e. CC ) |
8 |
1
|
adantr |
|- ( ( A e. RR+ /\ B e. CC ) -> A e. CC ) |
9 |
|
rpne0 |
|- ( A e. RR+ -> A =/= 0 ) |
10 |
9
|
adantr |
|- ( ( A e. RR+ /\ B e. CC ) -> A =/= 0 ) |
11 |
|
simpr |
|- ( ( A e. RR+ /\ B e. CC ) -> B e. CC ) |
12 |
|
cxpne0 |
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) =/= 0 ) |
13 |
8 10 11 12
|
syl3anc |
|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) =/= 0 ) |
14 |
8 10
|
recidd |
|- ( ( A e. RR+ /\ B e. CC ) -> ( A x. ( 1 / A ) ) = 1 ) |
15 |
14
|
oveq1d |
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( A x. ( 1 / A ) ) ^c B ) = ( 1 ^c B ) ) |
16 |
|
rprege0 |
|- ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) ) |
17 |
16
|
adantr |
|- ( ( A e. RR+ /\ B e. CC ) -> ( A e. RR /\ 0 <_ A ) ) |
18 |
4
|
rprege0d |
|- ( A e. RR+ -> ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) ) |
19 |
18
|
adantr |
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) ) |
20 |
|
mulcxp |
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( ( 1 / A ) e. RR /\ 0 <_ ( 1 / A ) ) /\ B e. CC ) -> ( ( A x. ( 1 / A ) ) ^c B ) = ( ( A ^c B ) x. ( ( 1 / A ) ^c B ) ) ) |
21 |
17 19 11 20
|
syl3anc |
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( A x. ( 1 / A ) ) ^c B ) = ( ( A ^c B ) x. ( ( 1 / A ) ^c B ) ) ) |
22 |
|
1cxp |
|- ( B e. CC -> ( 1 ^c B ) = 1 ) |
23 |
11 22
|
syl |
|- ( ( A e. RR+ /\ B e. CC ) -> ( 1 ^c B ) = 1 ) |
24 |
15 21 23
|
3eqtr3d |
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( A ^c B ) x. ( ( 1 / A ) ^c B ) ) = 1 ) |
25 |
3 7 13 24
|
mvllmuld |
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) ) |