expaddz

Description: Sum of exponents law for integer exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by Mario Carneiro, 4-Jun-2014)

		Ref	Expression
	Assertion	expaddz	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M + N} = A^{M} A^{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		expadd	$⊢ (A \in ℂ \land M \in ℕ_{0} \land N \in ℕ_{0}) \to A^{M + N} = A^{M} A^{N}$
4	3	3expia	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to (N \in ℕ_{0} \to A^{M + N} = A^{M} A^{N})$
5	4	adantlr	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0}) \to (N \in ℕ_{0} \to A^{M + N} = A^{M} A^{N})$
6		expaddzlem	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M + N} = A^{M} A^{N}$
7	6	3expia	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ)) \to (N \in ℕ_{0} \to A^{M + N} = A^{M} A^{N})$
8	5 7	jaodan	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℕ_{0} \lor (M \in ℝ \land - M \in ℕ))) \to (N \in ℕ_{0} \to A^{M + N} = A^{M} A^{N})$
9		expaddzlem	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A^{N + M} = A^{N} A^{M}$
10		simp3	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to M \in ℕ_{0}$
11	10	nn0cnd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to M \in ℂ$
12		simp2l	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to N \in ℝ$
13	12	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to N \in ℂ$
14	11 13	addcomd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to M + N = N + M$
15	14	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A^{M + N} = A^{N + M}$
16		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A \in ℂ$
17		expcl	$⊢ (A \in ℂ \land M \in ℕ_{0}) \to A^{M} \in ℂ$
18	16 10 17	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A^{M} \in ℂ$
19		simp1r	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A \neq 0$
20	13	negnegd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to - -N = N$
21		simp2r	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to - N \in ℕ$
22	21	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to - N \in ℕ_{0}$
23		nn0negz	$⊢ - N \in ℕ_{0} \to - -N \in ℤ$
24	22 23	syl	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to - -N \in ℤ$
25	20 24	eqeltrrd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to N \in ℤ$
26		expclz	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℂ$
27	16 19 25 26	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A^{N} \in ℂ$
28	18 27	mulcomd	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A^{M} A^{N} = A^{N} A^{M}$
29	9 15 28	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ) \land M \in ℕ_{0}) \to A^{M + N} = A^{M} A^{N}$
30	29	3expia	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℝ \land - N \in ℕ)) \to (M \in ℕ_{0} \to A^{M + N} = A^{M} A^{N})$
31	30	impancom	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℕ_{0}) \to ((N \in ℝ \land - N \in ℕ) \to A^{M + N} = A^{M} A^{N})$
32		simp2l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to M \in ℝ$
33	32	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to M \in ℂ$
34		simp3l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℝ$
35	34	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℂ$
36	33 35	negdid	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - (M + N) = - M + -N$
37	36	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 + -N}$
38		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A \in ℂ$
39		simp2r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - M \in ℕ$
40	39	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - M \in ℕ_{0}$
41		simp3r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ$
42	41	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ_{0}$
43		expadd	$⊢ (A \in ℂ \land - M \in ℕ_{0} \land - N \in ℕ_{0}) \to A^{- M + -N} = A^{- M} A^{- N}$
44	38 40 42 43	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} A^{- N}$
45	37 44	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{- (M + N)} = A^{- M} A^{- N}$
46	45	oveq2d	$⊢ ((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} A^{- N}}$
47		1t1e1	$⊢ 1 \cdot 1 = 1$
48	47	oveq1i	$⊢ \frac{1 \cdot 1}{A^{- M} A^{- N}} = \frac{1}{A^{- M} A^{- N}}$
49	46 48	syl6eqr	$⊢ ((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 \cdot 1}{A^{- M} A^{- N}}$
50		expcl	$⊢ (A \in ℂ \land - M \in ℕ_{0}) \to A^{- M} \in ℂ$
51	38 40 50	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{- M} \in ℂ$
52		simp1r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A \neq 0$
53	40	nn0zd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - M \in ℤ$
54		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land - M \in ℤ) \to A^{- M} \neq 0$
55	38 52 53 54	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{- M} \neq 0$
56		expcl	$⊢ (A \in ℂ \land - N \in ℕ_{0}) \to A^{- N} \in ℂ$
57	38 42 56	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{- N} \in ℂ$
58	42	nn0zd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℤ$
59		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land - N \in ℤ) \to A^{- N} \neq 0$
60	38 52 58 59	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{- N} \neq 0$
61		ax-1cn	$⊢ 1 \in ℂ$
62		divmuldiv	$⊢ ((1 \in ℂ \land 1 \in ℂ) \land ((A^{- M} \in ℂ \land A^{- M} \neq 0) \land (A^{- N} \in ℂ \land A^{- N} \neq 0))) \to (\frac{1}{A^{- M}}) (\frac{1}{A^{- N}}) = \frac{1 \cdot 1}{A^{- M} A^{- N}}$
63	61 61 62	mpanl12	$⊢ ((A^{- M} \in ℂ \land A^{- M} \neq 0) \land (A^{- N} \in ℂ \land A^{- N} \neq 0)) \to (\frac{1}{A^{- M}}) (\frac{1}{A^{- N}}) = \frac{1 \cdot 1}{A^{- M} A^{- N}}$
64	51 55 57 60 63	syl22anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to (\frac{1}{A^{- M}}) (\frac{1}{A^{- N}}) = \frac{1 \cdot 1}{A^{- M} A^{- N}}$
65	49 64	eqtr4d	$⊢ ((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}}) (\frac{1}{A^{- N}})$
66	33 35	addcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to M + N \in ℂ$
67	40 42	nn0addcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - M + -N \in ℕ_{0}$
68	36 67	eqeltrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to - (M + N) \in ℕ_{0}$
69		expneg2	$⊢ (A \in ℂ \land M + N \in ℂ \land - (M + N) \in ℕ_{0}) \to A^{M + N} = \frac{1}{A^{- (M + N)}}$
70	38 66 68 69	syl3anc	$⊢ ((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)}}$
71		expneg2	$⊢ (A \in ℂ \land M \in ℂ \land - M \in ℕ_{0}) \to A^{M} = \frac{1}{A^{- M}}$
72	38 33 40 71	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}}$
73		expneg2	$⊢ (A \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to A^{N} = \frac{1}{A^{- N}}$
74	38 35 42 73	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{N} = \frac{1}{A^{- N}}$
75	72 74	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{M} A^{N} = (\frac{1}{A^{- M}}) (\frac{1}{A^{- N}})$
76	65 70 75	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land (N \in ℝ \land - N \in ℕ)) \to A^{M + N} = A^{M} A^{N}$
77	76	3expia	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ)) \to ((N \in ℝ \land - N \in ℕ) \to A^{M + N} = A^{M} A^{N})$
78	31 77	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 + N} = A^{M} A^{N})$
79	8 78	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 + N} = A^{M} A^{N})$
80	2 79	sylan2b	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℤ) \to ((N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ)) \to A^{M + N} = A^{M} A^{N})$
81	1 80	syl5bi	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℤ) \to (N \in ℤ \to A^{M + N} = A^{M} A^{N})$
82	81	impr	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M + N} = A^{M} A^{N}$

Metamath Proof Explorer

Theorem expaddz

Proof