Theorem expp1

Description: Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of Gleason p. 134. When A is nonzero, this holds for all integers N , see expneg . (Contributed by NM, 20-May-2005) (Revised by Mario Carneiro, 2-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
2		seqp1	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N+1\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)\left(\mathbb{N}\times \left\{A\right\}\right)\left(N+1\right)$$
3		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
4	2 3	eleq2s	$$⊢N\in \mathbb{N}\to seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N+1\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)\left(\mathbb{N}\times \left\{A\right\}\right)\left(N+1\right)$$
5	4	adantl	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N+1\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)\left(\mathbb{N}\times \left\{A\right\}\right)\left(N+1\right)$$
6		peano2nn	$$⊢N\in \mathbb{N}\to N+1\in \mathbb{N}$$
7		fvconst2g	$$⊢\left(A\in ℂ\wedge N+1\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{A\right\}\right)\left(N+1\right)=A$$
8	6 7	sylan2	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{A\right\}\right)\left(N+1\right)=A$$
9	8	oveq2d	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)\left(\mathbb{N}\times \left\{A\right\}\right)\left(N+1\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)A$$
10	5 9	eqtrd	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N+1\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)A$$
11		expnnval	$$⊢\left(A\in ℂ\wedge N+1\in \mathbb{N}\right)\to A^{N+1}=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N+1\right)$$
12	6 11	sylan2	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^{N+1}=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N+1\right)$$
13		expnnval	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^N=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)$$
14	13	oveq1d	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^{N}A=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)A$$
15	10 12 14	3eqtr4d	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^{N+1}=A^{N}A$$
16		exp1	$$⊢A\in ℂ\to A^1=A$$
17		mullid	$$⊢A\in ℂ\to 1A=A$$
18	16 17	eqtr4d	$$⊢A\in ℂ\to A^1=1A$$
19	18	adantr	$$⊢\left(A\in ℂ\wedge N=0\right)\to A^1=1A$$
20		simpr	$$⊢\left(A\in ℂ\wedge N=0\right)\to N=0$$
21	20	oveq1d	$$⊢\left(A\in ℂ\wedge N=0\right)\to N+1=0+1$$
22		0p1e1	$$⊢0+1=1$$
23	21 22	eqtrdi	$$⊢\left(A\in ℂ\wedge N=0\right)\to N+1=1$$
24	23	oveq2d	$$⊢\left(A\in ℂ\wedge N=0\right)\to A^{N+1}=A^1$$
25		oveq2	$$⊢N=0\to A^N=A^0$$
26		exp0	$$⊢A\in ℂ\to A^0=1$$
27	25 26	sylan9eqr	$$⊢\left(A\in ℂ\wedge N=0\right)\to A^N=1$$
28	27	oveq1d	$$⊢\left(A\in ℂ\wedge N=0\right)\to A^{N}A=1A$$
29	19 24 28	3eqtr4d	$$⊢\left(A\in ℂ\wedge N=0\right)\to A^{N+1}=A^{N}A$$
30	15 29	jaodan	$$⊢\left(A\in ℂ\wedge \left(N\in \mathbb{N}\vee N=0\right)\right)\to A^{N+1}=A^{N}A$$
31	1 30	sylan2b	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to A^{N+1}=A^{N}A$$