Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BTernaryTau
Real and complex numbers
zltp1ne
Next ⟩
nnltp1ne
Metamath Proof Explorer
Ascii
Unicode
Theorem
zltp1ne
Description:
Integer ordering relation.
(Contributed by
BTernaryTau
, 24-Sep-2023)
Ref
Expression
Assertion
zltp1ne
⊢
A
∈
ℤ
∧
B
∈
ℤ
→
A
+
1
<
B
↔
A
<
B
∧
B
≠
A
+
1
Proof
Step
Hyp
Ref
Expression
1
zre
⊢
A
∈
ℤ
→
A
∈
ℝ
2
zre
⊢
B
∈
ℤ
→
B
∈
ℝ
3
peano2re
⊢
A
∈
ℝ
→
A
+
1
∈
ℝ
4
ltlen
⊢
A
+
1
∈
ℝ
∧
B
∈
ℝ
→
A
+
1
<
B
↔
A
+
1
≤
B
∧
B
≠
A
+
1
5
3
4
sylan
⊢
A
∈
ℝ
∧
B
∈
ℝ
→
A
+
1
<
B
↔
A
+
1
≤
B
∧
B
≠
A
+
1
6
1
2
5
syl2an
⊢
A
∈
ℤ
∧
B
∈
ℤ
→
A
+
1
<
B
↔
A
+
1
≤
B
∧
B
≠
A
+
1
7
zltp1le
⊢
A
∈
ℤ
∧
B
∈
ℤ
→
A
<
B
↔
A
+
1
≤
B
8
7
anbi1d
⊢
A
∈
ℤ
∧
B
∈
ℤ
→
A
<
B
∧
B
≠
A
+
1
↔
A
+
1
≤
B
∧
B
≠
A
+
1
9
6
8
bitr4d
⊢
A
∈
ℤ
∧
B
∈
ℤ
→
A
+
1
<
B
↔
A
<
B
∧
B
≠
A
+
1