Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Ordering on reals (cont.)
ltp1i
Next ⟩
recgt0i
Metamath Proof Explorer
Ascii
Unicode
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