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