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 A
Assertion sqgt0i A 0 0 < A 2

Proof

Step Hyp Ref Expression
1 resqcl.1 A
2 sqgt0 A A 0 0 < A 2
3 1 2 mpan A 0 0 < A 2