Metamath Proof Explorer


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