Theorem abvge0

Description: The absolute value of a number is greater than or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		abvf.a	|- A = ( AbsVal ` R )
2		abvf.b	|- B = ( Base ` R )
3	1 2	abvfge0	|- ( F e. A -> F : B --> ( 0 [,) +oo ) )
4	3	ffvelrnda	|- ( ( F e. A /\ X e. B ) -> ( F ` X ) e. ( 0 [,) +oo ) )
5		elrege0	|- ( ( F ` X ) e. ( 0 [,) +oo ) <-> ( ( F ` X ) e. RR /\ 0 <_ ( F ` X ) ) )
6	5	simprbi	|- ( ( F ` X ) e. ( 0 [,) +oo ) -> 0 <_ ( F ` X ) )
7	4 6	syl	|- ( ( F e. A /\ X e. B ) -> 0 <_ ( F ` X ) )