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 35	negdi2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - (M + N) = - M - N$
61	60	oveq1d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - (M + N) + N = -M - N + N$
62	15	negcld	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - M \in ℂ$
63	62 35	npcand	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to -M - N + N = - M$
64	61 63	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to - (M + N) + N = - M$
65	64	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$
66	65	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}$
67	59 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)} A^{N} = A^{- M}$
68	67	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}}$
69	56 68	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}}$
70	69	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}}}$
71	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}}$
72	71	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}}$
73	70 72	eqtrd	$⊢ (((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{A^{N}}{A^{- M}}$
74	47 73	eqtrd	$⊢ (((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}}$
75		elznn0	$⊢ M + N \in ℤ \leftrightarrow (M + N \in ℝ \land (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0}))$
76	75	simprbi	$⊢ M + N \in ℤ \to (M + N \in ℕ_{0} \lor - (M + N) \in ℕ_{0})$
77	21 76	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})$
78	42 74 77	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}}$
79		expneg2	$⊢ (A \in ℂ \land M \in ℂ \land - M \in ℕ_{0}) \to A^{M} = \frac{1}{A^{- M}}$
80	1 15 6 79	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℝ \land - M \in ℕ) \land N \in ℕ_{0}) \to A^{M} = \frac{1}{A^{- M}}$
81	80	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}$
82	13 78 81	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