This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cxp1

Description: Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014)

		Ref	Expression
	Assertion	cxp1	$⊢ A \in ℂ \to A^{1} = A$

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		cxpexp	$⊢ (A \in ℂ \land 1 \in ℕ_{0}) \to A^{1} = A^{1}$
3	1 2	mpan2	$⊢ A \in ℂ \to A^{1} = A^{1}$
4		exp1	$⊢ A \in ℂ \to A^{1} = A$
5	3 4	eqtrd	$⊢ A \in ℂ \to A^{1} = A$