Metamath Proof Explorer

Theorem expmul

Description: Product of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(b) of Gleason p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 4-Jan-2006)

Ref Expression
Assertion expmul 
|- ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 0 -> ( M x. j ) = ( M x. 0 ) )
2 1 oveq2d 
 |-  ( j = 0 -> ( A ^ ( M x. j ) ) = ( A ^ ( M x. 0 ) ) )
3 oveq2 
 |-  ( j = 0 -> ( ( A ^ M ) ^ j ) = ( ( A ^ M ) ^ 0 ) )
4 2 3 eqeq12d 
 |-  ( j = 0 -> ( ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) <-> ( A ^ ( M x. 0 ) ) = ( ( A ^ M ) ^ 0 ) ) )
5 4 imbi2d 
 |-  ( j = 0 -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. 0 ) ) = ( ( A ^ M ) ^ 0 ) ) ) )
6 oveq2 
 |-  ( j = k -> ( M x. j ) = ( M x. k ) )
7 6 oveq2d 
 |-  ( j = k -> ( A ^ ( M x. j ) ) = ( A ^ ( M x. k ) ) )
8 oveq2 
 |-  ( j = k -> ( ( A ^ M ) ^ j ) = ( ( A ^ M ) ^ k ) )
9 7 8 eqeq12d 
 |-  ( j = k -> ( ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) <-> ( A ^ ( M x. k ) ) = ( ( A ^ M ) ^ k ) ) )
10 9 imbi2d 
 |-  ( j = k -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. k ) ) = ( ( A ^ M ) ^ k ) ) ) )
11 oveq2 
 |-  ( j = ( k + 1 ) -> ( M x. j ) = ( M x. ( k + 1 ) ) )
12 11 oveq2d 
 |-  ( j = ( k + 1 ) -> ( A ^ ( M x. j ) ) = ( A ^ ( M x. ( k + 1 ) ) ) )
13 oveq2 
 |-  ( j = ( k + 1 ) -> ( ( A ^ M ) ^ j ) = ( ( A ^ M ) ^ ( k + 1 ) ) )
14 12 13 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) <-> ( A ^ ( M x. ( k + 1 ) ) ) = ( ( A ^ M ) ^ ( k + 1 ) ) ) )
15 14 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. ( k + 1 ) ) ) = ( ( A ^ M ) ^ ( k + 1 ) ) ) ) )
16 oveq2 
 |-  ( j = N -> ( M x. j ) = ( M x. N ) )
17 16 oveq2d 
 |-  ( j = N -> ( A ^ ( M x. j ) ) = ( A ^ ( M x. N ) ) )
18 oveq2 
 |-  ( j = N -> ( ( A ^ M ) ^ j ) = ( ( A ^ M ) ^ N ) )
19 17 18 eqeq12d 
 |-  ( j = N -> ( ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) <-> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
20 19 imbi2d 
 |-  ( j = N -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. j ) ) = ( ( A ^ M ) ^ j ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) ) )
21 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
22 21 mul01d 
 |-  ( M e. NN0 -> ( M x. 0 ) = 0 )
23 22 oveq2d 
 |-  ( M e. NN0 -> ( A ^ ( M x. 0 ) ) = ( A ^ 0 ) )
24 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
25 23 24 sylan9eqr 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. 0 ) ) = 1 )
26 expcl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ M ) e. CC )
27 exp0 
 |-  ( ( A ^ M ) e. CC -> ( ( A ^ M ) ^ 0 ) = 1 )
28 26 27 syl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( ( A ^ M ) ^ 0 ) = 1 )
29 25 28 eqtr4d 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. 0 ) ) = ( ( A ^ M ) ^ 0 ) )
30 oveq1 
 |-  ( ( A ^ ( M x. k ) ) = ( ( A ^ M ) ^ k ) -> ( ( A ^ ( M x. k ) ) x. ( A ^ M ) ) = ( ( ( A ^ M ) ^ k ) x. ( A ^ M ) ) )
31 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
32 ax-1cn 
 |-  1 e. CC
33 adddi 
 |-  ( ( M e. CC /\ k e. CC /\ 1 e. CC ) -> ( M x. ( k + 1 ) ) = ( ( M x. k ) + ( M x. 1 ) ) )
