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