Theorem cxpp1

Description: Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Assertion	cxpp1	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{B+1}=A^{B}A$$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$$⊢1\in ℂ$$
2		cxpadd	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in ℂ\wedge 1\in ℂ\right)\to A^{B+1}=A^B{A}^1$$
3	1 2	mp3an3	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in ℂ\right)\to A^{B+1}=A^B{A}^1$$
4	3	3impa	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{B+1}=A^B{A}^1$$
5		cxp1	$$⊢A\in ℂ\to A^1=A$$
6	5	3ad2ant1	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^1=A$$
7	6	oveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B{A}^1=A^{B}A$$
8	4 7	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^{B+1}=A^{B}A$$