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 ) )