Metamath Proof Explorer


Theorem cxprec

Description: Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxprec
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) )

Proof

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 ) ) )