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	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to {AB}^N=A^N{B}^N$$

Proof

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