Metamath Proof Explorer

Theorem reexpclzd

Description: Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses rpexpclzd.1 φ A
rpexpclzd.2 φ A 0
rpexpclzd.3 φ N
Assertion reexpclzd φ A N


Step Hyp Ref Expression
1 rpexpclzd.1 φ A
2 rpexpclzd.2 φ A 0
3 rpexpclzd.3 φ N
4 reexpclz A A 0 N A N
5 1 2 3 4 syl3anc φ A N