# 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 e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )`

### Proof

Step Hyp Ref Expression
1 simp1
` |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M e. ZZ )`
2 peano2z
` |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )`
` |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( N + 1 ) e. ZZ )`
4 zre
` |-  ( M e. ZZ -> M e. RR )`
5 zre
` |-  ( N e. ZZ -> N e. RR )`
6 letrp1
` |-  ( ( M e. RR /\ N e. RR /\ M <_ N ) -> M <_ ( N + 1 ) )`
7 5 6 syl3an2
` |-  ( ( M e. RR /\ N e. ZZ /\ M <_ N ) -> M <_ ( N + 1 ) )`
8 4 7 syl3an1
` |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> M <_ ( N + 1 ) )`
9 1 3 8 3jca
` |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( M e. ZZ /\ ( N + 1 ) e. ZZ /\ M <_ ( N + 1 ) ) )`
10 eluz2
` |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )`
11 eluz2
` |-  ( ( N + 1 ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( N + 1 ) e. ZZ /\ M <_ ( N + 1 ) ) )`
12 9 10 11 3imtr4i
` |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )`