This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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