Metamath Proof Explorer

Theorem mulexpz

Description: Integer exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135. (Contributed by Mario Carneiro, 4-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
2 simpl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A e. CC )
3 simpl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> B e. CC )
4 2 3 anim12i 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A e. CC /\ B e. CC ) )
5 mulexp 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
6 5 3expa 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
7 4 6 sylan 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
8 simplll 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> A e. CC )
9 simplrl 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> B e. CC )
10 8 9 mulcld 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A x. B ) e. CC )
11 recn 
 |-  ( N e. RR -> N e. CC )
12 11 ad2antrl 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC )
13 nnnn0 
 |-  ( -u N e. NN -> -u N e. NN0 )
14 13 ad2antll 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN0 )
15 expneg2 
 |-  ( ( ( A x. B ) e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( ( A x. B ) ^ N ) = ( 1 / ( ( A x. B ) ^ -u N ) ) )
16 10 12 14 15 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A x. B ) ^ N ) = ( 1 / ( ( A x. B ) ^ -u N ) ) )
17 expneg2 
 |-  ( ( A e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
18 8 12 14 17 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ N ) = ( 1 / ( A ^ -u N ) ) )
19 expneg2 
 |-  ( ( B e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( B ^ N ) = ( 1 / ( B ^ -u N ) ) )
20 9 12 14 19 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( B ^ N ) = ( 1 / ( B ^ -u N ) ) )
21 18 20 oveq12d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ N ) x. ( B ^ N ) ) = ( ( 1 / ( A ^ -u N ) ) x. ( 1 / ( B ^ -u N ) ) ) )
22 mulexp 
 |-  ( ( A e. CC /\ B e. CC /\ -u N e. NN0 ) -> ( ( A x. B ) ^ -u N ) = ( ( A ^ -u N ) x. ( B ^ -u N ) ) )
23 8 9 14 22 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A x. B ) ^ -u N ) = ( ( A ^ -u N ) x. ( B ^ -u N ) ) )
24 23 oveq2d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( ( A x. B ) ^ -u N ) ) = ( 1 / ( ( A ^ -u N ) x. ( B ^ -u N ) ) ) )
25 1t1e1 
 |-  ( 1 x. 1 ) = 1
26 25 oveq1i 
 |-  ( ( 1 x. 1 ) / ( ( A ^ -u N ) x. ( B ^ -u N ) ) ) = ( 1 / ( ( A ^ -u N ) x. ( B ^ -u N ) ) )
27 24 26 eqtr4di 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( ( A x. B ) ^ -u N ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u N ) x. ( B ^ -u N ) ) ) )
28 expcl 
 |-  ( ( A e. CC /\ -u N e. NN0 ) -> ( A ^ -u N ) e. CC )
29 8 14 28 syl2anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u N ) e. CC )
30 simpllr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> A =/= 0 )
31 nnz 
 |-  ( -u N e. NN -> -u N e. ZZ )
32 31 ad2antll 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. ZZ )
33 expne0i 
 |-  ( ( A e. CC /\ A =/= 0 /\ -u N e. ZZ ) -> ( A ^ -u N ) =/= 0 )
34 8 30 32 33 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u N ) =/= 0 )
35 expcl 
 |-  ( ( B e. CC /\ -u N e. NN0 ) -> ( B ^ -u N ) e. CC )
36 9 14 35 syl2anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( B ^ -u N ) e. CC )
37 simplrr 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> B =/= 0 )
38 expne0i 
 |-  ( ( B e. CC /\ B =/= 0 /\ -u N e. ZZ ) -> ( B ^ -u N ) =/= 0 )
39 9 37 32 38 syl3anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( B ^ -u N ) =/= 0 )
40 ax-1cn 
 |-  1 e. CC
41 divmuldiv 
 |-  ( ( ( 1 e. CC /\ 1 e. CC ) /\ ( ( ( A ^ -u N ) e. CC /\ ( A ^ -u N ) =/= 0 ) /\ ( ( B ^ -u N ) e. CC /\ ( B ^ -u N ) =/= 0 ) ) ) -> ( ( 1 / ( A ^ -u N ) ) x. ( 1 / ( B ^ -u N ) ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u N ) x. ( B ^ -u N ) ) ) )
42 40 40 41 mpanl12 
 |-  ( ( ( ( A ^ -u N ) e. CC /\ ( A ^ -u N ) =/= 0 ) /\ ( ( B ^ -u N ) e. CC /\ ( B ^ -u N ) =/= 0 ) ) -> ( ( 1 / ( A ^ -u N ) ) x. ( 1 / ( B ^ -u N ) ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u N ) x. ( B ^ -u N ) ) ) )
43 29 34 36 39 42 syl22anc 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( 1 / ( A ^ -u N ) ) x. ( 1 / ( B ^ -u N ) ) ) = ( ( 1 x. 1 ) / ( ( A ^ -u N ) x. ( B ^ -u N ) ) ) )
44 27 43 eqtr4d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( ( A x. B ) ^ -u N ) ) = ( ( 1 / ( A ^ -u N ) ) x. ( 1 / ( B ^ -u N ) ) ) )
45 21 44 eqtr4d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ N ) x. ( B ^ N ) ) = ( 1 / ( ( A x. B ) ^ -u N ) ) )
46 16 45 eqtr4d 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
47 7 46 jaodan 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
48 1 47 sylan2b 
 |-  ( ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) /\ N e. ZZ ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )
49 48 3impa 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) /\ N e. ZZ ) -> ( ( A x. B ) ^ N ) = ( ( A ^ N ) x. ( B ^ N ) ) )