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\in \mathscr{H}$$
Assertion	normcli	$$⊢{norm}_{ℎ}\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		normcl.1	$$⊢A\in \mathscr{H}$$
2		normcl	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)\in ℝ$$
3	1 2	ax-mp	$$⊢{norm}_{ℎ}\left(A\right)\in ℝ$$