Description: The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8Sep2014)
Ref  Expression  

Hypotheses  abvf.a   A = ( AbsVal ` R ) 

abvf.b   B = ( Base ` R ) 

abveq0.z   .0. = ( 0g ` R ) 

Assertion  abvne0   ( ( F e. A /\ X e. B /\ X =/= .0. ) > ( F ` X ) =/= 0 ) 
Step  Hyp  Ref  Expression 

1  abvf.a   A = ( AbsVal ` R ) 

2  abvf.b   B = ( Base ` R ) 

3  abveq0.z   .0. = ( 0g ` R ) 

4  1 2 3  abveq0   ( ( F e. A /\ X e. B ) > ( ( F ` X ) = 0 <> X = .0. ) ) 
5  4  necon3bid   ( ( F e. A /\ X e. B ) > ( ( F ` X ) =/= 0 <> X =/= .0. ) ) 
6  5  biimp3ar   ( ( F e. A /\ X e. B /\ X =/= .0. ) > ( F ` X ) =/= 0 ) 