Metamath Proof Explorer

Theorem zlem1lt

Description: Integer ordering relation. (Contributed by NM, 13-Nov-2004)

Ref Expression
Assertion zlem1lt ⊢M∈ℤ∧N∈ℤ→M≤N↔M−1<N

Proof

Step Hyp Ref Expression
1 peano2zm ⊢M∈ℤ→M−1∈ℤ
2 zltp1le ⊢M−1∈ℤ∧N∈ℤ→M−1<N↔M-1+1≤N
3 1 2 sylan ⊢M∈ℤ∧N∈ℤ→M−1<N↔M-1+1≤N
4 zcn ⊢M∈ℤ→M∈ℂ
5 ax-1cn ⊢1∈ℂ
6 npcan ⊢M∈ℂ∧1∈ℂ→M-1+1=M
7 4 5 6 sylancl ⊢M∈ℤ→M-1+1=M
8 7 adantr ⊢M∈ℤ∧N∈ℤ→M-1+1=M
9 8 breq1d ⊢M∈ℤ∧N∈ℤ→M-1+1≤N↔M≤N
10 3 9 bitr2d ⊢M∈ℤ∧N∈ℤ→M≤N↔M−1<N