Theorem elfz2nn0

Description: Membership in a finite set of sequential nonnegative integers. (Contributed by NM, 16-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0uz	|- ( K e. NN0 <-> K e. ( ZZ>= ` 0 ) )
2	1	anbi1i	|- ( ( K e. NN0 /\ N e. ( ZZ>= ` K ) ) <-> ( K e. ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` K ) ) )
3		eluznn0	|- ( ( K e. NN0 /\ N e. ( ZZ>= ` K ) ) -> N e. NN0 )
4		eluzle	|- ( N e. ( ZZ>= ` K ) -> K <_ N )
5	4	adantl	|- ( ( K e. NN0 /\ N e. ( ZZ>= ` K ) ) -> K <_ N )
6	3 5	jca	|- ( ( K e. NN0 /\ N e. ( ZZ>= ` K ) ) -> ( N e. NN0 /\ K <_ N ) )
7		nn0z	|- ( K e. NN0 -> K e. ZZ )
8		nn0z	|- ( N e. NN0 -> N e. ZZ )
9		eluz	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` K ) <-> K <_ N ) )
10	7 8 9	syl2an	|- ( ( K e. NN0 /\ N e. NN0 ) -> ( N e. ( ZZ>= ` K ) <-> K <_ N ) )
11	10	biimprd	|- ( ( K e. NN0 /\ N e. NN0 ) -> ( K <_ N -> N e. ( ZZ>= ` K ) ) )
12	11	impr	|- ( ( K e. NN0 /\ ( N e. NN0 /\ K <_ N ) ) -> N e. ( ZZ>= ` K ) )
13	6 12	impbida	|- ( K e. NN0 -> ( N e. ( ZZ>= ` K ) <-> ( N e. NN0 /\ K <_ N ) ) )
14	13	pm5.32i	|- ( ( K e. NN0 /\ N e. ( ZZ>= ` K ) ) <-> ( K e. NN0 /\ ( N e. NN0 /\ K <_ N ) ) )
15	2 14	bitr3i	|- ( ( K e. ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` K ) ) <-> ( K e. NN0 /\ ( N e. NN0 /\ K <_ N ) ) )
16		elfzuzb	|- ( K e. ( 0 ... N ) <-> ( K e. ( ZZ>= ` 0 ) /\ N e. ( ZZ>= ` K ) ) )
17		3anass	|- ( ( K e. NN0 /\ N e. NN0 /\ K <_ N ) <-> ( K e. NN0 /\ ( N e. NN0 /\ K <_ N ) ) )
18	15 16 17	3bitr4i	|- ( K e. ( 0 ... N ) <-> ( K e. NN0 /\ N e. NN0 /\ K <_ N ) )