Metamath Proof Explorer

Theorem eluzp1p1

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

Ref Expression
Assertion eluzp1p1 ⊢ N ∈ ℤ ≥ M → N + 1 ∈ ℤ ≥ M + 1

Proof

Step Hyp Ref Expression
1 peano2z ⊢ M ∈ ℤ → M + 1 ∈ ℤ
2 1 3ad2ant1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → M + 1 ∈ ℤ
3 peano2z ⊢ N ∈ ℤ → N + 1 ∈ ℤ
4 3 3ad2ant2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → N + 1 ∈ ℤ
5 zre ⊢ M ∈ ℤ → M ∈ ℝ
6 zre ⊢ N ∈ ℤ → N ∈ ℝ
7 1re ⊢ 1 ∈ ℝ
8 leadd1 ⊢ M ∈ ℝ ∧ N ∈ ℝ ∧ 1 ∈ ℝ → M ≤ N ↔ M + 1 ≤ N + 1
9 7 8 mp3an3 ⊢ M ∈ ℝ ∧ N ∈ ℝ → M ≤ N ↔ M + 1 ≤ N + 1
10 5 6 9 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M ≤ N ↔ M + 1 ≤ N + 1
11 10 biimp3a ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → M + 1 ≤ N + 1
12 2 4 11 3jca ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → M + 1 ∈ ℤ ∧ N + 1 ∈ ℤ ∧ M + 1 ≤ N + 1
13 eluz2 ⊢ N ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N
14 eluz2 ⊢ N + 1 ∈ ℤ ≥ M + 1 ↔ M + 1 ∈ ℤ ∧ N + 1 ∈ ℤ ∧ M + 1 ≤ N + 1
15 12 13 14 3imtr4i ⊢ N ∈ ℤ ≥ M → N + 1 ∈ ℤ ≥ M + 1