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 e. ~H -> ( ( normh ` A ) = 0 <-> A = 0h ) )

Proof

Step Hyp Ref Expression
1 normgt0 
 |-  ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
2 normcl 
 |-  ( A e. ~H -> ( normh ` A ) e. RR )
3 normge0 
 |-  ( A e. ~H -> 0 <_ ( normh ` A ) )
4 0re 
 |-  0 e. RR
5 leltne 
 |-  ( ( 0 e. RR /\ ( normh ` A ) e. RR /\ 0 <_ ( normh ` A ) ) -> ( 0 < ( normh ` A ) <-> ( normh ` A ) =/= 0 ) )
6 4 5 mp3an1 
 |-  ( ( ( normh ` A ) e. RR /\ 0 <_ ( normh ` A ) ) -> ( 0 < ( normh ` A ) <-> ( normh ` A ) =/= 0 ) )
7 2 3 6 syl2anc 
 |-  ( A e. ~H -> ( 0 < ( normh ` A ) <-> ( normh ` A ) =/= 0 ) )
8 1 7 bitrd 
 |-  ( A e. ~H -> ( A =/= 0h <-> ( normh ` A ) =/= 0 ) )
9 8 necon4bid 
 |-  ( A e. ~H -> ( A = 0h <-> ( normh ` A ) = 0 ) )
10 9 bicomd 
 |-  ( A e. ~H -> ( ( normh ` A ) = 0 <-> A = 0h ) )