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

Metamath Proof Explorer

Theorem abvgt0

Description: The absolute value of a nonzero number is strictly positive. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvf.a 
|- A = ( AbsVal ` R )
abvf.b 
|- B = ( Base ` R )
abveq0.z 
|- .0. = ( 0g ` R )
Assertion abvgt0 
|- ( ( F e. A /\ X e. B /\ X =/= .0. ) -> 0 < ( F ` X ) )

Proof

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 abvcl 
 |-  ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )
5 4 3adant3 
 |-  ( ( F e. A /\ X e. B /\ X =/= .0. ) -> ( F ` X ) e. RR )
6 1 2 abvge0 
 |-  ( ( F e. A /\ X e. B ) -> 0 <_ ( F ` X ) )
7 6 3adant3 
 |-  ( ( F e. A /\ X e. B /\ X =/= .0. ) -> 0 <_ ( F ` X ) )
8 1 2 3 abvne0 
 |-  ( ( F e. A /\ X e. B /\ X =/= .0. ) -> ( F ` X ) =/= 0 )
9 5 7 8 ne0gt0d 
 |-  ( ( F e. A /\ X e. B /\ X =/= .0. ) -> 0 < ( F ` X ) )