Theorem ovolq

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

	Ref	Expression
Assertion	ovolq	⊢ ( vol* ‘ ℚ ) = 0

Proof

Step	Hyp	Ref	Expression
1		qssre	⊢ ℚ ⊆ ℝ
2		qnnen	⊢ ℚ ≈ ℕ
3		ovolctb	⊢ ( ( ℚ ⊆ ℝ ∧ ℚ ≈ ℕ ) → ( vol* ‘ ℚ ) = 0 )
4	1 2 3	mp2an	⊢ ( vol* ‘ ℚ ) = 0