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 ∈ ℋ → norm ℎ ⁡ A = 0 ↔ A = 0 ℎ

Proof

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