expaddzlem

		Ref	Expression
	Assertion	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}$

Proof

Step	Hyp	Ref	Expression
1		simp1l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A \in ℂ$
2		simp3	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to N \in ℕ_{0}$
3		expcl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{N} \in ℂ$
4	1 2 3	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{N} \in ℂ$
5		simp2r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℕ$
6	5	nnnn0d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℕ_{0}$
7		expcl	$⊢ (A \in ℂ \land - M \in ℕ_{0}) \to A^{- M} \in ℂ$
8	1 6 7	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{- M} \in ℂ$
9		simp1r	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A \neq 0$
10	5	nnzd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℤ$
11		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land - M \in ℤ) \to A^{- M} \neq 0$
12	1 9 10 11	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{- M} \neq 0$
13	4 8 12	divrec2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to \frac{A^{N}}{A^{- M}} = (\frac{1}{A^{- M}}) A^{N}$
14		simp2l	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M \in ℝ$
15	14	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M \in ℂ$
16	15	negnegd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - -M = M$
17		nnnegz	$⊢ - M \in ℕ \to - -M \in ℤ$
18	5 17	syl	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - -M \in ℤ$
19	16 18	eqeltrrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M \in ℤ$
20	2	nn0zd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to N \in ℤ$
21	19 20	zaddcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M + N \in ℤ$
22		expclz	$⊢ (A \in ℂ \land A \neq 0 \land M + N \in ℤ) \to A^{M + N} \in ℂ$
23	1 9 21 22	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M + N} \in ℂ$
24	23	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A^{M + N} \in ℂ$
25	8	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A^{- M} \in ℂ$
26	12	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A^{- M} \neq 0$
27	24 25 26	divcan4d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to \frac{A^{M + N} A^{- M}}{A^{- M}} = A^{M + N}$
28	1	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A \in ℂ$
29		simpr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to M + N \in ℕ_{0}$
30	6	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to - M \in ℕ_{0}$
31		expadd	$⊢ (A \in ℂ \land M + N \in ℕ_{0} \land - M \in ℕ_{0}) \to A^{M + N + -M} = A^{M + N} A^{- M}$
32	28 29 30 31	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A^{M + N + -M} = A^{M + N} A^{- M}$
33	21	zcnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M + N \in ℂ$
34	33 15	negsubd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M + N + -M = M + N - M$
35	2	nn0cnd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to N \in ℂ$
36	15 35	pncan2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M + N - M = N$
37	34 36	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to M + N + -M = N$
38	37	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to M + N + -M = N$
39	38	oveq2d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A^{M + N + -M} = A^{N}$
40	32 39	eqtr3d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A^{M + N} A^{- M} = A^{N}$
41	40	oveq1d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to \frac{A^{M + N} A^{- M}}{A^{- M}} = \frac{A^{N}}{A^{- M}}$
42	27 41	eqtr3d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land M + N \in ℕ_{0}) \to A^{M + N} = \frac{A^{N}}{A^{- M}}$
43	1	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A \in ℂ$
44	33	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to M + N \in ℂ$
45		simpr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to - (M + N) \in ℕ_{0}$
46		expneg2	$⊢ (A \in ℂ \land M + N \in ℂ \land - (M + N) \in ℕ_{0}) \to A^{M + N} = \frac{1}{A^{- (M + N)}}$
47	43 44 45 46	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{M + N} = \frac{1}{A^{- (M + N)}}$
48	21	znegcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - (M + N) \in ℤ$
49		expclz	$⊢ (A \in ℂ \land A \neq 0 \land - (M + N) \in ℤ) \to A^{- (M + N)} \in ℂ$
50	1 9 48 49	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{- (M + N)} \in ℂ$
51	50	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{- (M + N)} \in ℂ$
52	4	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{N} \in ℂ$
53		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \neq 0$
54	1 9 20 53	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{N} \neq 0$
55	54	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{N} \neq 0$
56	51 52 55	divcan4d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to \frac{A^{- (M + N)} A^{N}}{A^{N}} = A^{- (M + N)}$
57	2	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to N \in ℕ_{0}$
58		expadd	$⊢ (A \in ℂ \land - (M + N) \in ℕ_{0} \land N \in ℕ_{0}) \to A^{- (M + N) + N} = A^{- (M + N)} A^{N}$
59	43 45 57 58	syl3anc	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{- (M + N) + N} = A^{- (M + N)} A^{N}$
60	15	negcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℂ$
61	15 35	negdi2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - (M + N) = - M - N$
62	60 35 61	mvrrsubd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - (M + N) + N = - M$
63	62	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to - (M + N) + N = - M$
64	63	oveq2d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{- (M + N) + N} = A^{- M}$
65	59 64	eqtr3d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{- (M + N)} A^{N} = A^{- M}$
66	65	oveq1d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to \frac{A^{- (M + N)} A^{N}}{A^{N}} = \frac{A^{- M}}{A^{N}}$
67	56 66	eqtr3d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{- (M + N)} = \frac{A^{- M}}{A^{N}}$
68	67	oveq2d	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to \frac{1}{A^{- (M + N)}} = \frac{1}{\frac{A^{- M}}{A^{N}}}$
69	8 4 12 54	recdivd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to \frac{1}{\frac{A^{- M}}{A^{N}}} = \frac{A^{N}}{A^{- M}}$
70	69	adantr	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to \frac{1}{\frac{A^{- M}}{A^{N}}} = \frac{A^{N}}{A^{- M}}$
71	47 68 70	3eqtrd	$⊢ (((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \land - (M + N) \in ℕ_{0}) \to A^{M + N} = \frac{A^{N}}{A^{- M}}$
72		elznn0	$⊢ M + N \in ℤ \leftrightarrow (M + N \in ℝ \land (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0}))$
73	72	simprbi	$⊢ M + N \in ℤ \to (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0})$
74	21 73	syl	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0})$
75	42 71 74	mpjaodan	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M + N} = \frac{A^{N}}{A^{- M}}$
76		expneg2	$⊢ (A \in ℂ \land M \in ℂ \land - M \in ℕ_{0}) \to A^{M} = \frac{1}{A^{- M}}$
77	1 15 6 76	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M} = \frac{1}{A^{- M}}$
78	77	oveq1d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M} A^{N} = (\frac{1}{A^{- M}}) A^{N}$
79	13 75 78	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M + N} = A^{M} A^{N}$

Metamath Proof Explorer

Theorem expaddzlem

Proof