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