Theorem qexpcl

Description: Closure of exponentiation of rationals. For integer exponents, see qexpclz . (Contributed by NM, 16-Dec-2005)

	Ref	Expression
Assertion	qexpcl	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ )

Proof

Step	Hyp	Ref	Expression
1		qsscn	⊢ ℚ ⊆ ℂ
2		qmulcl	⊢ ( ( 𝑥 ∈ ℚ ∧ 𝑦 ∈ ℚ ) → ( 𝑥 · 𝑦 ) ∈ ℚ )
3		1q	⊢ 1 ∈ ℚ
4	1 2 3	expcllem	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ )