# 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}\in {ℤ}_{\ge {M}}\to {N}+1\in {ℤ}_{\ge {M}}$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\to {M}\in ℤ$
2 peano2z ${⊢}{N}\in ℤ\to {N}+1\in ℤ$
3 2 3ad2ant2 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\to {N}+1\in ℤ$
4 zre ${⊢}{M}\in ℤ\to {M}\in ℝ$
5 zre ${⊢}{N}\in ℤ\to {N}\in ℝ$
6 letrp1 ${⊢}\left({M}\in ℝ\wedge {N}\in ℝ\wedge {M}\le {N}\right)\to {M}\le {N}+1$
7 5 6 syl3an2 ${⊢}\left({M}\in ℝ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\to {M}\le {N}+1$
8 4 7 syl3an1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\to {M}\le {N}+1$
9 1 3 8 3jca ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)\to \left({M}\in ℤ\wedge {N}+1\in ℤ\wedge {M}\le {N}+1\right)$
10 eluz2 ${⊢}{N}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {N}\in ℤ\wedge {M}\le {N}\right)$
11 eluz2 ${⊢}{N}+1\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {N}+1\in ℤ\wedge {M}\le {N}+1\right)$
12 9 10 11 3imtr4i ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1\in {ℤ}_{\ge {M}}$