Metamath Proof Explorer

Theorem nn0readdcl

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

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

Proof

Step Hyp Ref Expression
1 nn0addcl 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) e. NN0 )
2 1 nn0red 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) e. RR )