Theorem ovolre

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

	Ref	Expression
Assertion	ovolre	⊢ ( vol* ‘ ℝ ) = +∞

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ℝ ⊆ ℝ
2		ovolcl	⊢ ( ℝ ⊆ ℝ → ( vol* ‘ ℝ ) ∈ ℝ* )
3	1 2	ax-mp	⊢ ( vol* ‘ ℝ ) ∈ ℝ*
4		pnfge	⊢ ( ( vol* ‘ ℝ ) ∈ ℝ* → ( vol* ‘ ℝ ) ≤ +∞ )
5	3 4	ax-mp	⊢ ( vol* ‘ ℝ ) ≤ +∞
6		0re	⊢ 0 ∈ ℝ
7		ovolicopnf	⊢ ( 0 ∈ ℝ → ( vol* ‘ ( 0 [,) +∞ ) ) = +∞ )
8	6 7	ax-mp	⊢ ( vol* ‘ ( 0 [,) +∞ ) ) = +∞
9		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
10		ovolss	⊢ ( ( ( 0 [,) +∞ ) ⊆ ℝ ∧ ℝ ⊆ ℝ ) → ( vol* ‘ ( 0 [,) +∞ ) ) ≤ ( vol* ‘ ℝ ) )
11	9 1 10	mp2an	⊢ ( vol* ‘ ( 0 [,) +∞ ) ) ≤ ( vol* ‘ ℝ )
12	8 11	eqbrtrri	⊢ +∞ ≤ ( vol* ‘ ℝ )
13		pnfxr	⊢ +∞ ∈ ℝ*
14		xrletri3	⊢ ( ( ( vol* ‘ ℝ ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( vol* ‘ ℝ ) = +∞ ↔ ( ( vol* ‘ ℝ ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ℝ ) ) ) )
15	3 13 14	mp2an	⊢ ( ( vol* ‘ ℝ ) = +∞ ↔ ( ( vol* ‘ ℝ ) ≤ +∞ ∧ +∞ ≤ ( vol* ‘ ℝ ) ) )
16	5 12 15	mpbir2an	⊢ ( vol* ‘ ℝ ) = +∞