Metamath Proof Explorer

Theorem expm1

Description: Value of a nonzero complex number raised to an integer power minus one. (Contributed by NM, 25-Dec-2008) (Revised by Mario Carneiro, 4-Jun-2014)

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

Proof

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		expsub	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℤ \land 1 \in ℤ)) \to A^{N - 1} = \frac{A^{N}}{A^{1}}$
3	1 2	mpanr2	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℤ) \to A^{N - 1} = \frac{A^{N}}{A^{1}}$
4	3	3impa	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N - 1} = \frac{A^{N}}{A^{1}}$
5		exp1	$⊢ A \in ℂ \to A^{1} = A$
6	5	3ad2ant1	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{1} = A$
7	6	oveq2d	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to \frac{A^{N}}{A^{1}} = \frac{A^{N}}{A}$
8	4 7	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N - 1} = \frac{A^{N}}{A}$