Metamath Proof Explorer

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