This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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