Theorem elfz1end

Description: A nonempty finite range of integers contains its end point. (Contributed by Stefan O'Rear, 10-Oct-2014)

	Ref	Expression
Assertion	elfz1end	|- ( A e. NN <-> A e. ( 1 ... A ) )

Proof

Step	Hyp	Ref	Expression
1		elnnuz	|- ( A e. NN <-> A e. ( ZZ>= ` 1 ) )
2	1	biimpi	|- ( A e. NN -> A e. ( ZZ>= ` 1 ) )
3		nnz	|- ( A e. NN -> A e. ZZ )
4		uzid	|- ( A e. ZZ -> A e. ( ZZ>= ` A ) )
5	3 4	syl	|- ( A e. NN -> A e. ( ZZ>= ` A ) )
6		eluzfz	|- ( ( A e. ( ZZ>= ` 1 ) /\ A e. ( ZZ>= ` A ) ) -> A e. ( 1 ... A ) )
7	2 5 6	syl2anc	|- ( A e. NN -> A e. ( 1 ... A ) )
8		elfznn	|- ( A e. ( 1 ... A ) -> A e. NN )
9	7 8	impbii	|- ( A e. NN <-> A e. ( 1 ... A ) )