Theorem expm1t

Description: Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005)

	Ref	Expression
Assertion	expm1t	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^N=A^{N-1}A$$

Proof

Step	Hyp	Ref	Expression
1		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3		npcan	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N-1+1=N$$
4	1 2 3	sylancl	$$⊢N\in \mathbb{N}\to N-1+1=N$$
5	4	oveq2d	$$⊢N\in \mathbb{N}\to A^{N-1+1}=A^N$$
6	5	adantl	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^{N-1+1}=A^N$$
7		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
8		expp1	$$⊢\left(A\in ℂ\wedge N-1\in {\mathbb{N}}_0\right)\to A^{N-1+1}=A^{N-1}A$$
9	7 8	sylan2	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^{N-1+1}=A^{N-1}A$$
10	6 9	eqtr3d	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^N=A^{N-1}A$$