Theorem elfz1eq

Description: Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005)

	Ref	Expression
Assertion	elfz1eq	|- ( K e. ( N ... N ) -> K = N )

Proof

Step	Hyp	Ref	Expression
1		elfzle2	|- ( K e. ( N ... N ) -> K <_ N )
2		elfzle1	|- ( K e. ( N ... N ) -> N <_ K )
3		elfzelz	|- ( K e. ( N ... N ) -> K e. ZZ )
4		elfzel2	|- ( K e. ( N ... N ) -> N e. ZZ )
5		zre	|- ( K e. ZZ -> K e. RR )
6		zre	|- ( N e. ZZ -> N e. RR )
7		letri3	|- ( ( K e. RR /\ N e. RR ) -> ( K = N <-> ( K <_ N /\ N <_ K ) ) )
8	5 6 7	syl2an	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K = N <-> ( K <_ N /\ N <_ K ) ) )
9	3 4 8	syl2anc	|- ( K e. ( N ... N ) -> ( K = N <-> ( K <_ N /\ N <_ K ) ) )
10	1 2 9	mpbir2and	|- ( K e. ( N ... N ) -> K = N )