This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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