Metamath Proof Explorer

Theorem exprec

Description: Integer exponentiation of a reciprocal. (Contributed by NM, 2-Aug-2006) (Revised by Mario Carneiro, 4-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		expclz	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℂ$
2		reccl	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \in ℂ$
3	2	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to \frac{1}{A} \in ℂ$
4		recne0	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \neq 0$
5	4	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to \frac{1}{A} \neq 0$
6		simp3	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to N \in ℤ$
7		expclz	$⊢ (\frac{1}{A} \in ℂ \land \frac{1}{A} \neq 0 \land N \in ℤ) \to {(\frac{1}{A})}^{N} \in ℂ$
8	3 5 6 7	syl3anc	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to {(\frac{1}{A})}^{N} \in ℂ$
9		expne0i	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \neq 0$
10		simp1	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A \in ℂ$
11		simp2	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A \neq 0$
12	10 11	recidd	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A (\frac{1}{A}) = 1$
13	12	oveq1d	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to {A (\frac{1}{A})}^{N} = 1^{N}$
14		mulexpz	$⊢ ((A \in ℂ \land A \neq 0) \land (\frac{1}{A} \in ℂ \land \frac{1}{A} \neq 0) \land N \in ℤ) \to {A (\frac{1}{A})}^{N} = A^{N} {(\frac{1}{A})}^{N}$
15	10 11 3 5 6 14	syl221anc	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to {A (\frac{1}{A})}^{N} = A^{N} {(\frac{1}{A})}^{N}$
16		1exp	$⊢ N \in ℤ \to 1^{N} = 1$
17	6 16	syl	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to 1^{N} = 1$
18	13 15 17	3eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} {(\frac{1}{A})}^{N} = 1$
19	1 8 9 18	mvllmuld	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to {(\frac{1}{A})}^{N} = \frac{1}{A^{N}}$