expmulz

Description: Product of exponents law for integer exponentiation. Proposition 10-4.2(b) of Gleason p. 135. (Contributed by Mario Carneiro, 7-Jul-2014)

		Ref	Expression
	Assertion	expmulz	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M \cdot N} = {(A^{M})}^{N}$

Proof

Step	Hyp	Ref	Expression
1		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
2		elznn0nn	$⊢ M \in ℤ \leftrightarrow (M \in ℕ_{0} \lor (M \in ℝ \land - M \in ℕ))$
3		expmul	$⊢ (A \in ℂ \land M \in ℕ_{0} \land N \in ℕ_{0}) \to A^{M \cdot N} = {(A^{M})}^{N}$
4	3	3expia	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to (N \in ℕ_{0} \to A^{M \cdot N} = {(A^{M})}^{N})$
5	4	adantlr	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0}) \to (N \in ℕ_{0} \to A^{M \cdot N} = {(A^{M})}^{N})$
6		simp2l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M \in ℝ$
7	6	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M \in ℂ$
8		simp3	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to N \in ℕ_{0}$
9	8	nn0cnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to N \in ℂ$
10	7 9	mulneg1d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to -M \cdot N = - M \cdot N$
11	10	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{-M \cdot N} = A^{- M \cdot N}$
12		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A \in ℂ$
13		simp2r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℕ$
14	13	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℕ_{0}$
15		expmul	$⊢ (A \in ℂ \land - M \in ℕ_{0} \land N \in ℕ_{0}) \to A^{-M \cdot N} = {(A^{- M})}^{N}$
16	12 14 8 15	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{-M \cdot N} = {(A^{- M})}^{N}$
17	11 16	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{- M \cdot N} = {(A^{- M})}^{N}$
18	17	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to \frac{1}{A^{- M \cdot N}} = \frac{1}{{(A^{- M})}^{N}}$
19		expcl	$⊢ (A \in ℂ \land - M \in ℕ_{0}) \to A^{- M} \in ℂ$
20	12 14 19	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{- M} \in ℂ$
21		simp1r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A \neq 0$
22	13	nnzd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℤ$
23		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land - M \in ℤ) \to A^{- M} \neq 0$
24	12 21 22 23	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{- M} \neq 0$
25	8	nn0zd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to N \in ℤ$
26		exprec	$⊢ (A^{- M} \in ℂ \land A^{- M} \neq 0 \land N \in ℤ) \to {(\frac{1}{A^{- M}})}^{N} = \frac{1}{{(A^{- M})}^{N}}$
27	20 24 25 26	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to {(\frac{1}{A^{- M}})}^{N} = \frac{1}{{(A^{- M})}^{N}}$
28	18 27	eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to \frac{1}{A^{- M \cdot N}} = {(\frac{1}{A^{- M}})}^{N}$
29	7 9	mulcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M \cdot N \in ℂ$
30	14 8	nn0mulcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to -M \cdot N \in ℕ_{0}$
31	10 30	eqeltrrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \cdot N \in ℕ_{0}$
32		expneg2	$⊢ (A \in ℂ \land M \cdot N \in ℂ \land - M \cdot N \in ℕ_{0}) \to A^{M \cdot N} = \frac{1}{A^{- M \cdot N}}$
33	12 29 31 32	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M \cdot N} = \frac{1}{A^{- M \cdot N}}$
34		expneg2	$⊢ (A \in ℂ \land M \in ℂ \land - M \in ℕ_{0}) \to A^{M} = \frac{1}{A^{- M}}$
35	12 7 14 34	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M} = \frac{1}{A^{- M}}$
36	35	oveq1d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to {(A^{M})}^{N} = {(\frac{1}{A^{- M}})}^{N}$
37	28 33 36	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M \cdot N} = {(A^{M})}^{N}$
38	37	3expia	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ)) \to (N \in ℕ_{0} \to A^{M \cdot N} = {(A^{M})}^{N})$
39	5 38	jaodan	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℕ_{0} \lor (M \in ℝ \land - M \in ℕ))) \to (N \in ℕ_{0} \to A^{M \cdot N} = {(A^{M})}^{N})$
40		simp2	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to M \in ℕ_{0}$
41	40	nn0cnd	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to M \in ℂ$
42		simp3l	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to N \in ℝ$
43	42	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to N \in ℂ$
44	41 43	mulneg2d	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to M -N = - M \cdot N$
45	44	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to A^{M -N} = A^{- M \cdot N}$
46		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to A \in ℂ$
47		simp3r	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ$
48	47	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ_{0}$
49		expmul	$⊢ (A \in ℂ \land M \in ℕ_{0} \land - N \in ℕ_{0}) \to A^{M -N} = {(A^{M})}^{- N}$
50	46 40 48 49	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to A^{M -N} = {(A^{M})}^{- N}$
51	45 50	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to A^{- M \cdot N} = {(A^{M})}^{- N}$
52	51	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{A^{- M \cdot N}} = \frac{1}{{(A^{M})}^{- N}}$
53	41 43	mulcld	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to M \cdot N \in ℂ$
54	40 48	nn0mulcld	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to M -N \in ℕ_{0}$
55	44 54	eqeltrrd	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to - M \cdot N \in ℕ_{0}$
56	46 53 55 32	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to A^{M \cdot N} = \frac{1}{A^{- M \cdot N}}$
57		expcl	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to A^{M} \in ℂ$
58	46 40 57	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to A^{M} \in ℂ$
59		expneg2	$⊢ (A^{M} \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to {(A^{M})}^{N} = \frac{1}{{(A^{M})}^{- N}}$
60	58 43 48 59	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to {(A^{M})}^{N} = \frac{1}{{(A^{M})}^{- N}}$
61	52 56 60	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0} \land (N \in ℝ \land - N \in ℕ)) \to A^{M \cdot N} = {(A^{M})}^{N}$
62	61	3expia	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0}) \to ((N \in ℝ \land - N \in ℕ) \to A^{M \cdot N} = {(A^{M})}^{N})$
63		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A \in ℂ$
64		simp2l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to M \in ℝ$
65	64	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to M \in ℂ$
66		simp2r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - M \in ℕ$
67	66	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - M \in ℕ_{0}$
68	63 65 67 34	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{M} = \frac{1}{A^{- M}}$
69	68	oveq1d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to {(A^{M})}^{N} = {(\frac{1}{A^{- M}})}^{N}$
70	63 67 19	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{- M} \in ℂ$
71		simp1r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A \neq 0$
72	66	nnzd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - M \in ℤ$
73	63 71 72 23	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{- M} \neq 0$
74	70 73	reccld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{A^{- M}} \in ℂ$
75		simp3l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℝ$
76	75	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℂ$
77		simp3r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ$
78	77	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ_{0}$
79		expneg2	$⊢ (\frac{1}{A^{- M}} \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to {(\frac{1}{A^{- M}})}^{N} = \frac{1}{{(\frac{1}{A^{- M}})}^{- N}}$
80	74 76 78 79	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to {(\frac{1}{A^{- M}})}^{N} = \frac{1}{{(\frac{1}{A^{- M}})}^{- N}}$
81	77	nnzd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℤ$
82		exprec	$⊢ (A^{- M} \in ℂ \land A^{- M} \neq 0 \land - N \in ℤ) \to {(\frac{1}{A^{- M}})}^{- N} = \frac{1}{{(A^{- M})}^{- N}}$
83	70 73 81 82	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to {(\frac{1}{A^{- M}})}^{- N} = \frac{1}{{(A^{- M})}^{- N}}$
84	83	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{{(\frac{1}{A^{- M}})}^{- N}} = \frac{1}{\frac{1}{{(A^{- M})}^{- N}}}$
85		expcl	$⊢ (A^{- M} \in ℂ \land - N \in ℕ_{0}) \to {(A^{- M})}^{- N} \in ℂ$
86	70 78 85	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to {(A^{- M})}^{- N} \in ℂ$
87		expne0i	$⊢ (A^{- M} \in ℂ \land A^{- M} \neq 0 \land - N \in ℤ) \to {(A^{- M})}^{- N} \neq 0$
88	70 73 81 87	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to {(A^{- M})}^{- N} \neq 0$
89	86 88	recrecd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{\frac{1}{{(A^{- M})}^{- N}}} = {(A^{- M})}^{- N}$
90		expmul	$⊢ (A \in ℂ \land - M \in ℕ_{0} \land - N \in ℕ_{0}) \to A^{-M -N} = {(A^{- M})}^{- N}$
91	63 67 78 90	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{-M -N} = {(A^{- M})}^{- N}$
92	65 76	mul2negd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to -M -N = M \cdot N$
93	92	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{-M -N} = A^{M \cdot N}$
94	91 93	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to {(A^{- M})}^{- N} = A^{M \cdot N}$
95	84 89 94	3eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to \frac{1}{{(\frac{1}{A^{- M}})}^{- N}} = A^{M \cdot N}$
96	69 80 95	3eqtrrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{M \cdot N} = {(A^{M})}^{N}$
97	96	3expia	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ)) \to ((N \in ℝ \land - N \in ℕ) \to A^{M \cdot N} = {(A^{M})}^{N})$
98	62 97	jaodan	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℕ_{0} \lor (M \in ℝ \land - M \in ℕ))) \to ((N \in ℝ \land - N \in ℕ) \to A^{M \cdot N} = {(A^{M})}^{N})$
99	39 98	jaod	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℕ_{0} \lor (M \in ℝ \land - M \in ℕ))) \to ((N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ)) \to A^{M \cdot N} = {(A^{M})}^{N})$
100	2 99	sylan2b	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℤ) \to ((N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ)) \to A^{M \cdot N} = {(A^{M})}^{N})$
101	1 100	biimtrid	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℤ) \to (N \in ℤ \to A^{M \cdot N} = {(A^{M})}^{N})$
102	101	impr	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M \cdot N} = {(A^{M})}^{N}$

Metamath Proof Explorer

Theorem expmulz

Proof