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