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

Metamath Proof Explorer

Theorem expmulz

Description: Product of exponents law for integer exponentiation. Proposition 10-4.2(b) of Gleason p. 135. (Contributed by Mario Carneiro, 7-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 elznn0nn 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
2 elznn0nn 
 |-  ( M e. ZZ <-> ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) )
3 expmul 
 |-  ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
4 3 3expia 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( N e. NN0 -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
5 4 adantlr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 ) -> ( N e. NN0 -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
6 simp2l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> M e. RR )
7 6 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> M e. CC )
8 simp3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> N e. NN0 )
9 8 nn0cnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> N e. CC )
10 7 9 mulneg1d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( -u M x. N ) = -u ( M x. N ) )
11 10 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( -u M x. N ) ) = ( A ^ -u ( M x. N ) ) )
12 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> A e. CC )
13 simp2r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u M e. NN )
14 13 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u M e. NN0 )
15 expmul 
 |-  ( ( A e. CC /\ -u M e. NN0 /\ N e. NN0 ) -> ( A ^ ( -u M x. N ) ) = ( ( A ^ -u M ) ^ N ) )
16 12 14 8 15 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( -u M x. N ) ) = ( ( A ^ -u M ) ^ N ) )
17 11 16 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ -u ( M x. N ) ) = ( ( A ^ -u M ) ^ N ) )
18 17 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( 1 / ( A ^ -u ( M x. N ) ) ) = ( 1 / ( ( A ^ -u M ) ^ N ) ) )
19 expcl 
 |-  ( ( A e. CC /\ -u M e. NN0 ) -> ( A ^ -u M ) e. CC )
20 12 14 19 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ -u M ) e. CC )
21 simp1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> A =/= 0 )
22 13 nnzd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u M e. ZZ )
23 expne0i 
 |-  ( ( A e. CC /\ A =/= 0 /\ -u M e. ZZ ) -> ( A ^ -u M ) =/= 0 )
24 12 21 22 23 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ -u M ) =/= 0 )
25 8 nn0zd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> N e. ZZ )
26 exprec 
 |-  ( ( ( A ^ -u M ) e. CC /\ ( A ^ -u M ) =/= 0 /\ N e. ZZ ) -> ( ( 1 / ( A ^ -u M ) ) ^ N ) = ( 1 / ( ( A ^ -u M ) ^ N ) ) )
27 20 24 25 26 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( 1 / ( A ^ -u M ) ) ^ N ) = ( 1 / ( ( A ^ -u M ) ^ N ) ) )
28 18 27 eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( 1 / ( A ^ -u ( M x. N ) ) ) = ( ( 1 / ( A ^ -u M ) ) ^ N ) )
29 7 9 mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( M x. N ) e. CC )
30 14 8 nn0mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( -u M x. N ) e. NN0 )
31 10 30 eqeltrrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> -u ( M x. N ) e. NN0 )
32 expneg2 
 |-  ( ( A e. CC /\ ( M x. N ) e. CC /\ -u ( M x. N ) e. NN0 ) -> ( A ^ ( M x. N ) ) = ( 1 / ( A ^ -u ( M x. N ) ) ) )
33 12 29 31 32 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M x. N ) ) = ( 1 / ( A ^ -u ( M x. N ) ) ) )
34 expneg2 
 |-  ( ( A e. CC /\ M e. CC /\ -u M e. NN0 ) -> ( A ^ M ) = ( 1 / ( A ^ -u M ) ) )
35 12 7 14 34 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ M ) = ( 1 / ( A ^ -u M ) ) )
36 35 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( ( A ^ M ) ^ N ) = ( ( 1 / ( A ^ -u M ) ) ^ N ) )
37 28 33 36 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ N e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
38 37 3expia 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) ) -> ( N e. NN0 -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
39 5 38 jaodan 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) ) -> ( N e. NN0 -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
40 simp2 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> M e. NN0 )
41 40 nn0cnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> M e. CC )
42 simp3l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> N e. RR )
43 42 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC )
44 41 43 mulneg2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( M x. -u N ) = -u ( M x. N ) )
45 44 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M x. -u N ) ) = ( A ^ -u ( M x. N ) ) )
46 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> A e. CC )
47 simp3r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN )
48 47 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN0 )
49 expmul 
 |-  ( ( A e. CC /\ M e. NN0 /\ -u N e. NN0 ) -> ( A ^ ( M x. -u N ) ) = ( ( A ^ M ) ^ -u N ) )
