Metamath Proof Explorer


Theorem nn0addge2

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

Ref Expression
Assertion nn0addge2 A N 0 A N + A

Proof

Step Hyp Ref Expression
1 nn0re N 0 N
2 nn0ge0 N 0 0 N
3 1 2 jca N 0 N 0 N
4 addge02 A N 0 N A N + A
5 4 biimp3a A N 0 N A N + A
6 5 3expb A N 0 N A N + A
7 3 6 sylan2 A N 0 A N + A