Metamath Proof Explorer


Theorem sqn0rp

Description: The square of a nonzero real is a positive real. (Contributed by AV, 5-Mar-2023)

Ref Expression
Assertion sqn0rp A A 0 A 2 +

Proof

Step Hyp Ref Expression
1 resqcl A A 2
2 1 adantr A A 0 A 2
3 sqgt0 A A 0 0 < A 2
4 2 3 elrpd A A 0 A 2 +