Description: A number is less than or equal to itself plus 1. (Contributed by NM, 5-Jan-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | lep1 | |- ( A e. RR -> A <_ ( A + 1 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltp1 | |- ( A e. RR -> A < ( A + 1 ) ) |
|
2 | peano2re | |- ( A e. RR -> ( A + 1 ) e. RR ) |
|
3 | ltle | |- ( ( A e. RR /\ ( A + 1 ) e. RR ) -> ( A < ( A + 1 ) -> A <_ ( A + 1 ) ) ) |
|
4 | 2 3 | mpdan | |- ( A e. RR -> ( A < ( A + 1 ) -> A <_ ( A + 1 ) ) ) |
5 | 1 4 | mpd | |- ( A e. RR -> A <_ ( A + 1 ) ) |