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	$⊢ (A \in ℂ \land M \in ℕ_{0} \land N \in ℕ_{0}) \to A^{M \cdot N} = {(A^{M})}^{N}$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ j = 0 \to M j = M \cdot 0$
2	1	oveq2d	$⊢ j = 0 \to A^{M j} = A^{M \cdot 0}$
3		oveq2	$⊢ j = 0 \to {(A^{M})}^{j} = {(A^{M})}^{0}$
4	2 3	eqeq12d	$⊢ j = 0 \to (A^{M j} = {(A^{M})}^{j} \leftrightarrow A^{M \cdot 0} = {(A^{M})}^{0})$
5	4	imbi2d	$⊢ j = 0 \to (((A \in ℂ \land M \in ℕ_{0}) \to A^{M j} = {(A^{M})}^{j}) \leftrightarrow ((A \in ℂ \land M \in ℕ_{0}) \to A^{M \cdot 0} = {(A^{M})}^{0}))$
6		oveq2	$⊢ j = k \to M j = M k$
7	6	oveq2d	$⊢ j = k \to A^{M j} = A^{M k}$
8		oveq2	$⊢ j = k \to {(A^{M})}^{j} = {(A^{M})}^{k}$
9	7 8	eqeq12d	$⊢ j = k \to (A^{M j} = {(A^{M})}^{j} \leftrightarrow A^{M k} = {(A^{M})}^{k})$
10	9	imbi2d	$⊢ j = k \to (((A \in ℂ \land M \in ℕ_{0}) \to A^{M j} = {(A^{M})}^{j}) \leftrightarrow ((A \in ℂ \land M \in ℕ_{0}) \to A^{M k} = {(A^{M})}^{k}))$
11		oveq2	$⊢ j = k + 1 \to M j = M (k + 1)$
12	11	oveq2d	$⊢ j = k + 1 \to A^{M j} = A^{M (k + 1)}$
13		oveq2	$⊢ j = k + 1 \to {(A^{M})}^{j} = {(A^{M})}^{k + 1}$
14	12 13	eqeq12d	$⊢ j = k + 1 \to (A^{M j} = {(A^{M})}^{j} \leftrightarrow A^{M (k + 1)} = {(A^{M})}^{k + 1})$
15	14	imbi2d	$⊢ j = k + 1 \to (((A \in ℂ \land M \in ℕ_{0}) \to A^{M j} = {(A^{M})}^{j}) \leftrightarrow ((A \in ℂ \land M \in ℕ_{0}) \to A^{M (k + 1)} = {(A^{M})}^{k + 1}))$
16		oveq2	$⊢ j = N \to M j = M \cdot N$
17	16	oveq2d	$⊢ j = N \to A^{M j} = A^{M \cdot N}$
18		oveq2	$⊢ j = N \to {(A^{M})}^{j} = {(A^{M})}^{N}$
19	17 18	eqeq12d	$⊢ j = N \to (A^{M j} = {(A^{M})}^{j} \leftrightarrow A^{M \cdot N} = {(A^{M})}^{N})$
20	19	imbi2d	$⊢ j = N \to (((A \in ℂ \land M \in ℕ_{0}) \to A^{M j} = {(A^{M})}^{j}) \leftrightarrow ((A \in ℂ \land M \in ℕ_{0}) \to A^{M \cdot N} = {(A^{M})}^{N}))$
21		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
22	21	mul01d	$⊢ M \in ℕ_{0} \to M \cdot 0 = 0$
23	22	oveq2d	$⊢ M \in ℕ_{0} \to A^{M \cdot 0} = A^{0}$
24		exp0	$⊢ A \in ℂ \to A^{0} = 1$
25	23 24	sylan9eqr	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to A^{M \cdot 0} = 1$
26		expcl	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to A^{M} \in ℂ$
27		exp0	$⊢ A^{M} \in ℂ \to {(A^{M})}^{0} = 1$
28	26 27	syl	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to {(A^{M})}^{0} = 1$
29	25 28	eqtr4d	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to A^{M \cdot 0} = {(A^{M})}^{0}$
30		oveq1	$⊢ A^{M k} = {(A^{M})}^{k} \to A^{M k} A^{M} = {(A^{M})}^{k} A^{M}$
31		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
32		ax-1cn	$⊢ 1 \in ℂ$
33		adddi	$⊢ (M \in ℂ \land k \in ℂ \land 1 \in ℂ) \to M (k + 1) = M k + M \cdot 1$
34	32 33	mp3an3	$⊢ (M \in ℂ \land k \in ℂ) \to M (k + 1) = M k + M \cdot 1$
35		mulid1	$⊢ M \in ℂ \to M \cdot 1 = M$
36	35	adantr	$⊢ (M \in ℂ \land k \in ℂ) \to M \cdot 1 = M$
37	36	oveq2d	$⊢ (M \in ℂ \land k \in ℂ) \to M k + M \cdot 1 = M k + M$
38	34 37	eqtrd	$⊢ (M \in ℂ \land k \in ℂ) \to M (k + 1) = M k + M$
39	21 31 38	syl2an	$⊢ (M \in ℕ_{0} \land k \in ℕ_{0}) \to M (k + 1) = M k + M$
40	39	adantll	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to M (k + 1) = M k + M$
41	40	oveq2d	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{M (k + 1)} = A^{M k + M}$
42		simpll	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to A \in ℂ$
43		nn0mulcl	$⊢ (M \in ℕ_{0} \land k \in ℕ_{0}) \to M k \in ℕ_{0}$
44	43	adantll	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to M k \in ℕ_{0}$
45		simplr	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to M \in ℕ_{0}$
46		expadd	$⊢ (A \in ℂ \land M k \in ℕ_{0} \land M \in ℕ_{0}) \to A^{M k + M} = A^{M k} A^{M}$
47	42 44 45 46	syl3anc	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{M k + M} = A^{M k} A^{M}$
48	41 47	eqtrd	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to A^{M (k + 1)} = A^{M k} A^{M}$
49		expp1	$⊢ (A^{M} \in ℂ \land k \in ℕ_{0}) \to {(A^{M})}^{k + 1} = {(A^{M})}^{k} A^{M}$
50	26 49	sylan	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to {(A^{M})}^{k + 1} = {(A^{M})}^{k} A^{M}$
51	48 50	eqeq12d	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to (A^{M (k + 1)} = {(A^{M})}^{k + 1} \leftrightarrow A^{M k} A^{M} = {(A^{M})}^{k} A^{M})$
52	30 51	syl5ibr	$⊢ ((A \in ℂ \land M \in ℕ_{0}) \land k \in ℕ_{0}) \to (A^{M k} = {(A^{M})}^{k} \to A^{M (k + 1)} = {(A^{M})}^{k + 1})$
53	52	expcom	$⊢ k \in ℕ_{0} \to ((A \in ℂ \land M \in ℕ_{0}) \to (A^{M k} = {(A^{M})}^{k} \to A^{M (k + 1)} = {(A^{M})}^{k + 1}))$
54	53	a2d	$⊢ k \in ℕ_{0} \to (((A \in ℂ \land M \in ℕ_{0}) \to A^{M k} = {(A^{M})}^{k}) \to ((A \in ℂ \land M \in ℕ_{0}) \to A^{M (k + 1)} = {(A^{M})}^{k + 1}))$
55	5 10 15 20 29 54	nn0ind	$⊢ N \in ℕ_{0} \to ((A \in ℂ \land M \in ℕ_{0}) \to A^{M \cdot N} = {(A^{M})}^{N})$
56	55	expdcom	$⊢ A \in ℂ \to (M \in ℕ_{0} \to (N \in ℕ_{0} \to A^{M \cdot N} = {(A^{M})}^{N}))$
57	56	3imp	$⊢ (A \in ℂ \land M \in ℕ_{0} \land N \in ℕ_{0}) \to A^{M \cdot N} = {(A^{M})}^{N}$

Metamath Proof Explorer

Theorem expmul

Proof