This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem peano2fzr

Description: A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ... N ) ) -> K e. ( ZZ>= ` M ) )
2 eluzelz 
 |-  ( K e. ( ZZ>= ` M ) -> K e. ZZ )
3 elfzuz3 
 |-  ( ( K + 1 ) e. ( M ... N ) -> N e. ( ZZ>= ` ( K + 1 ) ) )
4 peano2uzr 
 |-  ( ( K e. ZZ /\ N e. ( ZZ>= ` ( K + 1 ) ) ) -> N e. ( ZZ>= ` K ) )
5 2 3 4 syl2an 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ... N ) ) -> N e. ( ZZ>= ` K ) )
6 elfzuzb 
 |-  ( K e. ( M ... N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` K ) ) )
7 1 5 6 sylanbrc 
 |-  ( ( K e. ( ZZ>= ` M ) /\ ( K + 1 ) e. ( M ... N ) ) -> K e. ( M ... N ) )