Description: Closure of exponentiation of rationals. (Contributed by NM, 16-Dec-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | qexpcl | |- ( ( A e. QQ /\ N e. NN0 ) -> ( A ^ N ) e. QQ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qsscn | |- QQ C_ CC |
|
2 | qmulcl | |- ( ( x e. QQ /\ y e. QQ ) -> ( x x. y ) e. QQ ) |
|
3 | 1z | |- 1 e. ZZ |
|
4 | zq | |- ( 1 e. ZZ -> 1 e. QQ ) |
|
5 | 3 4 | ax-mp | |- 1 e. QQ |
6 | 1 2 5 | expcllem | |- ( ( A e. QQ /\ N e. NN0 ) -> ( A ^ N ) e. QQ ) |