Description: Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | qexpcl | ⊢ ( ( 𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ ) |
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 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℚ ) |