Metamath Proof Explorer

Theorem zleltp1

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

Ref Expression
Assertion zleltp1 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ M < N + 1

Proof

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