50 46 40 48 49 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M x. -u N ) ) = ( ( A ^ M ) ^ -u N ) )
51 45 50 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u ( M x. N ) ) = ( ( A ^ M ) ^ -u N ) )
52 51 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( A ^ -u ( M x. N ) ) ) = ( 1 / ( ( A ^ M ) ^ -u N ) ) )
53 41 43 mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( M x. N ) e. CC )
54 40 48 nn0mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( M x. -u N ) e. NN0 )
55 44 54 eqeltrrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> -u ( M x. N ) e. NN0 )
56 46 53 55 32 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M x. N ) ) = ( 1 / ( A ^ -u ( M x. N ) ) ) )
57 expcl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ M ) e. CC )
58 46 40 57 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ M ) e. CC )
59 expneg2 
 |-  ( ( ( A ^ M ) e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( ( A ^ M ) ^ N ) = ( 1 / ( ( A ^ M ) ^ -u N ) ) )
60 58 43 48 59 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ M ) ^ N ) = ( 1 / ( ( A ^ M ) ^ -u N ) ) )
61 52 56 60 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
62 61 3expia 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. NN0 ) -> ( ( N e. RR /\ -u N e. NN ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
63 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> A e. CC )
64 simp2l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> M e. RR )
65 64 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> M e. CC )
66 simp2r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u M e. NN )
67 66 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u M e. NN0 )
68 63 65 67 34 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ M ) = ( 1 / ( A ^ -u M ) ) )
69 68 oveq1d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ M ) ^ N ) = ( ( 1 / ( A ^ -u M ) ) ^ N ) )
70 63 67 19 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u M ) e. CC )
71 simp1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> A =/= 0 )
72 66 nnzd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u M e. ZZ )
73 63 71 72 23 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ -u M ) =/= 0 )
74 70 73 reccld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( A ^ -u M ) ) e. CC )
75 simp3l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. RR )
76 75 recnd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> N e. CC )
77 simp3r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN )
78 77 nnnn0d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. NN0 )
79 expneg2 
 |-  ( ( ( 1 / ( A ^ -u M ) ) e. CC /\ N e. CC /\ -u N e. NN0 ) -> ( ( 1 / ( A ^ -u M ) ) ^ N ) = ( 1 / ( ( 1 / ( A ^ -u M ) ) ^ -u N ) ) )
80 74 76 78 79 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( 1 / ( A ^ -u M ) ) ^ N ) = ( 1 / ( ( 1 / ( A ^ -u M ) ) ^ -u N ) ) )
81 77 nnzd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> -u N e. ZZ )
82 exprec 
 |-  ( ( ( A ^ -u M ) e. CC /\ ( A ^ -u M ) =/= 0 /\ -u N e. ZZ ) -> ( ( 1 / ( A ^ -u M ) ) ^ -u N ) = ( 1 / ( ( A ^ -u M ) ^ -u N ) ) )
83 70 73 81 82 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( 1 / ( A ^ -u M ) ) ^ -u N ) = ( 1 / ( ( A ^ -u M ) ^ -u N ) ) )
84 83 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( ( 1 / ( A ^ -u M ) ) ^ -u N ) ) = ( 1 / ( 1 / ( ( A ^ -u M ) ^ -u N ) ) ) )
85 expcl 
 |-  ( ( ( A ^ -u M ) e. CC /\ -u N e. NN0 ) -> ( ( A ^ -u M ) ^ -u N ) e. CC )
86 70 78 85 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ -u M ) ^ -u N ) e. CC )
87 expne0i 
 |-  ( ( ( A ^ -u M ) e. CC /\ ( A ^ -u M ) =/= 0 /\ -u N e. ZZ ) -> ( ( A ^ -u M ) ^ -u N ) =/= 0 )
88 70 73 81 87 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ -u M ) ^ -u N ) =/= 0 )
89 86 88 recrecd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( 1 / ( ( A ^ -u M ) ^ -u N ) ) ) = ( ( A ^ -u M ) ^ -u N ) )
90 expmul 
 |-  ( ( A e. CC /\ -u M e. NN0 /\ -u N e. NN0 ) -> ( A ^ ( -u M x. -u N ) ) = ( ( A ^ -u M ) ^ -u N ) )
91 63 67 78 90 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( -u M x. -u N ) ) = ( ( A ^ -u M ) ^ -u N ) )
92 65 76 mul2negd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( -u M x. -u N ) = ( M x. N ) )
93 92 oveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( -u M x. -u N ) ) = ( A ^ ( M x. N ) ) )
94 91 93 eqtr3d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( ( A ^ -u M ) ^ -u N ) = ( A ^ ( M x. N ) ) )
95 84 89 94 3eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( 1 / ( ( 1 / ( A ^ -u M ) ) ^ -u N ) ) = ( A ^ ( M x. N ) ) )
96 69 80 95 3eqtrrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )
97 96 3expia 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. RR /\ -u M e. NN ) ) -> ( ( N e. RR /\ -u N e. NN ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
98 62 97 jaodan 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) ) -> ( ( N e. RR /\ -u N e. NN ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
99 39 98 jaod 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. NN0 \/ ( M e. RR /\ -u M e. NN ) ) ) -> ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
100 2 99 sylan2b 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. ZZ ) -> ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
101 1 100 biimtrid 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ M e. ZZ ) -> ( N e. ZZ -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
102 101 impr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )