Theorem zltp1le

Description: Integer ordering relation. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		nnge1	⊢ ( ( 𝑁 − 𝑀 ) ∈ ℕ → 1 ≤ ( 𝑁 − 𝑀 ) )
2	1	a1i	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 − 𝑀 ) ∈ ℕ → 1 ≤ ( 𝑁 − 𝑀 ) ) )
3		znnsub	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑁 − 𝑀 ) ∈ ℕ ) )
4		zre	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
5		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6		1re	⊢ 1 ∈ ℝ
7		leaddsub2	⊢ ( ( 𝑀 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ 1 ≤ ( 𝑁 − 𝑀 ) ) )
8	6 7	mp3an2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ 1 ≤ ( 𝑁 − 𝑀 ) ) )
9	4 5 8	syl2an	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 ↔ 1 ≤ ( 𝑁 − 𝑀 ) ) )
10	2 3 9	3imtr4d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 → ( 𝑀 + 1 ) ≤ 𝑁 ) )
11	4	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℝ )
12	11	ltp1d	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 < ( 𝑀 + 1 ) )
13		peano2re	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ )
14	11 13	syl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 1 ) ∈ ℝ )
15	5	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
16		ltletr	⊢ ( ( 𝑀 ∈ ℝ ∧ ( 𝑀 + 1 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝑀 < ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → 𝑀 < 𝑁 ) )
17	11 14 15 16	syl3anc	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 < ( 𝑀 + 1 ) ∧ ( 𝑀 + 1 ) ≤ 𝑁 ) → 𝑀 < 𝑁 ) )
18	12 17	mpand	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 + 1 ) ≤ 𝑁 → 𝑀 < 𝑁 ) )
19	10 18	impbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 1 ) ≤ 𝑁 ) )