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 𝐴 ∈ ℋ
Assertion normcli ( norm𝐴 ) ∈ ℝ

Proof

Step Hyp Ref Expression
1 normcl.1 𝐴 ∈ ℋ
2 normcl ( 𝐴 ∈ ℋ → ( norm𝐴 ) ∈ ℝ )
3 1 2 ax-mp ( norm𝐴 ) ∈ ℝ