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