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 e. ~H -> 0 <_ ( normh ` A ) )

Proof

Step	Hyp	Ref	Expression
1		hiidrcl	|- ( A e. ~H -> ( A .ih A ) e. RR )
2		hiidge0	|- ( A e. ~H -> 0 <_ ( A .ih A ) )
3	1 2	sqrtge0d	|- ( A e. ~H -> 0 <_ ( sqrt ` ( A .ih A ) ) )
4		normval	|- ( A e. ~H -> ( normh ` A ) = ( sqrt ` ( A .ih A ) ) )
5	3 4	breqtrrd	|- ( A e. ~H -> 0 <_ ( normh ` A ) )