This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )

Proof

Step Hyp Ref Expression
1 normgt0 ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ 0 < ( normℎ ‘ 𝐴 ) ) )
2 normcl ⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ 𝐴 ) ∈ ℝ )
3 normge0 ⊢ ( 𝐴 ∈ ℋ → 0 ≤ ( normℎ ‘ 𝐴 ) )
4 0re ⊢ 0 ∈ ℝ
5 leltne ⊢ ( ( 0 ∈ ℝ ∧ ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝐴 ) ) → ( 0 < ( normℎ ‘ 𝐴 ) ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
6 4 5 mp3an1 ⊢ ( ( ( normℎ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( normℎ ‘ 𝐴 ) ) → ( 0 < ( normℎ ‘ 𝐴 ) ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
7 2 3 6 syl2anc ⊢ ( 𝐴 ∈ ℋ → ( 0 < ( normℎ ‘ 𝐴 ) ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
8 1 7 bitrd ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 ≠ 0ℎ ↔ ( normℎ ‘ 𝐴 ) ≠ 0 ) )
9 8 necon4bid ⊢ ( 𝐴 ∈ ℋ → ( 𝐴 = 0ℎ ↔ ( normℎ ‘ 𝐴 ) = 0 ) )
10 9 bicomd ⊢ ( 𝐴 ∈ ℋ → ( ( normℎ ‘ 𝐴 ) = 0 ↔ 𝐴 = 0ℎ ) )