Theorem expgt0

Description: Nonnegative integer exponentiation with a positive mantissa is positive. (Contributed by NM, 16-Dec-2005) (Revised by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expgt0	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\wedge 0<A\right)\to 0<A^N$$

Proof

Step	Hyp	Ref	Expression
1		elrp	$$⊢A\in {ℝ}^{+}\leftrightarrow \left(A\in ℝ\wedge 0<A\right)$$
2		rpexpcl	$$⊢\left(A\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to A^N\in {ℝ}^{+}$$
3	2	rpgt0d	$$⊢\left(A\in {ℝ}^{+}\wedge N\in \mathbb{Z}\right)\to 0<A^N$$
4	1 3	sylanbr	$$⊢\left(\left(A\in ℝ\wedge 0<A\right)\wedge N\in \mathbb{Z}\right)\to 0<A^N$$
5	4	3impa	$$⊢\left(A\in ℝ\wedge 0<A\wedge N\in \mathbb{Z}\right)\to 0<A^N$$
6	5	3com23	$$⊢\left(A\in ℝ\wedge N\in \mathbb{Z}\wedge 0<A\right)\to 0<A^N$$