Metamath Proof Explorer


Theorem uzdisj

Description: The first N elements of an upper integer set are distinct from any later members. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion uzdisj
|- ( ( M ... ( N - 1 ) ) i^i ( ZZ>= ` N ) ) = (/)

Proof

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 ) ) = (/)