Theorem expnnval

Description: Value of exponentiation to positive integer powers. (Contributed by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
2		expval	$$⊢\left(A\in ℂ\wedge N\in \mathbb{Z}\right)\to A^N=if\left(N=0,1,if\left(0<N,seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(-N\right)}\right)\right)$$
3	1 2	sylan2	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to A^N=if\left(N=0,1,if\left(0<N,seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(-N\right)}\right)\right)$$
4		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
5	4	neneqd	$$⊢N\in \mathbb{N}\to \neg N=0$$
6	5	iffalsed	$$⊢N\in \mathbb{N}\to if\left(N=0,1,if\left(0<N,seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(-N\right)}\right)\right)=if\left(0<N,seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(-N\right)}\right)$$
7		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
8	7	iftrued	$$⊢N\in \mathbb{N}\to if\left(0<N,seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(-N\right)}\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)$$
9	6 8	eqtrd	$$⊢N\in \mathbb{N}\to if\left(N=0,1,if\left(0<N,seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(-N\right)}\right)\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)$$
10	9	adantl	$$⊢\left(A\in ℂ\wedge N\in \mathbb{N}\right)\to if\left(N=0,1,if\left(0<N,seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right),\frac{1}{seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(-N\right)}\right)\right)=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(N\right)$$
11	3 10	eqtrd	$$⊢\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)$$