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 e. RR /\ N e. ZZ /\ 0 < A ) -> 0 < ( A ^ N ) )

Proof

Step Hyp Ref Expression
1 elrp
 |-  ( A e. RR+ <-> ( A e. RR /\ 0 < A ) )
2 rpexpcl
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) e. RR+ )
3 2 rpgt0d
 |-  ( ( A e. RR+ /\ N e. ZZ ) -> 0 < ( A ^ N ) )
4 1 3 sylanbr
 |-  ( ( ( A e. RR /\ 0 < A ) /\ N e. ZZ ) -> 0 < ( A ^ N ) )
5 4 3impa
 |-  ( ( A e. RR /\ 0 < A /\ N e. ZZ ) -> 0 < ( A ^ N ) )
6 5 3com23
 |-  ( ( A e. RR /\ N e. ZZ /\ 0 < A ) -> 0 < ( A ^ N ) )