Step |
Hyp |
Ref |
Expression |
1 |
|
elinel2 |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> k e. ( ZZ>= ` N ) ) |
2 |
|
eluzle |
|- ( k e. ( ZZ>= ` N ) -> N <_ k ) |
3 |
1 2
|
syl |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> N <_ k ) |
4 |
|
eluzel2 |
|- ( k e. ( ZZ>= ` N ) -> N e. ZZ ) |
5 |
1 4
|
syl |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> N e. ZZ ) |
6 |
|
eluzelz |
|- ( k e. ( ZZ>= ` N ) -> k e. ZZ ) |
7 |
1 6
|
syl |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> k e. ZZ ) |
8 |
|
zlem1lt |
|- ( ( N e. ZZ /\ k e. ZZ ) -> ( N <_ k <-> ( N - 1 ) < k ) ) |
9 |
5 7 8
|
syl2anc |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> ( N <_ k <-> ( N - 1 ) < k ) ) |
10 |
3 9
|
mpbid |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> ( N - 1 ) < k ) |
11 |
7
|
zred |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> k e. RR ) |
12 |
|
peano2zm |
|- ( N e. ZZ -> ( N - 1 ) e. ZZ ) |
13 |
5 12
|
syl |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> ( N - 1 ) e. ZZ ) |
14 |
13
|
zred |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> ( N - 1 ) e. RR ) |
15 |
|
elinel1 |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> k e. ( M ... ( N - 1 ) ) ) |
16 |
|
elfzle2 |
|- ( k e. ( M ... ( N - 1 ) ) -> k <_ ( N - 1 ) ) |
17 |
15 16
|
syl |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> k <_ ( N - 1 ) ) |
18 |
11 14 17
|
lensymd |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> -. ( N - 1 ) < k ) |
19 |
10 18
|
pm2.21dd |
|- ( k e. ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) -> k e. (/) ) |
20 |
19
|
ssriv |
|- ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) C_ (/) |
21 |
|
ss0 |
|- ( ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) C_ (/) -> ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) = (/) ) |
22 |
20 21
|
ax-mp |
|- ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) = (/) |