Metamath Proof Explorer
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 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ ) |