Theorem ovolq

Description: The rational numbers have 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014)

	Ref	Expression
Assertion	ovolq	$$⊢{vol}^{*}\left(\mathbb{Q}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
2		qnnen	$$⊢\mathbb{Q}\approx \mathbb{N}$$
3		ovolctb	$$⊢\left(\mathbb{Q}\subseteq ℝ\wedge \mathbb{Q}\approx \mathbb{N}\right)\to {vol}^{*}\left(\mathbb{Q}\right)=0$$
4	1 2 3	mp2an	$$⊢{vol}^{*}\left(\mathbb{Q}\right)=0$$