Metamath Proof Explorer

Theorem zltlem1

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

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

Proof

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