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 ) → ( ( 𝐴 · 𝐵 ) ↑ 𝑁 ) = ( ( 𝐴 ↑ 𝑁 ) · ( 𝐵 ↑ 𝑁 ) ) )