Metamath Proof Explorer


Theorem expgt0

Description: A positive real raised to an integer power is positive. (Contributed by NM, 16-Dec-2005) (Revised by Mario Carneiro, 4-Jun-2014)

Ref Expression
Assertion expgt0 A N 0 < A 0 < A N

Proof

Step Hyp Ref Expression
1 elrp A + A 0 < A
2 rpexpcl A + N A N +
3 2 rpgt0d A + N 0 < A N
4 1 3 sylanbr A 0 < A N 0 < A N
5 4 3impa A 0 < A N 0 < A N
6 5 3com23 A N 0 < A 0 < A N