Step |
Hyp |
Ref |
Expression |
1 |
|
elinel2 |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> k e. ( ZZ>= ` ( N + 1 ) ) ) |
2 |
|
eluzle |
|- ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( N + 1 ) <_ k ) |
3 |
1 2
|
syl |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( N + 1 ) <_ k ) |
4 |
|
eluzel2 |
|- ( k e. ( ZZ>= ` ( N + 1 ) ) -> ( N + 1 ) e. ZZ ) |
5 |
1 4
|
syl |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( N + 1 ) e. ZZ ) |
6 |
|
eluzelz |
|- ( k e. ( ZZ>= ` ( N + 1 ) ) -> k e. ZZ ) |
7 |
1 6
|
syl |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> k e. ZZ ) |
8 |
|
zlem1lt |
|- ( ( ( N + 1 ) e. ZZ /\ k e. ZZ ) -> ( ( N + 1 ) <_ k <-> ( ( N + 1 ) - 1 ) < k ) ) |
9 |
5 7 8
|
syl2anc |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N + 1 ) <_ k <-> ( ( N + 1 ) - 1 ) < k ) ) |
10 |
3 9
|
mpbid |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N + 1 ) - 1 ) < k ) |
11 |
|
elinel1 |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> k e. ( 0 ... N ) ) |
12 |
|
elfzle2 |
|- ( k e. ( 0 ... N ) -> k <_ N ) |
13 |
11 12
|
syl |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> k <_ N ) |
14 |
7
|
zred |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> k e. RR ) |
15 |
|
elin |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) <-> ( k e. ( 0 ... N ) /\ k e. ( ZZ>= ` ( N + 1 ) ) ) ) |
16 |
|
elfzel2 |
|- ( k e. ( 0 ... N ) -> N e. ZZ ) |
17 |
16
|
adantr |
|- ( ( k e. ( 0 ... N ) /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> N e. ZZ ) |
18 |
15 17
|
sylbi |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> N e. ZZ ) |
19 |
18
|
zred |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> N e. RR ) |
20 |
14 19
|
lenltd |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( k <_ N <-> -. N < k ) ) |
21 |
18
|
zcnd |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> N e. CC ) |
22 |
|
pncan1 |
|- ( N e. CC -> ( ( N + 1 ) - 1 ) = N ) |
23 |
21 22
|
syl |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( ( N + 1 ) - 1 ) = N ) |
24 |
23
|
eqcomd |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> N = ( ( N + 1 ) - 1 ) ) |
25 |
24
|
breq1d |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( N < k <-> ( ( N + 1 ) - 1 ) < k ) ) |
26 |
25
|
notbid |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( -. N < k <-> -. ( ( N + 1 ) - 1 ) < k ) ) |
27 |
20 26
|
bitrd |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> ( k <_ N <-> -. ( ( N + 1 ) - 1 ) < k ) ) |
28 |
13 27
|
mpbid |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> -. ( ( N + 1 ) - 1 ) < k ) |
29 |
10 28
|
pm2.21dd |
|- ( k e. ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) -> k e. (/) ) |
30 |
29
|
ssriv |
|- ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) C_ (/) |
31 |
|
ss0 |
|- ( ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) C_ (/) -> ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) ) |
32 |
30 31
|
ax-mp |
|- ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/) |