Metamath Proof Explorer


Theorem mulexp

Description: Nonnegative integer exponentiation of a product. Proposition 10-4.2(c) of Gleason p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005)

Ref Expression
Assertion mulexp A B N 0 A B N = A N B N

Proof

Step Hyp Ref Expression
1 oveq2 j = 0 A B j = A B 0
2 oveq2 j = 0 A j = A 0
3 oveq2 j = 0 B j = B 0
4 2 3 oveq12d j = 0 A j B j = A 0 B 0
5 1 4 eqeq12d j = 0 A B j = A j B j A B 0 = A 0 B 0
6 5 imbi2d j = 0 A B A B j = A j B j A B A B 0 = A 0 B 0
7 oveq2 j = k A B j = A B k
8 oveq2 j = k A j = A k
9 oveq2 j = k B j = B k
10 8 9 oveq12d j = k A j B j = A k B k
11 7 10 eqeq12d j = k A B j = A j B j A B k = A k B k
12 11 imbi2d j = k A B A B j = A j B j A B A B k = A k B k
13 oveq2 j = k + 1 A B j = A B k + 1
14 oveq2 j = k + 1 A j = A k + 1
15 oveq2 j = k + 1 B j = B k + 1
16 14 15 oveq12d j = k + 1 A j B j = A k + 1 B k + 1
17 13 16 eqeq12d j = k + 1 A B j = A j B j A B k + 1 = A k + 1 B k + 1
18 17 imbi2d j = k + 1 A B A B j = A j B j A B A B k + 1 = A k + 1 B k + 1
19 oveq2 j = N A B j = A B N
20 oveq2 j = N A j = A N
21 oveq2 j = N B j = B N
22 20 21 oveq12d j = N A j B j = A N B N
23 19 22 eqeq12d j = N A B j = A j B j A B N = A N B N
24 23 imbi2d j = N A B A B j = A j B j A B A B N = A N B N
25 mulcl A B A B
26 exp0 A B A B 0 = 1
27 25 26 syl A B A B 0 = 1
28 exp0 A A 0 = 1
29 exp0 B B 0 = 1
30 28 29 oveqan12d A B A 0 B 0 = 1 1
31 1t1e1 1 1 = 1
32 30 31 eqtrdi A B A 0 B 0 = 1
33 27 32 eqtr4d A B A B 0 = A 0 B 0
34 expp1 A B k 0 A B k + 1 = A B k A B
35 25 34 sylan A B k 0 A B k + 1 = A B k A B
36 35 adantr A B k 0 A B k = A k B k A B k + 1 = A B k A B
37 oveq1 A B k = A k B k A B k A B = A k B k A B
38 expcl A k 0 A k
39 expcl B k 0 B k
40 38 39 anim12i A k 0 B k 0 A k B k
41 40 anandirs A B k 0 A k B k
42 simpl A B k 0 A B
43 mul4 A k B k A B A k B k A B = A k A B k B
44 41 42 43 syl2anc A B k 0 A k B k A B = A k A B k B
45 expp1 A k 0 A k + 1 = A k A
46 45 adantlr A B k 0 A k + 1 = A k A
47 expp1 B k 0 B k + 1 = B k B
48 47 adantll A B k 0 B k + 1 = B k B
49 46 48 oveq12d A B k 0 A k + 1 B k + 1 = A k A B k B
50 44 49 eqtr4d A B k 0 A k B k A B = A k + 1 B k + 1
51 37 50 sylan9eqr A B k 0 A B k = A k B k A B k A B = A k + 1 B k + 1
52 36 51 eqtrd A B k 0 A B k = A k B k A B k + 1 = A k + 1 B k + 1
53 52 exp31 A B k 0 A B k = A k B k A B k + 1 = A k + 1 B k + 1
54 53 com12 k 0 A B A B k = A k B k A B k + 1 = A k + 1 B k + 1
55 54 a2d k 0 A B A B k = A k B k A B A B k + 1 = A k + 1 B k + 1
56 6 12 18 24 33 55 nn0ind N 0 A B A B N = A N B N
57 56 expdcom A B N 0 A B N = A N B N
58 57 3imp A B N 0 A B N = A N B N