Theorem norm-i

Description: Theorem 3.3(i) of Beran p. 97. (Contributed by NM, 29-Jul-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	norm-i	$$⊢A\in \mathscr{H}\to \left({norm}_{ℎ}\left(A\right)=0\leftrightarrow A=0_{ℎ}\right)$$

Proof

Step	Hyp	Ref	Expression
1		normgt0	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\leftrightarrow 0<{norm}_{ℎ}\left(A\right)\right)$$
2		normcl	$$⊢A\in \mathscr{H}\to {norm}_{ℎ}\left(A\right)\in ℝ$$
3		normge0	$$⊢A\in \mathscr{H}\to 0\le {norm}_{ℎ}\left(A\right)$$
4		0re	$$⊢0\in ℝ$$
5		leltne	$$⊢\left(0\in ℝ\wedge {norm}_{ℎ}\left(A\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left(A\right)\right)\to \left(0<{norm}_{ℎ}\left(A\right)\leftrightarrow {norm}_{ℎ}\left(A\right)\ne 0\right)$$
6	4 5	mp3an1	$$⊢\left({norm}_{ℎ}\left(A\right)\in ℝ\wedge 0\le {norm}_{ℎ}\left(A\right)\right)\to \left(0<{norm}_{ℎ}\left(A\right)\leftrightarrow {norm}_{ℎ}\left(A\right)\ne 0\right)$$
7	2 3 6	syl2anc	$$⊢A\in \mathscr{H}\to \left(0<{norm}_{ℎ}\left(A\right)\leftrightarrow {norm}_{ℎ}\left(A\right)\ne 0\right)$$
8	1 7	bitrd	$$⊢A\in \mathscr{H}\to \left(A\ne 0_{ℎ}\leftrightarrow {norm}_{ℎ}\left(A\right)\ne 0\right)$$
9	8	necon4bid	$$⊢A\in \mathscr{H}\to \left(A=0_{ℎ}\leftrightarrow {norm}_{ℎ}\left(A\right)=0\right)$$
10	9	bicomd	$$⊢A\in \mathscr{H}\to \left({norm}_{ℎ}\left(A\right)=0\leftrightarrow A=0_{ℎ}\right)$$