Metamath Proof Explorer
Description: Closure law for addition of reals, restricted to nonnegative integers.
(Contributed by Alexander van der Vekens, 6Apr2018)


Ref 
Expression 

Assertion 
nn0readdcl 
$${\u22a2}\left({A}\in {\mathbb{N}}_{0}\wedge {B}\in {\mathbb{N}}_{0}\right)\to {A}+{B}\in \mathbb{R}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nn0addcl 
$${\u22a2}\left({A}\in {\mathbb{N}}_{0}\wedge {B}\in {\mathbb{N}}_{0}\right)\to {A}+{B}\in {\mathbb{N}}_{0}$$ 
2 
1

nn0red 
$${\u22a2}\left({A}\in {\mathbb{N}}_{0}\wedge {B}\in {\mathbb{N}}_{0}\right)\to {A}+{B}\in \mathbb{R}$$ 