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 ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑗 = 0 → ( 𝑀 · 𝑗 ) = ( 𝑀 · 0 ) )
2 1 oveq2d ( 𝑗 = 0 → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 · 0 ) ) )
3 oveq2 ( 𝑗 = 0 → ( ( 𝐴𝑀 ) ↑ 𝑗 ) = ( ( 𝐴𝑀 ) ↑ 0 ) )
4 2 3 eqeq12d ( 𝑗 = 0 → ( ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ↔ ( 𝐴 ↑ ( 𝑀 · 0 ) ) = ( ( 𝐴𝑀 ) ↑ 0 ) ) )
5 4 imbi2d ( 𝑗 = 0 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 0 ) ) = ( ( 𝐴𝑀 ) ↑ 0 ) ) ) )
6 oveq2 ( 𝑗 = 𝑘 → ( 𝑀 · 𝑗 ) = ( 𝑀 · 𝑘 ) )
7 6 oveq2d ( 𝑗 = 𝑘 → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) )
8 oveq2 ( 𝑗 = 𝑘 → ( ( 𝐴𝑀 ) ↑ 𝑗 ) = ( ( 𝐴𝑀 ) ↑ 𝑘 ) )
9 7 8 eqeq12d ( 𝑗 = 𝑘 → ( ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ↔ ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑘 ) ) )
10 9 imbi2d ( 𝑗 = 𝑘 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑘 ) ) ) )
11 oveq2 ( 𝑗 = ( 𝑘 + 1 ) → ( 𝑀 · 𝑗 ) = ( 𝑀 · ( 𝑘 + 1 ) ) )
12 11 oveq2d ( 𝑗 = ( 𝑘 + 1 ) → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) )
13 oveq2 ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴𝑀 ) ↑ 𝑗 ) = ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) )
14 12 13 eqeq12d ( 𝑗 = ( 𝑘 + 1 ) → ( ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ↔ ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) ) )
15 14 imbi2d ( 𝑗 = ( 𝑘 + 1 ) → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) ) ) )
16 oveq2 ( 𝑗 = 𝑁 → ( 𝑀 · 𝑗 ) = ( 𝑀 · 𝑁 ) )
17 16 oveq2d ( 𝑗 = 𝑁 → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) )
18 oveq2 ( 𝑗 = 𝑁 → ( ( 𝐴𝑀 ) ↑ 𝑗 ) = ( ( 𝐴𝑀 ) ↑ 𝑁 ) )
19 17 18 eqeq12d ( 𝑗 = 𝑁 → ( ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ↔ ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑁 ) ) )
20 19 imbi2d ( 𝑗 = 𝑁 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑗 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑗 ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑁 ) ) ) )
21 nn0cn ( 𝑀 ∈ ℕ0𝑀 ∈ ℂ )
22 21 mul01d ( 𝑀 ∈ ℕ0 → ( 𝑀 · 0 ) = 0 )
23 22 oveq2d ( 𝑀 ∈ ℕ0 → ( 𝐴 ↑ ( 𝑀 · 0 ) ) = ( 𝐴 ↑ 0 ) )
24 exp0 ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
25 23 24 sylan9eqr ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 0 ) ) = 1 )
26 expcl ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴𝑀 ) ∈ ℂ )
27 exp0 ( ( 𝐴𝑀 ) ∈ ℂ → ( ( 𝐴𝑀 ) ↑ 0 ) = 1 )
28 26 27 syl ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴𝑀 ) ↑ 0 ) = 1 )
29 25 28 eqtr4d ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 0 ) ) = ( ( 𝐴𝑀 ) ↑ 0 ) )
30 oveq1 ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑘 ) → ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) · ( 𝐴𝑀 ) ) = ( ( ( 𝐴𝑀 ) ↑ 𝑘 ) · ( 𝐴𝑀 ) ) )
31 nn0cn ( 𝑘 ∈ ℕ0𝑘 ∈ ℂ )
32 ax-1cn 1 ∈ ℂ
33 adddi ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑀 · ( 𝑘 + 1 ) ) = ( ( 𝑀 · 𝑘 ) + ( 𝑀 · 1 ) ) )
34 32 33 mp3an3 ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑀 · ( 𝑘 + 1 ) ) = ( ( 𝑀 · 𝑘 ) + ( 𝑀 · 1 ) ) )
35 mulid1 ( 𝑀 ∈ ℂ → ( 𝑀 · 1 ) = 𝑀 )
36 35 adantr ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑀 · 1 ) = 𝑀 )
37 36 oveq2d ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( ( 𝑀 · 𝑘 ) + ( 𝑀 · 1 ) ) = ( ( 𝑀 · 𝑘 ) + 𝑀 ) )
38 34 37 eqtrd ( ( 𝑀 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 𝑀 · ( 𝑘 + 1 ) ) = ( ( 𝑀 · 𝑘 ) + 𝑀 ) )
39 21 31 38 syl2an ( ( 𝑀 ∈ ℕ0𝑘 ∈ ℕ0 ) → ( 𝑀 · ( 𝑘 + 1 ) ) = ( ( 𝑀 · 𝑘 ) + 𝑀 ) )
40 39 adantll ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 · ( 𝑘 + 1 ) ) = ( ( 𝑀 · 𝑘 ) + 𝑀 ) )
41 40 oveq2d ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( 𝐴 ↑ ( ( 𝑀 · 𝑘 ) + 𝑀 ) ) )
42 simpll ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
43 nn0mulcl ( ( 𝑀 ∈ ℕ0𝑘 ∈ ℕ0 ) → ( 𝑀 · 𝑘 ) ∈ ℕ0 )
44 43 adantll ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑀 · 𝑘 ) ∈ ℕ0 )
45 simplr ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ ℕ0 )
46 expadd ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 · 𝑘 ) ∈ ℕ0𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 · 𝑘 ) + 𝑀 ) ) = ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) · ( 𝐴𝑀 ) ) )
47 42 44 45 46 syl3anc ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( ( 𝑀 · 𝑘 ) + 𝑀 ) ) = ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) · ( 𝐴𝑀 ) ) )
48 41 47 eqtrd ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) · ( 𝐴𝑀 ) ) )
49 expp1 ( ( ( 𝐴𝑀 ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 𝐴𝑀 ) ↑ 𝑘 ) · ( 𝐴𝑀 ) ) )
50 26 49 sylan ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) = ( ( ( 𝐴𝑀 ) ↑ 𝑘 ) · ( 𝐴𝑀 ) ) )
51 48 50 eqeq12d ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) ↔ ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) · ( 𝐴𝑀 ) ) = ( ( ( 𝐴𝑀 ) ↑ 𝑘 ) · ( 𝐴𝑀 ) ) ) )
52 30 51 syl5ibr ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑘 ) → ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) ) )
53 52 expcom ( 𝑘 ∈ ℕ0 → ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑘 ) → ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) ) ) )
54 53 a2d ( 𝑘 ∈ ℕ0 → ( ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑘 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑘 ) ) → ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · ( 𝑘 + 1 ) ) ) = ( ( 𝐴𝑀 ) ↑ ( 𝑘 + 1 ) ) ) ) )
55 5 10 15 20 29 54 nn0ind ( 𝑁 ∈ ℕ0 → ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑁 ) ) )
56 55 expdcom ( 𝐴 ∈ ℂ → ( 𝑀 ∈ ℕ0 → ( 𝑁 ∈ ℕ0 → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑁 ) ) ) )
57 56 3imp ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴𝑀 ) ↑ 𝑁 ) )