Metamath Proof Explorer

Theorem nn0disj

Description: The first N + 1 elements of the set of nonnegative integers are distinct from any later members. (Contributed by AV, 8-Nov-2019)

Ref Expression
Assertion nn0disj 
|- ( ( 0 ... N ) i^i ( ZZ>= ` ( N + 1 ) ) ) = (/)

Proof

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