Theorem zleltp1

Description: Integer ordering relation. (Contributed by NM, 10-May-2004)

	Ref	Expression
Assertion	zleltp1	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ 𝑀 < ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3		1re	⊢ 1 ∈ ℝ
4		leadd1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
5	3 4	mp3an3	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
6	1 2 5	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
7		peano2z	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
8		zltp1le	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝑀 < ( 𝑁 + 1 ) ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
9	7 8	sylan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < ( 𝑁 + 1 ) ↔ ( 𝑀 + 1 ) ≤ ( 𝑁 + 1 ) ) )
10	6 9	bitr4d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ 𝑀 < ( 𝑁 + 1 ) ) )