This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolq

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

		Ref	Expression
	Assertion	ovolq	$⊢ {vol}^{*} (ℚ) = 0$

Step	Hyp	Ref	Expression
1		qssre	$⊢ ℚ \subseteq ℝ$
2		qnnen	$⊢ ℚ \approx ℕ$
3		ovolctb	$⊢ (ℚ \subseteq ℝ \land ℚ \approx ℕ) \to {vol}^{*} (ℚ) = 0$
4	1 2 3	mp2an	$⊢ {vol}^{*} (ℚ) = 0$