Theorem ovolre

Description: The measure of the real numbers. (Contributed by Mario Carneiro, 14-Jun-2014)

	Ref	Expression
Assertion	ovolre	$$⊢{vol}^{*}\left(ℝ\right)=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢ℝ\subseteq ℝ$$
2		ovolcl	$$⊢ℝ\subseteq ℝ\to {vol}^{*}\left(ℝ\right)\in {ℝ}^{*}$$
3	1 2	ax-mp	$$⊢{vol}^{*}\left(ℝ\right)\in {ℝ}^{*}$$
4		pnfge	$$⊢{vol}^{*}\left(ℝ\right)\in {ℝ}^{*}\to {vol}^{*}\left(ℝ\right)\le \mathrm{+\infty }$$
5	3 4	ax-mp	$$⊢{vol}^{*}\left(ℝ\right)\le \mathrm{+\infty }$$
6		0re	$$⊢0\in ℝ$$
7		ovolicopnf	$$⊢0\in ℝ\to {vol}^{*}\left(\left[0,\mathrm{+\infty }\right)\right)=\mathrm{+\infty }$$
8	6 7	ax-mp	$$⊢{vol}^{*}\left(\left[0,\mathrm{+\infty }\right)\right)=\mathrm{+\infty }$$
9		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
10		ovolss	$$⊢\left(\left[0,\mathrm{+\infty }\right)\subseteq ℝ\wedge ℝ\subseteq ℝ\right)\to {vol}^{*}\left(\left[0,\mathrm{+\infty }\right)\right)\le {vol}^{*}\left(ℝ\right)$$
11	9 1 10	mp2an	$$⊢{vol}^{*}\left(\left[0,\mathrm{+\infty }\right)\right)\le {vol}^{*}\left(ℝ\right)$$
12	8 11	eqbrtrri	$$⊢\mathrm{+\infty }\le {vol}^{*}\left(ℝ\right)$$
13		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
14		xrletri3	$$⊢\left({vol}^{*}\left(ℝ\right)\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left({vol}^{*}\left(ℝ\right)=\mathrm{+\infty }\leftrightarrow \left({vol}^{*}\left(ℝ\right)\le \mathrm{+\infty }\wedge \mathrm{+\infty }\le {vol}^{*}\left(ℝ\right)\right)\right)$$
15	3 13 14	mp2an	$$⊢{vol}^{*}\left(ℝ\right)=\mathrm{+\infty }\leftrightarrow \left({vol}^{*}\left(ℝ\right)\le \mathrm{+\infty }\wedge \mathrm{+\infty }\le {vol}^{*}\left(ℝ\right)\right)$$
16	5 12 15	mpbir2an	$$⊢{vol}^{*}\left(ℝ\right)=\mathrm{+\infty }$$