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