Metamath Proof Explorer


Theorem nn0addge2i

Description: A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005)

Ref Expression
Hypotheses nn0addge1i.1 A
nn0addge1i.2 N0
Assertion nn0addge2i AN+A

Proof

Step Hyp Ref Expression
1 nn0addge1i.1 A
2 nn0addge1i.2 N0
3 nn0addge2 AN0AN+A
4 1 2 3 mp2an AN+A