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 0 B 0 A B

Proof

Step Hyp Ref Expression
1 nn0re A 0 A
2 nn0re B 0 B
3 resubcl A B A B
4 1 2 3 syl2an A 0 B 0 A B