Metamath Proof Explorer

Theorem expadd

Description: Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by NM, 30-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( j = 0 -> ( M + j ) = ( M + 0 ) )
2 1 oveq2d 
 |-  ( j = 0 -> ( A ^ ( M + j ) ) = ( A ^ ( M + 0 ) ) )
3 oveq2 
 |-  ( j = 0 -> ( A ^ j ) = ( A ^ 0 ) )
4 3 oveq2d 
 |-  ( j = 0 -> ( ( A ^ M ) x. ( A ^ j ) ) = ( ( A ^ M ) x. ( A ^ 0 ) ) )
5 2 4 eqeq12d 
 |-  ( j = 0 -> ( ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) <-> ( A ^ ( M + 0 ) ) = ( ( A ^ M ) x. ( A ^ 0 ) ) ) )
6 5 imbi2d 
 |-  ( j = 0 -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + 0 ) ) = ( ( A ^ M ) x. ( A ^ 0 ) ) ) ) )
7 oveq2 
 |-  ( j = k -> ( M + j ) = ( M + k ) )
8 7 oveq2d 
 |-  ( j = k -> ( A ^ ( M + j ) ) = ( A ^ ( M + k ) ) )
9 oveq2 
 |-  ( j = k -> ( A ^ j ) = ( A ^ k ) )
10 9 oveq2d 
 |-  ( j = k -> ( ( A ^ M ) x. ( A ^ j ) ) = ( ( A ^ M ) x. ( A ^ k ) ) )
11 8 10 eqeq12d 
 |-  ( j = k -> ( ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) <-> ( A ^ ( M + k ) ) = ( ( A ^ M ) x. ( A ^ k ) ) ) )
12 11 imbi2d 
 |-  ( j = k -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + k ) ) = ( ( A ^ M ) x. ( A ^ k ) ) ) ) )
13 oveq2 
 |-  ( j = ( k + 1 ) -> ( M + j ) = ( M + ( k + 1 ) ) )
14 13 oveq2d 
 |-  ( j = ( k + 1 ) -> ( A ^ ( M + j ) ) = ( A ^ ( M + ( k + 1 ) ) ) )
15 oveq2 
 |-  ( j = ( k + 1 ) -> ( A ^ j ) = ( A ^ ( k + 1 ) ) )
16 15 oveq2d 
 |-  ( j = ( k + 1 ) -> ( ( A ^ M ) x. ( A ^ j ) ) = ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) )
17 14 16 eqeq12d 
 |-  ( j = ( k + 1 ) -> ( ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) <-> ( A ^ ( M + ( k + 1 ) ) ) = ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) ) )
18 17 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + ( k + 1 ) ) ) = ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) ) ) )
19 oveq2 
 |-  ( j = N -> ( M + j ) = ( M + N ) )
20 19 oveq2d 
 |-  ( j = N -> ( A ^ ( M + j ) ) = ( A ^ ( M + N ) ) )
21 oveq2 
 |-  ( j = N -> ( A ^ j ) = ( A ^ N ) )
22 21 oveq2d 
 |-  ( j = N -> ( ( A ^ M ) x. ( A ^ j ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )
23 20 22 eqeq12d 
 |-  ( j = N -> ( ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) <-> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
24 23 imbi2d 
 |-  ( j = N -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + j ) ) = ( ( A ^ M ) x. ( A ^ j ) ) ) <-> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) ) )
25 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
26 25 addridd 
 |-  ( M e. NN0 -> ( M + 0 ) = M )
27 26 adantl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( M + 0 ) = M )
28 27 oveq2d 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + 0 ) ) = ( A ^ M ) )
29 expcl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ M ) e. CC )
30 29 mulridd 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( ( A ^ M ) x. 1 ) = ( A ^ M ) )
31 28 30 eqtr4d 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + 0 ) ) = ( ( A ^ M ) x. 1 ) )
32 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
33 32 adantr 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ 0 ) = 1 )
34 33 oveq2d 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( ( A ^ M ) x. ( A ^ 0 ) ) = ( ( A ^ M ) x. 1 ) )
35 31 34 eqtr4d 
 |-  ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + 0 ) ) = ( ( A ^ M ) x. ( A ^ 0 ) ) )
