# Metamath Proof Explorer

## 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 ℋ\to \left({norm}_{ℎ}\left({A}\right)=0↔{A}={0}_{ℎ}\right)$

### Proof

Step Hyp Ref Expression
1 normgt0 ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}↔0<{norm}_{ℎ}\left({A}\right)\right)$
2 normcl ${⊢}{A}\in ℋ\to {norm}_{ℎ}\left({A}\right)\in ℝ$
3 normge0 ${⊢}{A}\in ℋ\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)↔{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)↔{norm}_{ℎ}\left({A}\right)\ne 0\right)$
7 2 3 6 syl2anc ${⊢}{A}\in ℋ\to \left(0<{norm}_{ℎ}\left({A}\right)↔{norm}_{ℎ}\left({A}\right)\ne 0\right)$
8 1 7 bitrd ${⊢}{A}\in ℋ\to \left({A}\ne {0}_{ℎ}↔{norm}_{ℎ}\left({A}\right)\ne 0\right)$
9 8 necon4bid ${⊢}{A}\in ℋ\to \left({A}={0}_{ℎ}↔{norm}_{ℎ}\left({A}\right)=0\right)$
10 9 bicomd ${⊢}{A}\in ℋ\to \left({norm}_{ℎ}\left({A}\right)=0↔{A}={0}_{ℎ}\right)$