expp1z

Description: Value of a nonzero complex number raised to an integer power plus one. (Contributed by Mario Carneiro, 4-Jun-2014)

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

Step	Hyp	Ref	Expression
1		1z	$⊢ 1 \in ℤ$
2		expaddz	$⊢ ((A \in ℂ \land A \neq 0) \land (N \in ℤ \land 1 \in ℤ)) \to A^{N + 1} = A^{N} A^{1}$
3	1 2	mpanr2	$⊢ ((A \in ℂ \land A \neq 0) \land N \in ℤ) \to A^{N + 1} = A^{N} A^{1}$
4	3	3impa	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N + 1} = 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 A^{N} A^{1} = A^{N} A$
8	4 7	eqtrd	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N + 1} = A^{N} A$

Metamath Proof Explorer