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

Proof

Step Hyp Ref Expression
1 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
2 1 3ad2ant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( M + 1 ) e. ZZ )
3 peano2z 
 |-  ( N e. ZZ -> ( N + 1 ) e. ZZ )
4 3 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( N + 1 ) e. ZZ )
5 zre 
 |-  ( M e. ZZ -> M e. RR )
6 zre 
 |-  ( N e. ZZ -> N e. RR )
7 1re 
 |-  1 e. RR
8 leadd1 
 |-  ( ( M e. RR /\ N e. RR /\ 1 e. RR ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) )
9 7 8 mp3an3 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) )
10 5 6 9 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( M + 1 ) <_ ( N + 1 ) ) )
11 10 biimp3a 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( M + 1 ) <_ ( N + 1 ) )
12 2 4 11 3jca 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ( ( M + 1 ) e. ZZ /\ ( N + 1 ) e. ZZ /\ ( M + 1 ) <_ ( N + 1 ) ) )
13 eluz2 
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
14 eluz2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` ( M + 1 ) ) <-> ( ( M + 1 ) e. ZZ /\ ( N + 1 ) e. ZZ /\ ( M + 1 ) <_ ( N + 1 ) ) )
15 12 13 14 3imtr4i 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` ( M + 1 ) ) )