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
Assertion ltp1i A < A + 1

Proof

Step Hyp Ref Expression
1 ltplus1.1 A
2 ltp1 A A < A + 1
3 1 2 ax-mp A < A + 1