Metamath Proof Explorer


Theorem sqgt0i

Description: The square of a nonzero real is positive. (Contributed by NM, 17-Sep-1999)

Ref Expression
Hypothesis resqcl.1 𝐴 ∈ ℝ
Assertion sqgt0i ( 𝐴 ≠ 0 → 0 < ( 𝐴 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 resqcl.1 𝐴 ∈ ℝ
2 sqgt0 ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → 0 < ( 𝐴 ↑ 2 ) )
3 1 2 mpan ( 𝐴 ≠ 0 → 0 < ( 𝐴 ↑ 2 ) )