Metamath Proof Explorer


Theorem fz1eqin

Description: Express a one-based finite range as the intersection of lower integers with NN . (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion fz1eqin
|- ( N e. NN0 -> ( 1 ... N ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) )

Proof

Step Hyp Ref Expression
1 1z
 |-  1 e. ZZ
2 nn0z
 |-  ( N e. NN0 -> N e. ZZ )
3 elfz1
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( a e. ( 1 ... N ) <-> ( a e. ZZ /\ 1 <_ a /\ a <_ N ) ) )
4 1 2 3 sylancr
 |-  ( N e. NN0 -> ( a e. ( 1 ... N ) <-> ( a e. ZZ /\ 1 <_ a /\ a <_ N ) ) )
5 3anass
 |-  ( ( a e. ZZ /\ 1 <_ a /\ a <_ N ) <-> ( a e. ZZ /\ ( 1 <_ a /\ a <_ N ) ) )
6 ancom
 |-  ( ( 1 <_ a /\ a <_ N ) <-> ( a <_ N /\ 1 <_ a ) )
7 6 anbi2i
 |-  ( ( a e. ZZ /\ ( 1 <_ a /\ a <_ N ) ) <-> ( a e. ZZ /\ ( a <_ N /\ 1 <_ a ) ) )
8 anandi
 |-  ( ( a e. ZZ /\ ( a <_ N /\ 1 <_ a ) ) <-> ( ( a e. ZZ /\ a <_ N ) /\ ( a e. ZZ /\ 1 <_ a ) ) )
9 5 7 8 3bitri
 |-  ( ( a e. ZZ /\ 1 <_ a /\ a <_ N ) <-> ( ( a e. ZZ /\ a <_ N ) /\ ( a e. ZZ /\ 1 <_ a ) ) )
10 4 9 bitrdi
 |-  ( N e. NN0 -> ( a e. ( 1 ... N ) <-> ( ( a e. ZZ /\ a <_ N ) /\ ( a e. ZZ /\ 1 <_ a ) ) ) )
11 elin
 |-  ( a e. ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) <-> ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) /\ a e. NN ) )
12 ellz1
 |-  ( N e. ZZ -> ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) <-> ( a e. ZZ /\ a <_ N ) ) )
13 2 12 syl
 |-  ( N e. NN0 -> ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) <-> ( a e. ZZ /\ a <_ N ) ) )
14 elnnz1
 |-  ( a e. NN <-> ( a e. ZZ /\ 1 <_ a ) )
15 14 a1i
 |-  ( N e. NN0 -> ( a e. NN <-> ( a e. ZZ /\ 1 <_ a ) ) )
16 13 15 anbi12d
 |-  ( N e. NN0 -> ( ( a e. ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) /\ a e. NN ) <-> ( ( a e. ZZ /\ a <_ N ) /\ ( a e. ZZ /\ 1 <_ a ) ) ) )
17 11 16 syl5bb
 |-  ( N e. NN0 -> ( a e. ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) <-> ( ( a e. ZZ /\ a <_ N ) /\ ( a e. ZZ /\ 1 <_ a ) ) ) )
18 10 17 bitr4d
 |-  ( N e. NN0 -> ( a e. ( 1 ... N ) <-> a e. ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) ) )
19 18 eqrdv
 |-  ( N e. NN0 -> ( 1 ... N ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) )