Metamath Proof Explorer

Theorem expmul

Description: Product of exponents law for positive 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 ) → ( 𝐴 ↑ ( 𝑀 · 𝑁 ) ) = ( ( 𝐴 ↑ 𝑀 ) ↑ 𝑁 ) )