Metamath Proof Explorer

Theorem cxpneg

Description: Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpneg 
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c -u B ) = ( 1 / ( A ^c B ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> A e. CC )
2 simp3 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> B e. CC )
3 cxpcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )
4 1 2 3 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) e. CC )
5 2 negcld 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> -u B e. CC )
6 cxpcl 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( A ^c -u B ) e. CC )
7 1 5 6 syl2anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c -u B ) e. CC )
8 cxpne0 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) =/= 0 )
9 2 negidd 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( B + -u B ) = 0 )
10 9 oveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c ( B + -u B ) ) = ( A ^c 0 ) )
11 simp2 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> A =/= 0 )
12 cxpadd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ -u B e. CC ) -> ( A ^c ( B + -u B ) ) = ( ( A ^c B ) x. ( A ^c -u B ) ) )
13 1 11 2 5 12 syl211anc 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c ( B + -u B ) ) = ( ( A ^c B ) x. ( A ^c -u B ) ) )
14 cxp0 
 |-  ( A e. CC -> ( A ^c 0 ) = 1 )
15 1 14 syl 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c 0 ) = 1 )
16 10 13 15 3eqtr3d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( ( A ^c B ) x. ( A ^c -u B ) ) = 1 )
17 4 7 8 16 mvllmuld 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c -u B ) = ( 1 / ( A ^c B ) ) )