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 e. RR
nn0addge1i.2
|- N e. NN0
Assertion nn0addge2i
|- A <_ ( N + A )

Proof

Step Hyp Ref Expression
1 nn0addge1i.1
 |-  A e. RR
2 nn0addge1i.2
 |-  N e. NN0
3 nn0addge2
 |-  ( ( A e. RR /\ N e. NN0 ) -> A <_ ( N + A ) )
4 1 2 3 mp2an
 |-  A <_ ( N + A )