Theorem exp1

Description: Value of a complex number raised to the first power. (Contributed by NM, 20-Oct-2004) (Revised by Mario Carneiro, 2-Jul-2013)

	Ref	Expression
Assertion	exp1	$$⊢A\in ℂ\to A^1=A$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		expnnval	$$⊢\left(A\in ℂ\wedge 1\in \mathbb{N}\right)\to A^1=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(1\right)$$
3	1 2	mpan2	$$⊢A\in ℂ\to A^1=seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(1\right)$$
4		1z	$$⊢1\in \mathbb{Z}$$
5		seq1	$$⊢1\in \mathbb{Z}\to seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(1\right)=\left(\mathbb{N}\times \left\{A\right\}\right)\left(1\right)$$
6	4 5	ax-mp	$$⊢seq1\left(\times ,\left(\mathbb{N}\times \left\{A\right\}\right)\right)\left(1\right)=\left(\mathbb{N}\times \left\{A\right\}\right)\left(1\right)$$
7	3 6	eqtrdi	$$⊢A\in ℂ\to A^1=\left(\mathbb{N}\times \left\{A\right\}\right)\left(1\right)$$
8		fvconst2g	$$⊢\left(A\in ℂ\wedge 1\in \mathbb{N}\right)\to \left(\mathbb{N}\times \left\{A\right\}\right)\left(1\right)=A$$
9	1 8	mpan2	$$⊢A\in ℂ\to \left(\mathbb{N}\times \left\{A\right\}\right)\left(1\right)=A$$
10	7 9	eqtrd	$$⊢A\in ℂ\to A^1=A$$