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 AM0N0A M N=AMN

Proof

Step Hyp Ref Expression
1 oveq2 j=0Mj= M0
2 1 oveq2d j=0AMj=A M0
3 oveq2 j=0AMj=AM0
4 2 3 eqeq12d j=0AMj=AMjA M0=AM0
5 4 imbi2d j=0AM0AMj=AMjAM0A M0=AM0
6 oveq2 j=kMj=Mk
7 6 oveq2d j=kAMj=AMk
8 oveq2 j=kAMj=AMk
9 7 8 eqeq12d j=kAMj=AMjAMk=AMk
10 9 imbi2d j=kAM0AMj=AMjAM0AMk=AMk
11 oveq2 j=k+1Mj=Mk+1
12 11 oveq2d j=k+1AMj=AMk+1
13 oveq2 j=k+1AMj=AMk+1
14 12 13 eqeq12d j=k+1AMj=AMjAMk+1=AMk+1
15 14 imbi2d j=k+1AM0AMj=AMjAM0AMk+1=AMk+1
16 oveq2 j=NMj= M N
17 16 oveq2d j=NAMj=A M N
18 oveq2 j=NAMj=AMN
19 17 18 eqeq12d j=NAMj=AMjA M N=AMN
20 19 imbi2d j=NAM0AMj=AMjAM0A M N=AMN
21 nn0cn M0M
22 21 mul01d M0 M0=0
23 22 oveq2d M0A M0=A0
24 exp0 AA0=1
25 23 24 sylan9eqr AM0A M0=1
26 expcl AM0AM
27 exp0 AMAM0=1
28 26 27 syl AM0AM0=1
29 25 28 eqtr4d AM0A M0=AM0
30 oveq1 AMk=AMkAMkAM=AMkAM
31 nn0cn k0k
32 ax-1cn 1
33 adddi Mk1Mk+1=Mk+ M1
34 32 33 mp3an3 MkMk+1=Mk+ M1
35 mulrid M M1=M
36 35 adantr Mk M1=M
37 36 oveq2d MkMk+ M1=Mk+M
38 34 37 eqtrd MkMk+1=Mk+M
39 21 31 38 syl2an M0k0Mk+1=Mk+M
40 39 adantll AM0k0Mk+1=Mk+M
41 40 oveq2d AM0k0AMk+1=AMk+M
42 simpll AM0k0A
43 nn0mulcl M0k0Mk0
44 43 adantll AM0k0Mk0
45 simplr AM0k0M0
46 expadd AMk0M0AMk+M=AMkAM
47 42 44 45 46 syl3anc AM0k0AMk+M=AMkAM
48 41 47 eqtrd AM0k0AMk+1=AMkAM
49 expp1 AMk0AMk+1=AMkAM
50 26 49 sylan AM0k0AMk+1=AMkAM
51 48 50 eqeq12d AM0k0AMk+1=AMk+1AMkAM=AMkAM
52 30 51 imbitrrid AM0k0AMk=AMkAMk+1=AMk+1
53 52 expcom k0AM0AMk=AMkAMk+1=AMk+1
54 53 a2d k0AM0AMk=AMkAM0AMk+1=AMk+1
55 5 10 15 20 29 54 nn0ind N0AM0A M N=AMN
56 55 expdcom AM0N0A M N=AMN
57 56 3imp AM0N0A M N=AMN