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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 | |
|
2 | 1 | oveq2d | |
3 | oveq2 | |
|
4 | 2 3 | eqeq12d | |
5 | 4 | imbi2d | |
6 | oveq2 | |
|
7 | 6 | oveq2d | |
8 | oveq2 | |
|
9 | 7 8 | eqeq12d | |
10 | 9 | imbi2d | |
11 | oveq2 | |
|
12 | 11 | oveq2d | |
13 | oveq2 | |
|
14 | 12 13 | eqeq12d | |
15 | 14 | imbi2d | |
16 | oveq2 | |
|
17 | 16 | oveq2d | |
18 | oveq2 | |
|
19 | 17 18 | eqeq12d | |
20 | 19 | imbi2d | |
21 | nn0cn | |
|
22 | 21 | mul01d | |
23 | 22 | oveq2d | |
24 | exp0 | |
|
25 | 23 24 | sylan9eqr | |
26 | expcl | |
|
27 | exp0 | |
|
28 | 26 27 | syl | |
29 | 25 28 | eqtr4d | |
30 | oveq1 | |
|
31 | nn0cn | |
|
32 | ax-1cn | |
|
33 | adddi | |
|
34 | 32 33 | mp3an3 | |
35 | mulrid | |
|
36 | 35 | adantr | |
37 | 36 | oveq2d | |
38 | 34 37 | eqtrd | |
39 | 21 31 38 | syl2an | |
40 | 39 | adantll | |
41 | 40 | oveq2d | |
42 | simpll | |
|
43 | nn0mulcl | |
|
44 | 43 | adantll | |
45 | simplr | |
|
46 | expadd | |
|
47 | 42 44 45 46 | syl3anc | |
48 | 41 47 | eqtrd | |
49 | expp1 | |
|
50 | 26 49 | sylan | |
51 | 48 50 | eqeq12d | |
52 | 30 51 | imbitrrid | |
53 | 52 | expcom | |
54 | 53 | a2d | |
55 | 5 10 15 20 29 54 | nn0ind | |
56 | 55 | expdcom | |
57 | 56 | 3imp | |