This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exprecd

Description: An integer power of a reciprocal is the reciprocal of the integer power with same exponent. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	expcld.1	$⊢ φ \to A \in ℂ$
	sqrecd.1	$⊢ φ \to A \neq 0$
	expclzd.3	$⊢ φ \to N \in ℤ$
Assertion	exprecd	$⊢ φ \to {(\frac{1}{A})}^{N} = \frac{1}{A^{N}}$

Proof

Step	Hyp	Ref	Expression
1		expcld.1	$⊢ φ \to A \in ℂ$
2		sqrecd.1	$⊢ φ \to A \neq 0$
3		expclzd.3	$⊢ φ \to N \in ℤ$
4		exprec	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to {(\frac{1}{A})}^{N} = \frac{1}{A^{N}}$
5	1 2 3 4	syl3anc	$⊢ φ \to {(\frac{1}{A})}^{N} = \frac{1}{A^{N}}$