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

Metamath Proof Explorer

Theorem cxp0

Description: Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014)

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

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