Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BTernaryTau
nnltp1ne
Next ⟩
nn0ltp1ne
Metamath Proof Explorer
Ascii
Unicode
Theorem
nnltp1ne
Description:
Positive integer ordering relation.
(Contributed by
BTernaryTau
, 24-Sep-2023)
Ref
Expression
Assertion
nnltp1ne
⊢
A
∈
ℕ
∧
B
∈
ℕ
→
A
+
1
<
B
↔
A
<
B
∧
B
≠
A
+
1
Proof
Step
Hyp
Ref
Expression
1
nnz
⊢
A
∈
ℕ
→
A
∈
ℤ
2
nnz
⊢
B
∈
ℕ
→
B
∈
ℤ
3
zltp1ne
⊢
A
∈
ℤ
∧
B
∈
ℤ
→
A
+
1
<
B
↔
A
<
B
∧
B
≠
A
+
1
4
1
2
3
syl2an
⊢
A
∈
ℕ
∧
B
∈
ℕ
→
A
+
1
<
B
↔
A
<
B
∧
B
≠
A
+
1