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 e. CC -> ( A ^ 1 ) = A )

Proof

Step	Hyp	Ref	Expression
1		1nn	|- 1 e. NN
2		expnnval	|- ( ( A e. CC /\ 1 e. NN ) -> ( A ^ 1 ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` 1 ) )
3	1 2	mpan2	|- ( A e. CC -> ( A ^ 1 ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` 1 ) )
4		1z	|- 1 e. ZZ
5		seq1	|- ( 1 e. ZZ -> ( seq 1 ( x. , ( NN X. { A } ) ) ` 1 ) = ( ( NN X. { A } ) ` 1 ) )
6	4 5	ax-mp	|- ( seq 1 ( x. , ( NN X. { A } ) ) ` 1 ) = ( ( NN X. { A } ) ` 1 )
7	3 6	eqtrdi	|- ( A e. CC -> ( A ^ 1 ) = ( ( NN X. { A } ) ` 1 ) )
8		fvconst2g	|- ( ( A e. CC /\ 1 e. NN ) -> ( ( NN X. { A } ) ` 1 ) = A )
9	1 8	mpan2	|- ( A e. CC -> ( ( NN X. { A } ) ` 1 ) = A )
10	7 9	eqtrd	|- ( A e. CC -> ( A ^ 1 ) = A )