34 32 33 mp3an3 
 |-  ( ( M e. CC /\ k e. CC ) -> ( M x. ( k + 1 ) ) = ( ( M x. k ) + ( M x. 1 ) ) )
35 mulid1 
 |-  ( M e. CC -> ( M x. 1 ) = M )
36 35 adantr 
 |-  ( ( M e. CC /\ k e. CC ) -> ( M x. 1 ) = M )
37 36 oveq2d 
 |-  ( ( M e. CC /\ k e. CC ) -> ( ( M x. k ) + ( M x. 1 ) ) = ( ( M x. k ) + M ) )
38 34 37 eqtrd 
 |-  ( ( M e. CC /\ k e. CC ) -> ( M x. ( k + 1 ) ) = ( ( M x. k ) + M ) )
39 21 31 38 syl2an 
 |-  ( ( M e. NN0 /\ k e. NN0 ) -> ( M x. ( k + 1 ) ) = ( ( M x. k ) + M ) )
40 39 adantll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( M x. ( k + 1 ) ) = ( ( M x. k ) + M ) )
41 40 oveq2d 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ ( M x. ( k + 1 ) ) ) = ( A ^ ( ( M x. k ) + M ) ) )
42 simpll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> A e. CC )
43 nn0mulcl 
 |-  ( ( M e. NN0 /\ k e. NN0 ) -> ( M x. k ) e. NN0 )
44 43 adantll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( M x. k ) e. NN0 )
45 simplr 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> M e. NN0 )
46 expadd 
 |-  ( ( A e. CC /\ ( M x. k ) e. NN0 /\ M e. NN0 ) -> ( A ^ ( ( M x. k ) + M ) ) = ( ( A ^ ( M x. k ) ) x. ( A ^ M ) ) )
47 42 44 45 46 syl3anc 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ ( ( M x. k ) + M ) ) = ( ( A ^ ( M x. k ) ) x. ( A ^ M ) ) )
48 41 47 eqtrd 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ ( M x. ( k + 1 ) ) ) = ( ( A ^ ( M x. k ) ) x. ( A ^ M ) ) )
49 expp1 
 |-  ( ( ( A ^ M ) e. CC /\ k e. NN0 ) -> ( ( A ^ M ) ^ ( k + 1 ) ) = ( ( ( A ^ M ) ^ k ) x. ( A ^ M ) ) )
50 26 49 sylan 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ M ) ^ ( k + 1 ) ) = ( ( ( A ^ M ) ^ k ) x. ( A ^ M ) ) )
51 48 50 eqeq12d 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ ( M x. ( k + 1 ) ) ) = ( ( A ^ M ) ^ ( k + 1 ) ) <-> ( ( A ^ ( M x. k ) ) x. ( A ^ M ) ) = ( ( ( A ^ M ) ^ k ) x. ( A ^ M ) ) ) )
52 30 51 syl5ibr 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ ( M x. k ) ) = ( ( A ^ M ) ^ k ) -> ( A ^ ( M x. ( k + 1 ) ) ) = ( ( A ^ M ) ^ ( k + 1 ) ) ) )
53 52 expcom 
 |-  ( k e. NN0 -> ( ( A e. CC /\ M e. NN0 ) -> ( ( A ^ ( M x. k ) ) = ( ( A ^ M ) ^ k ) -> ( A ^ ( M x. ( k + 1 ) ) ) = ( ( A ^ M ) ^ ( k + 1 ) ) ) ) )
54 53 a2d 
 |-  ( k e. NN0 -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. k ) ) = ( ( A ^ M ) ^ k ) ) -> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. ( k + 1 ) ) ) = ( ( A ^ M ) ^ ( k + 1 ) ) ) ) )
55 5 10 15 20 29 54 nn0ind 
 |-  ( N e. NN0 -> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) )
56 55 expdcom 
 |-  ( A e. CC -> ( M e. NN0 -> ( N e. NN0 -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) ) ) )
57 56 3imp 
 |-  ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M x. N ) ) = ( ( A ^ M ) ^ N ) )