expsub

Description: Exponent subtraction law for nonnegative integer exponentiation. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
2		expaddz	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land - N \in ℤ)) \to A^{M + -N} = A^{M} A^{- N}$
3	1 2	sylanr2	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M + -N} = A^{M} A^{- N}$
4		zcn	$⊢ M \in ℤ \to M \in ℂ$
5		zcn	$⊢ N \in ℤ \to N \in ℂ$
6		negsub	$⊢ (M \in ℂ \land N \in ℂ) \to M + -N = M - N$
7	4 5 6	syl2an	$⊢ (M \in ℤ \land N \in ℤ) \to M + -N = M - N$
8	7	adantl	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to M + -N = M - N$
9	8	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M + -N} = A^{M - N}$
10		expnegz	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{- N} = \frac{1}{A^{N}}$
11	10	3expa	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℤ) \to A^{- N} = \frac{1}{A^{N}}$
12	11	adantrl	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{- N} = \frac{1}{A^{N}}$
13	12	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M} A^{- N} = A^{M} (\frac{1}{A^{N}})$
14		expclz	$⊢ (A \in ℂ \land A \neq 0 \land M \in ℤ) \to A^{M} \in ℂ$
15	14	3expa	$⊢ ((A \in ℂ \land A \neq 0) \land M \in ℤ) \to A^{M} \in ℂ$
16	15	adantrr	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M} \in ℂ$
17		expclz	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℂ$
18	17	3expa	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℤ) \to A^{N} \in ℂ$
19	18	adantrl	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{N} \in ℂ$
20		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \neq 0$
21	20	3expa	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℤ) \to A^{N} \neq 0$
22	21	adantrl	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{N} \neq 0$
23	16 19 22	divrecd	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to \frac{A^{M}}{A^{N}} = A^{M} (\frac{1}{A^{N}})$
24	13 23	eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M} A^{- N} = \frac{A^{M}}{A^{N}}$
25	3 9 24	3eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land (M \in ℤ \land N \in ℤ)) \to A^{M - N} = \frac{A^{M}}{A^{N}}$

Metamath Proof Explorer

Theorem expsub

Proof