Database
REAL AND COMPLEX NUMBERS
Integer sets
Integers (as a subset of complex numbers)
nn0leltp1
Next ⟩
nn0ltlem1
Metamath Proof Explorer
Ascii
Unicode
Theorem
nn0leltp1
Description:
Nonnegative integer ordering relation.
(Contributed by
Raph Levien
, 10-Apr-2004)
Ref
Expression
Assertion
nn0leltp1
⊢
M
∈
ℕ
0
∧
N
∈
ℕ
0
→
M
≤
N
↔
M
<
N
+
1
Proof
Step
Hyp
Ref
Expression
1
nn0z
⊢
M
∈
ℕ
0
→
M
∈
ℤ
2
nn0z
⊢
N
∈
ℕ
0
→
N
∈
ℤ
3
zleltp1
⊢
M
∈
ℤ
∧
N
∈
ℤ
→
M
≤
N
↔
M
<
N
+
1
4
1
2
3
syl2an
⊢
M
∈
ℕ
0
∧
N
∈
ℕ
0
→
M
≤
N
↔
M
<
N
+
1