Metamath Proof Explorer

Theorem eluzp1m1

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

Ref Expression
Assertion eluzp1m1 
|- ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )

Proof

Step Hyp Ref Expression
1 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
2 1 ad2antrl 
 |-  ( ( M e. ZZ /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> ( N - 1 ) e. ZZ )
3 zre 
 |-  ( M e. ZZ -> M e. RR )
4 zre 
 |-  ( N e. ZZ -> N e. RR )
5 1re 
 |-  1 e. RR
6 leaddsub 
 |-  ( ( M e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( M + 1 ) <_ N <-> M <_ ( N - 1 ) ) )
7 5 6 mp3an2 
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( M + 1 ) <_ N <-> M <_ ( N - 1 ) ) )
8 3 4 7 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) <_ N <-> M <_ ( N - 1 ) ) )
9 8 biimpa 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M + 1 ) <_ N ) -> M <_ ( N - 1 ) )
10 9 anasss 
 |-  ( ( M e. ZZ /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> M <_ ( N - 1 ) )
11 2 10 jca 
 |-  ( ( M e. ZZ /\ ( N e. ZZ /\ ( M + 1 ) <_ N ) ) -> ( ( N - 1 ) e. ZZ /\ M <_ ( N - 1 ) ) )
12 11 ex 
 |-  ( M e. ZZ -> ( ( N e. ZZ /\ ( M + 1 ) <_ N ) -> ( ( N - 1 ) e. ZZ /\ M <_ ( N - 1 ) ) ) )
13 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
14 eluz1 
 |-  ( ( M + 1 ) e. ZZ -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( N e. ZZ /\ ( M + 1 ) <_ N ) ) )
15 13 14 syl 
 |-  ( M e. ZZ -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( N e. ZZ /\ ( M + 1 ) <_ N ) ) )
16 eluz1 
 |-  ( M e. ZZ -> ( ( N - 1 ) e. ( ZZ>= ` M ) <-> ( ( N - 1 ) e. ZZ /\ M <_ ( N - 1 ) ) ) )
17 12 15 16 3imtr4d 
 |-  ( M e. ZZ -> ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) ) )
18 17 imp 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )