Metamath Proof Explorer

Theorem ltp1

Description: A number is less than itself plus 1. (Contributed by NM, 20-Aug-2001)

Ref Expression
Assertion ltp1 
|- ( A e. RR -> A < ( A + 1 ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 0lt1 
 |-  0 < 1
3 ltaddpos 
 |-  ( ( 1 e. RR /\ A e. RR ) -> ( 0 < 1 <-> A < ( A + 1 ) ) )
4 2 3 mpbii 
 |-  ( ( 1 e. RR /\ A e. RR ) -> A < ( A + 1 ) )
5 1 4 mpan 
 |-  ( A e. RR -> A < ( A + 1 ) )