Metamath Proof Explorer


Theorem absge0i

Description: Absolute value is nonnegative. (Contributed by NM, 2-Aug-1999)

Ref Expression
Hypothesis absvalsqi.1 A
Assertion absge0i 0A

Proof

Step Hyp Ref Expression
1 absvalsqi.1 A
2 absge0 A0A
3 1 2 ax-mp 0A