Metamath Proof Explorer

Theorem peano2uz

Description: Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → M ∈ ℤ
2 peano2z ⊢ N ∈ ℤ → N + 1 ∈ ℤ
3 2 3ad2ant2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → N + 1 ∈ ℤ
4 zre ⊢ M ∈ ℤ → M ∈ ℝ
5 zre ⊢ N ∈ ℤ → N ∈ ℝ
6 letrp1 ⊢ M ∈ ℝ ∧ N ∈ ℝ ∧ M ≤ N → M ≤ N + 1
7 5 6 syl3an2 ⊢ M ∈ ℝ ∧ N ∈ ℤ ∧ M ≤ N → M ≤ N + 1
8 4 7 syl3an1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → M ≤ N + 1
9 1 3 8 3jca ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N → M ∈ ℤ ∧ N + 1 ∈ ℤ ∧ M ≤ N + 1
10 eluz2 ⊢ N ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N
11 eluz2 ⊢ N + 1 ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ N + 1 ∈ ℤ ∧ M ≤ N + 1
12 9 10 11 3imtr4i ⊢ N ∈ ℤ ≥ M → N + 1 ∈ ℤ ≥ M