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