Metamath Proof Explorer


Theorem normcli

Description: Real closure of the norm of a vector. (Contributed by NM, 30-Sep-1999) (New usage is discouraged.)

Ref Expression
Hypothesis normcl.1
|- A e. ~H
Assertion normcli
|- ( normh ` A ) e. RR

Proof

Step Hyp Ref Expression
1 normcl.1
 |-  A e. ~H
2 normcl
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
3 1 2 ax-mp
 |-  ( normh ` A ) e. RR