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

Metamath Proof Explorer

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 1z ⊢ 1 ∈ ℤ
4 zq ⊢ ( 1 ∈ ℤ → 1 ∈ ℚ )
5 3 4 ax-mp ⊢ 1 ∈ ℚ
6 1 2 5 expcllem ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ )