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* ` QQ ) = 0

Proof

Step Hyp Ref Expression
1 qssre 
 |-  QQ C_ RR
2 qnnen 
 |-  QQ ~~ NN
3 ovolctb 
 |-  ( ( QQ C_ RR /\ QQ ~~ NN ) -> ( vol* ` QQ ) = 0 )
4 1 2 3 mp2an 
 |-  ( vol* ` QQ ) = 0