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$

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2		expnnval	$⊢ (A \in ℂ \land 1 \in ℕ) \to A^{1} = seq 1 (\times (ℕ \times \{A\})) (1)$
3	1 2	mpan2	$⊢ A \in ℂ \to A^{1} = seq 1 (\times (ℕ \times \{A\})) (1)$
4		1z	$⊢ 1 \in ℤ$
5		seq1	$⊢ 1 \in ℤ \to seq 1 (\times (ℕ \times \{A\})) (1) = (ℕ \times \{A\}) (1)$
6	4 5	ax-mp	$⊢ seq 1 (\times (ℕ \times \{A\})) (1) = (ℕ \times \{A\}) (1)$
7	3 6	eqtrdi	$⊢ A \in ℂ \to A^{1} = (ℕ \times \{A\}) (1)$
8		fvconst2g	$⊢ (A \in ℂ \land 1 \in ℕ) \to (ℕ \times \{A\}) (1) = A$
9	1 8	mpan2	$⊢ A \in ℂ \to (ℕ \times \{A\}) (1) = A$
10	7 9	eqtrd	$⊢ A \in ℂ \to A^{1} = A$

Metamath Proof Explorer