Metamath Proof Explorer

Theorem eluzp1m1

Description: Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005)

Ref Expression
Assertion eluzp1m1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → N − 1 ∈ ℤ ≥ M

Proof

Step Hyp Ref Expression
1 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
2 1 ad2antrl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M + 1 ≤ N → N − 1 ∈ ℤ
3 zre ⊢ M ∈ ℤ → M ∈ ℝ
4 zre ⊢ N ∈ ℤ → N ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 leaddsub ⊢ M ∈ ℝ ∧ 1 ∈ ℝ ∧ N ∈ ℝ → M + 1 ≤ N ↔ M ≤ N − 1
7 5 6 mp3an2 ⊢ M ∈ ℝ ∧ N ∈ ℝ → M + 1 ≤ N ↔ M ≤ N − 1
8 3 4 7 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M + 1 ≤ N ↔ M ≤ N − 1
9 8 biimpa ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M + 1 ≤ N → M ≤ N − 1
10 9 anasss ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M + 1 ≤ N → M ≤ N − 1
11 2 10 jca ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M + 1 ≤ N → N − 1 ∈ ℤ ∧ M ≤ N − 1
12 11 ex ⊢ M ∈ ℤ → N ∈ ℤ ∧ M + 1 ≤ N → N − 1 ∈ ℤ ∧ M ≤ N − 1
13 peano2z ⊢ M ∈ ℤ → M + 1 ∈ ℤ
14 eluz1 ⊢ M + 1 ∈ ℤ → N ∈ ℤ ≥ M + 1 ↔ N ∈ ℤ ∧ M + 1 ≤ N
15 13 14 syl ⊢ M ∈ ℤ → N ∈ ℤ ≥ M + 1 ↔ N ∈ ℤ ∧ M + 1 ≤ N
16 eluz1 ⊢ M ∈ ℤ → N − 1 ∈ ℤ ≥ M ↔ N − 1 ∈ ℤ ∧ M ≤ N − 1
17 12 15 16 3imtr4d ⊢ M ∈ ℤ → N ∈ ℤ ≥ M + 1 → N − 1 ∈ ℤ ≥ M
18 17 imp ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → N − 1 ∈ ℤ ≥ M