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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elrp	⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
2		rpexpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℝ+ )
3	2	rpgt0d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → 0 < ( 𝐴 ↑ 𝑁 ) )
4	1 3	sylanbr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ 𝑁 ∈ ℤ ) → 0 < ( 𝐴 ↑ 𝑁 ) )
5	4	3impa	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝑁 ∈ ℤ ) → 0 < ( 𝐴 ↑ 𝑁 ) )
6	5	3com23	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑁 ∈ ℤ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 ↑ 𝑁 ) )