Theorem qexpclz

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

	Ref	Expression
Assertion	qexpclz	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		qsscn	⊢ ℚ ⊆ ℂ
2		qmulcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 · 𝑦 ) ∈ ℚ )
3		1z	⊢ 1 ∈ ℤ
4		zq	⊢ ( 1 ∈ ℤ → 1 ∈ ℚ )
5	3 4	ax-mp	⊢ 1 ∈ ℚ
6		qreccl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℚ )
7	1 2 5 6	expcl2lem	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ )