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	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A-B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		nn0re	$$⊢A\in {\mathbb{N}}_0\to A\in ℝ$$
2		nn0re	$$⊢B\in {\mathbb{N}}_0\to B\in ℝ$$
3		resubcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to A-B\in ℝ$$
4	1 2 3	syl2an	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in {\mathbb{N}}_0\right)\to A-B\in ℝ$$