Metamath Proof Explorer


Theorem sqgt0

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

Ref Expression
Assertion sqgt0 A A 0 0 < A 2

Proof

Step Hyp Ref Expression
1 msqgt0 A A 0 0 < A A
2 recn A A
3 sqval A A 2 = A A
4 2 3 syl A A 2 = A A
5 4 adantr A A 0 A 2 = A A
6 1 5 breqtrrd A A 0 0 < A 2