36 oveq1 
 |-  ( ( A ^ ( M + k ) ) = ( ( A ^ M ) x. ( A ^ k ) ) -> ( ( A ^ ( M + k ) ) x. A ) = ( ( ( A ^ M ) x. ( A ^ k ) ) x. A ) )
37 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
38 ax-1cn 
 |-  1 e. CC
39 addass 
 |-  ( ( M e. CC /\ k e. CC /\ 1 e. CC ) -> ( ( M + k ) + 1 ) = ( M + ( k + 1 ) ) )
40 38 39 mp3an3 
 |-  ( ( M e. CC /\ k e. CC ) -> ( ( M + k ) + 1 ) = ( M + ( k + 1 ) ) )
41 25 37 40 syl2an 
 |-  ( ( M e. NN0 /\ k e. NN0 ) -> ( ( M + k ) + 1 ) = ( M + ( k + 1 ) ) )
42 41 adantll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( M + k ) + 1 ) = ( M + ( k + 1 ) ) )
43 42 oveq2d 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ ( ( M + k ) + 1 ) ) = ( A ^ ( M + ( k + 1 ) ) ) )
44 simpll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> A e. CC )
45 nn0addcl 
 |-  ( ( M e. NN0 /\ k e. NN0 ) -> ( M + k ) e. NN0 )
46 45 adantll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( M + k ) e. NN0 )
47 expp1 
 |-  ( ( A e. CC /\ ( M + k ) e. NN0 ) -> ( A ^ ( ( M + k ) + 1 ) ) = ( ( A ^ ( M + k ) ) x. A ) )
48 44 46 47 syl2anc 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ ( ( M + k ) + 1 ) ) = ( ( A ^ ( M + k ) ) x. A ) )
49 43 48 eqtr3d 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ ( M + ( k + 1 ) ) ) = ( ( A ^ ( M + k ) ) x. A ) )
50 expp1 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
51 50 adantlr 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ ( k + 1 ) ) = ( ( A ^ k ) x. A ) )
52 51 oveq2d 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) = ( ( A ^ M ) x. ( ( A ^ k ) x. A ) ) )
53 29 adantr 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ M ) e. CC )
54 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
55 54 adantlr 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( A ^ k ) e. CC )
56 53 55 44 mulassd 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( ( A ^ M ) x. ( A ^ k ) ) x. A ) = ( ( A ^ M ) x. ( ( A ^ k ) x. A ) ) )
57 52 56 eqtr4d 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) = ( ( ( A ^ M ) x. ( A ^ k ) ) x. A ) )
58 49 57 eqeq12d 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ ( M + ( k + 1 ) ) ) = ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) <-> ( ( A ^ ( M + k ) ) x. A ) = ( ( ( A ^ M ) x. ( A ^ k ) ) x. A ) ) )
59 36 58 imbitrrid 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. NN0 ) -> ( ( A ^ ( M + k ) ) = ( ( A ^ M ) x. ( A ^ k ) ) -> ( A ^ ( M + ( k + 1 ) ) ) = ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) ) )
60 59 expcom 
 |-  ( k e. NN0 -> ( ( A e. CC /\ M e. NN0 ) -> ( ( A ^ ( M + k ) ) = ( ( A ^ M ) x. ( A ^ k ) ) -> ( A ^ ( M + ( k + 1 ) ) ) = ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) ) ) )
61 60 a2d 
 |-  ( k e. NN0 -> ( ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + k ) ) = ( ( A ^ M ) x. ( A ^ k ) ) ) -> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + ( k + 1 ) ) ) = ( ( A ^ M ) x. ( A ^ ( k + 1 ) ) ) ) ) )
62 6 12 18 24 35 61 nn0ind 
 |-  ( N e. NN0 -> ( ( A e. CC /\ M e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) )
63 62 expdcom 
 |-  ( A e. CC -> ( M e. NN0 -> ( N e. NN0 -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) ) ) )
64 63 3imp 
 |-  ( ( A e. CC /\ M e. NN0 /\ N e. NN0 ) -> ( A ^ ( M + N ) ) = ( ( A ^ M ) x. ( A ^ N ) ) )