Metamath Proof Explorer

Theorem fzp1elp1

Description: Add one to an element of a finite set of integers. (Contributed by Jeff Madsen, 6-Jun-2010) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion fzp1elp1 
|- ( K e. ( M ... N ) -> ( K + 1 ) e. ( M ... ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 elfzuz 
 |-  ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
2 peano2uz 
 |-  ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
3 1 2 syl 
 |-  ( K e. ( M ... N ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
4 elfzuz3 
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
5 eluzp1p1 
 |-  ( N e. ( ZZ>= ` K ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
6 4 5 syl 
 |-  ( K e. ( M ... N ) -> ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) )
7 elfzuzb 
 |-  ( ( K + 1 ) e. ( M ... ( N + 1 ) ) <-> ( ( K + 1 ) e. ( ZZ>= ` M ) /\ ( N + 1 ) e. ( ZZ>= ` ( K + 1 ) ) ) )
8 3 6 7 sylanbrc 
 |-  ( K e. ( M ... N ) -> ( K + 1 ) e. ( M ... ( N + 1 ) ) )