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 e. RR /\ N e. NN0 ) -> A <_ ( N + A ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
3 1 2 jca 
 |-  ( N e. NN0 -> ( N e. RR /\ 0 <_ N ) )
4 addge02 
 |-  ( ( A e. RR /\ N e. RR ) -> ( 0 <_ N <-> A <_ ( N + A ) ) )
5 4 biimp3a 
 |-  ( ( A e. RR /\ N e. RR /\ 0 <_ N ) -> A <_ ( N + A ) )
6 5 3expb 
 |-  ( ( A e. RR /\ ( N e. RR /\ 0 <_ N ) ) -> A <_ ( N + A ) )
7 3 6 sylan2 
 |-  ( ( A e. RR /\ N e. NN0 ) -> A <_ ( N + A ) )