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