Theorem qexpclz

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

	Ref	Expression
Assertion	qexpclz	$$⊢\left(A\in \mathbb{Q}\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\in \mathbb{Q}$$

Proof

Step	Hyp	Ref	Expression
1		qsscn	$$⊢\mathbb{Q}\subseteq ℂ$$
2		qmulcl	$$⊢\left(x\in \mathbb{Q}\wedge y\in \mathbb{Q}\right)\to xy\in \mathbb{Q}$$
3		1z	$$⊢1\in \mathbb{Z}$$
4		zq	$$⊢1\in \mathbb{Z}\to 1\in \mathbb{Q}$$
5	3 4	ax-mp	$$⊢1\in \mathbb{Q}$$
6		qreccl	$$⊢\left(x\in \mathbb{Q}\wedge x\ne 0\right)\to \frac{1}{x}\in \mathbb{Q}$$
7	1 2 5 6	expcl2lem	$$⊢\left(A\in \mathbb{Q}\wedge A\ne 0\wedge N\in \mathbb{Z}\right)\to A^N\in \mathbb{Q}$$