Metamath Proof Explorer

Theorem nn0resubcl

Description: Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018)

Ref Expression
Assertion nn0resubcl 
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A - B ) e. RR )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( A e. NN0 -> A e. RR )
2 nn0re 
 |-  ( B e. NN0 -> B e. RR )
3 resubcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. RR )
4 1 2 3 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A - B ) e. RR )