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

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