Metamath Proof Explorer

Theorem normge0

Description: The norm of a vector is nonnegative. (Contributed by NM, 29-May-1999) (New usage is discouraged.)

Ref Expression
Assertion normge0 A 0 norm A


Step Hyp Ref Expression
1 hiidrcl A A ih A
2 hiidge0 A 0 A ih A
3 1 2 sqrtge0d A 0 A ih A
4 normval A norm A = A ih A
5 3 4 breqtrrd A 0 norm A