Metamath Proof Explorer

Theorem zltp1le

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

Ref Expression
Assertion zltp1le ⊢M∈ℤ∧N∈ℤ→M<N↔M+1≤N

Proof

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