Theorem fznn0

Description: Characterization of a finite set of sequential nonnegative integers. (Contributed by NM, 1-Aug-2005)

	Ref	Expression
Assertion	fznn0	|- ( N e. NN0 -> ( K e. ( 0 ... N ) <-> ( K e. NN0 /\ K <_ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		0z	|- 0 e. ZZ
2		nn0z	|- ( N e. NN0 -> N e. ZZ )
3		elfz1	|- ( ( 0 e. ZZ /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> ( K e. ZZ /\ 0 <_ K /\ K <_ N ) ) )
4	1 2 3	sylancr	|- ( N e. NN0 -> ( K e. ( 0 ... N ) <-> ( K e. ZZ /\ 0 <_ K /\ K <_ N ) ) )
5		df-3an	|- ( ( K e. ZZ /\ 0 <_ K /\ K <_ N ) <-> ( ( K e. ZZ /\ 0 <_ K ) /\ K <_ N ) )
6		elnn0z	|- ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )
7	6	anbi1i	|- ( ( K e. NN0 /\ K <_ N ) <-> ( ( K e. ZZ /\ 0 <_ K ) /\ K <_ N ) )
8	5 7	bitr4i	|- ( ( K e. ZZ /\ 0 <_ K /\ K <_ N ) <-> ( K e. NN0 /\ K <_ N ) )
9	4 8	bitrdi	|- ( N e. NN0 -> ( K e. ( 0 ... N ) <-> ( K e. NN0 /\ K <_ N ) ) )