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

Metamath Proof Explorer

Theorem qexpclz

Description: Closure of integer exponentiation of rational numbers. (Contributed by Mario Carneiro, 9-Sep-2014)

		Ref	Expression
	Assertion	qexpclz	$⊢ (A \in ℚ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℚ$

Step	Hyp	Ref	Expression
1		qsscn	$⊢ ℚ \subseteq ℂ$
2		qmulcl	$⊢ (x \in ℚ \land y \in ℚ) \to x y \in ℚ$
3		1z	$⊢ 1 \in ℤ$
4		zq	$⊢ 1 \in ℤ \to 1 \in ℚ$
5	3 4	ax-mp	$⊢ 1 \in ℚ$
6		qreccl	$⊢ (x \in ℚ \land x \neq 0) \to \frac{1}{x} \in ℚ$
7	1 2 5 6	expcl2lem	$⊢ (A \in ℚ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℚ$