Theorem measge0

Description: A measure is nonnegative. (Contributed by Thierry Arnoux, 9-Mar-2018)

	Ref	Expression
Assertion	measge0	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge A\in S\right)\to 0\le M\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		measvxrge0	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge A\in S\right)\to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
2		elxrge0	$$⊢M\left(A\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(M\left(A\right)\in {ℝ}^{*}\wedge 0\le M\left(A\right)\right)$$
3	1 2	sylib	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge A\in S\right)\to \left(M\left(A\right)\in {ℝ}^{*}\wedge 0\le M\left(A\right)\right)$$
4	3	simprd	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge A\in S\right)\to 0\le M\left(A\right)$$