Metamath Proof Explorer

Theorem ltp1i

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

Ref Expression
Hypothesis ltplus1.1 
|- A e. RR
Assertion ltp1i 
|- A < ( A + 1 )

Proof

Step Hyp Ref Expression
1 ltplus1.1 
 |-  A e. RR
2 ltp1 
 |-  ( A e. RR -> A < ( A + 1 ) )
3 1 2 ax-mp 
 |-  A < ( A + 1 )