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