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