Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
Integer powers
qexpcl
Next ⟩
reexpcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
qexpcl
Description:
Closure of exponentiation of rationals.
(Contributed by
NM
, 16-Dec-2005)
Ref
Expression
Assertion
qexpcl
⊢
A
∈
ℚ
∧
N
∈
ℕ
0
→
A
N
∈
ℚ
Proof
Step
Hyp
Ref
Expression
1
qsscn
⊢
ℚ
⊆
ℂ
2
qmulcl
⊢
x
∈
ℚ
∧
y
∈
ℚ
→
x
⁢
y
∈
ℚ
3
1z
⊢
1
∈
ℤ
4
zq
⊢
1
∈
ℤ
→
1
∈
ℚ
5
3
4
ax-mp
⊢
1
∈
ℚ
6
1
2
5
expcllem
⊢
A
∈
ℚ
∧
N
∈
ℕ
0
→
A
N
∈
ℚ