Metamath Proof Explorer


Theorem nn0addge1i

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 N 0
Assertion nn0addge1i A A + N

Proof

Step Hyp Ref Expression
1 nn0addge1i.1 A
2 nn0addge1i.2 N 0
3 nn0addge1 A N 0 A A + N
4 1 2 3 mp2an A A + N