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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 < 𝑁 ↔ ( 𝑀 + 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 ) ≤ 𝑁 ) )