Metamath Proof Explorer


Theorem cxpsub

Description: Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion cxpsub
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B - C ) ) = ( ( A ^c B ) / ( A ^c C ) ) )

Proof

Step Hyp Ref Expression
1 negcl
 |-  ( C e. CC -> -u C e. CC )
2 cxpadd
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ -u C e. CC ) -> ( A ^c ( B + -u C ) ) = ( ( A ^c B ) x. ( A ^c -u C ) ) )
3 1 2 syl3an3
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + -u C ) ) = ( ( A ^c B ) x. ( A ^c -u C ) ) )
4 simp2
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> B e. CC )
5 simp3
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> C e. CC )
6 4 5 negsubd
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( B + -u C ) = ( B - C ) )
7 6 oveq2d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + -u C ) ) = ( A ^c ( B - C ) ) )
8 simp1l
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> A e. CC )
9 simp1r
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> A =/= 0 )
10 cxpneg
 |-  ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c -u C ) = ( 1 / ( A ^c C ) ) )
11 8 9 5 10 syl3anc
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c -u C ) = ( 1 / ( A ^c C ) ) )
12 11 oveq2d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( A ^c B ) x. ( A ^c -u C ) ) = ( ( A ^c B ) x. ( 1 / ( A ^c C ) ) ) )
13 cxpcl
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )
14 8 4 13 syl2anc
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c B ) e. CC )
15 cxpcl
 |-  ( ( A e. CC /\ C e. CC ) -> ( A ^c C ) e. CC )
16 8 5 15 syl2anc
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c C ) e. CC )
17 cxpne0
 |-  ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c C ) =/= 0 )
18 8 9 5 17 syl3anc
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c C ) =/= 0 )
19 14 16 18 divrecd
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( A ^c B ) / ( A ^c C ) ) = ( ( A ^c B ) x. ( 1 / ( A ^c C ) ) ) )
20 12 19 eqtr4d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( A ^c B ) x. ( A ^c -u C ) ) = ( ( A ^c B ) / ( A ^c C ) ) )
21 3 7 20 3eqtr3d
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B - C ) ) = ( ( A ^c B ) / ( A ^c C ) ) )