# 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 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}↔{M}+1\le {N}\right)$

### Proof

Step Hyp Ref Expression
1 nnge1 ${⊢}{N}-{M}\in ℕ\to 1\le {N}-{M}$
2 1 a1i ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({N}-{M}\in ℕ\to 1\le {N}-{M}\right)$
3 znnsub ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}↔{N}-{M}\in ℕ\right)$
4 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
5 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
6 1re ${⊢}1\in ℝ$
7 leaddsub2 ${⊢}\left({M}\in ℝ\wedge 1\in ℝ\wedge {N}\in ℝ\right)\to \left({M}+1\le {N}↔1\le {N}-{M}\right)$
8 6 7 mp3an2 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\right)\to \left({M}+1\le {N}↔1\le {N}-{M}\right)$
9 4 5 8 syl2an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}+1\le {N}↔1\le {N}-{M}\right)$
10 2 3 9 3imtr4d ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}\to {M}+1\le {N}\right)$
11 4 adantr ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}\in ℝ$
12 11 ltp1d ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}<{M}+1$
13 peano2re ${⊢}{M}\in ℝ\to {M}+1\in ℝ$
14 11 13 syl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}+1\in ℝ$
15 5 adantl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {N}\in ℝ$
16 ltletr ${⊢}\left({M}\in ℝ\wedge {M}+1\in ℝ\wedge {N}\in ℝ\right)\to \left(\left({M}<{M}+1\wedge {M}+1\le {N}\right)\to {M}<{N}\right)$
17 11 14 15 16 syl3anc ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({M}<{M}+1\wedge {M}+1\le {N}\right)\to {M}<{N}\right)$
18 12 17 mpand ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}+1\le {N}\to {M}<{N}\right)$
19 10 18 impbid ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}<{N}↔{M}+1\le {N}\right)$