Metamath Proof Explorer


Theorem reexpcl

Description: Closure of exponentiation of reals. (Contributed by NM, 14-Dec-2005)

Ref Expression
Assertion reexpcl AN0AN

Proof

Step Hyp Ref Expression
1 ax-resscn
2 remulcl xyxy
3 1re 1
4 1 2 3 expcllem AN0AN