This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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