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 ) )