Theorem ovolge0

Description: The volume of a set is always nonnegative. (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Assertion	ovolge0	$$⊢A\subseteq ℝ\to 0\le {vol}^{*}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$$⊢\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}\subseteq {ℝ}^{*}$$
2		0xr	$$⊢0\in {ℝ}^{*}$$
3		infxrgelb	$$⊢\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}\subseteq {ℝ}^{*}\wedge 0\in {ℝ}^{*}\right)\to \left(0\le inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)\leftrightarrow \forall x\in \left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}0\le x\right)$$
4	1 2 3	mp2an	$$⊢0\le inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)\leftrightarrow \forall x\in \left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}0\le x$$
5		eqid	$$⊢\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}=\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}$$
6	5	ovolmge0	$$⊢x\in \left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\}\to 0\le x$$
7	4 6	mprgbir	$$⊢0\le inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)$$
8	5	ovolval	$$⊢A\subseteq ℝ\to {vol}^{*}\left(A\right)=inf\left(\left\{y\in {ℝ}^{*}|\exists f\in \left({\left(\le \cap {ℝ}^2\right)}^{\mathbb{N}}\right)\left(A\subseteq \bigcup \mathrm{ran}\left(\left(.\right)\circ f\right)\wedge y=sup\left(\mathrm{ran}seq1\left(+,\left(\left(\mathrm{abs}\circ -\right)\circ f\right)\right),{ℝ}^{*},<\right)\right)\right\},{ℝ}^{*},<\right)$$
9	7 8	breqtrrid	$$⊢A\subseteq ℝ\to 0\le {vol}^{*}\left(A\right)$$