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

Metamath Proof Explorer

Theorem numexp1

Description: Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015)

		Ref	Expression
	Hypothesis	numexp.1	$⊢ A \in ℕ_{0}$
	Assertion	numexp1	$⊢ A^{1} = A$

Step	Hyp	Ref	Expression
1		numexp.1	$⊢ A \in ℕ_{0}$
2	1	nn0cni	$⊢ A \in ℂ$
3		exp1	$⊢ A \in ℂ \to A^{1} = A$
4	2 3	ax-mp	$⊢ A^{1} = A$