Theorem zlem1lt

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

	Ref	Expression
Assertion	zlem1lt	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≤ 𝑁 ↔ ( 𝑀 − 1 ) < 𝑁 ) )

Proof

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