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 ) )