Theorem zltp1ne

Description: Integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023)

	Ref	Expression
Assertion	zltp1ne	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
2		zre	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
3		peano2re	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
4		ltlen	⊢ ( ( ( 𝐴 + 1 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( ( 𝐴 + 1 ) ≤ 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) )
5	3 4	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( ( 𝐴 + 1 ) ≤ 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) )
6	1 2 5	syl2an	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( ( 𝐴 + 1 ) ≤ 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) )
7		zltp1le	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 < 𝐵 ↔ ( 𝐴 + 1 ) ≤ 𝐵 ) )
8	7	anbi1d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ↔ ( ( 𝐴 + 1 ) ≤ 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) )
9	6 8	bitr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 1 ) < 𝐵 ↔ ( 𝐴 < 𝐵 ∧ 𝐵 ≠ ( 𝐴 + 1 ) ) ) )