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=\mathrm{AbsVal}\left(R\right)$$
	abvf.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	abvge0	$$⊢\left(F\in A\wedge X\in B\right)\to 0\le F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		abvf.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvf.b	$$⊢B={\mathrm{Base}}_R$$
3	1 2	abvfge0	$$⊢F\in A\to F:B⟶\left[0,\mathrm{+\infty }\right)$$
4	3	ffvelcdmda	$$⊢\left(F\in A\wedge X\in B\right)\to F\left(X\right)\in \left[0,\mathrm{+\infty }\right)$$
5		elrege0	$$⊢F\left(X\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(F\left(X\right)\in ℝ\wedge 0\le F\left(X\right)\right)$$
6	5	simprbi	$$⊢F\left(X\right)\in \left[0,\mathrm{+\infty }\right)\to 0\le F\left(X\right)$$
7	4 6	syl	$$⊢\left(F\in A\wedge X\in B\right)\to 0\le F\left(X\right)$$