Metamath Proof Explorer

Theorem cxpmul2z

Description: Generalize cxpmul2 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 elznn0 
 |-  ( C e. ZZ <-> ( C e. RR /\ ( C e. NN0 \/ -u C e. NN0 ) ) )
2 cxpmul2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. NN0 ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
3 2 3expia 
 |-  ( ( A e. CC /\ B e. CC ) -> ( C e. NN0 -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
4 3 ad4ant13 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ C e. RR ) -> ( C e. NN0 -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
5 simplll 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> A e. CC )
6 simplr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> B e. CC )
7 simprr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u C e. NN0 )
8 cxpmul2 
 |-  ( ( A e. CC /\ B e. CC /\ -u C e. NN0 ) -> ( A ^c ( B x. -u C ) ) = ( ( A ^c B ) ^ -u C ) )
9 5 6 7 8 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c ( B x. -u C ) ) = ( ( A ^c B ) ^ -u C ) )
10 9 oveq2d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( 1 / ( A ^c ( B x. -u C ) ) ) = ( 1 / ( ( A ^c B ) ^ -u C ) ) )
11 simprl 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> C e. RR )
12 11 recnd 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> C e. CC )
13 6 12 mulneg2d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( B x. -u C ) = -u ( B x. C ) )
14 13 negeqd 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u ( B x. -u C ) = -u -u ( B x. C ) )
15 6 12 mulcld 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( B x. C ) e. CC )
16 15 negnegd 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u -u ( B x. C ) = ( B x. C ) )
17 14 16 eqtrd 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u ( B x. -u C ) = ( B x. C ) )
18 17 oveq2d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c -u ( B x. -u C ) ) = ( A ^c ( B x. C ) ) )
19 simpllr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> A =/= 0 )
20 12 negcld 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> -u C e. CC )
21 6 20 mulcld 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( B x. -u C ) e. CC )
22 cxpneg 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( B x. -u C ) e. CC ) -> ( A ^c -u ( B x. -u C ) ) = ( 1 / ( A ^c ( B x. -u C ) ) ) )
23 5 19 21 22 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c -u ( B x. -u C ) ) = ( 1 / ( A ^c ( B x. -u C ) ) ) )
24 18 23 eqtr3d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c ( B x. C ) ) = ( 1 / ( A ^c ( B x. -u C ) ) ) )
25 cxpcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )
26 25 ad4ant13 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c B ) e. CC )
27 expneg2 
 |-  ( ( ( A ^c B ) e. CC /\ C e. CC /\ -u C e. NN0 ) -> ( ( A ^c B ) ^ C ) = ( 1 / ( ( A ^c B ) ^ -u C ) ) )
28 26 12 7 27 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( ( A ^c B ) ^ C ) = ( 1 / ( ( A ^c B ) ^ -u C ) ) )
29 10 24 28 3eqtr4d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ ( C e. RR /\ -u C e. NN0 ) ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
30 29 expr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ C e. RR ) -> ( -u C e. NN0 -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
31 4 30 jaod 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) /\ C e. RR ) -> ( ( C e. NN0 \/ -u C e. NN0 ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
32 31 expimpd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( ( C e. RR /\ ( C e. NN0 \/ -u C e. NN0 ) ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
33 1 32 syl5bi 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( C e. ZZ -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) ) )
34 33 impr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ C e. ZZ ) ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )