Metamath Proof Explorer


Theorem expge0d

Description: A nonnegative real raised to a nonnegative integer is nonnegative. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses reexpcld.1 φ A
reexpcld.2 φ N 0
expge0d.3 φ 0 A
Assertion expge0d φ 0 A N

Proof

Step Hyp Ref Expression
1 reexpcld.1 φ A
2 reexpcld.2 φ N 0
3 expge0d.3 φ 0 A
4 expge0 A N 0 0 A 0 A N
5 1 2 3 4 syl3anc φ 0 A N