Metamath Proof Explorer

Theorem nndiffz1

Description: Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017)

Ref Expression
Assertion nndiffz1 
|- ( N e. NN0 -> ( NN \ ( 1 ... N ) ) = ( ZZ>= ` ( N + 1 ) ) )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
3 elfz1 
 |-  ( ( 1 e. ZZ /\ N e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( j e. ZZ /\ 1 <_ j /\ j <_ N ) ) )
4 1 2 3 sylancr 
 |-  ( N e. NN0 -> ( j e. ( 1 ... N ) <-> ( j e. ZZ /\ 1 <_ j /\ j <_ N ) ) )
5 3anass 
 |-  ( ( j e. ZZ /\ 1 <_ j /\ j <_ N ) <-> ( j e. ZZ /\ ( 1 <_ j /\ j <_ N ) ) )
6 4 5 bitrdi 
 |-  ( N e. NN0 -> ( j e. ( 1 ... N ) <-> ( j e. ZZ /\ ( 1 <_ j /\ j <_ N ) ) ) )
7 6 baibd 
 |-  ( ( N e. NN0 /\ j e. ZZ ) -> ( j e. ( 1 ... N ) <-> ( 1 <_ j /\ j <_ N ) ) )
8 7 baibd 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ 1 <_ j ) -> ( j e. ( 1 ... N ) <-> j <_ N ) )
9 8 notbid 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ 1 <_ j ) -> ( -. j e. ( 1 ... N ) <-> -. j <_ N ) )
10 simpl 
 |-  ( ( N e. ZZ /\ j e. ZZ ) -> N e. ZZ )
11 10 zred 
 |-  ( ( N e. ZZ /\ j e. ZZ ) -> N e. RR )
12 simpr 
 |-  ( ( N e. ZZ /\ j e. ZZ ) -> j e. ZZ )
13 12 zred 
 |-  ( ( N e. ZZ /\ j e. ZZ ) -> j e. RR )
14 11 13 ltnled 
 |-  ( ( N e. ZZ /\ j e. ZZ ) -> ( N < j <-> -. j <_ N ) )
15 zltp1le 
 |-  ( ( N e. ZZ /\ j e. ZZ ) -> ( N < j <-> ( N + 1 ) <_ j ) )
16 14 15 bitr3d 
 |-  ( ( N e. ZZ /\ j e. ZZ ) -> ( -. j <_ N <-> ( N + 1 ) <_ j ) )
17 2 16 sylan 
 |-  ( ( N e. NN0 /\ j e. ZZ ) -> ( -. j <_ N <-> ( N + 1 ) <_ j ) )
18 17 adantr 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ 1 <_ j ) -> ( -. j <_ N <-> ( N + 1 ) <_ j ) )
19 9 18 bitrd 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ 1 <_ j ) -> ( -. j e. ( 1 ... N ) <-> ( N + 1 ) <_ j ) )
20 19 pm5.32da 
 |-  ( ( N e. NN0 /\ j e. ZZ ) -> ( ( 1 <_ j /\ -. j e. ( 1 ... N ) ) <-> ( 1 <_ j /\ ( N + 1 ) <_ j ) ) )
21 1red 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> 1 e. RR )
22 simpll 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> N e. NN0 )
23 22 nn0red 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> N e. RR )
24 23 21 readdcld 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> ( N + 1 ) e. RR )
25 simplr 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> j e. ZZ )
26 25 zred 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> j e. RR )
27 0p1e1 
 |-  ( 0 + 1 ) = 1
28 0red 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> 0 e. RR )
29 22 nn0ge0d 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> 0 <_ N )
30 28 23 21 29 leadd1dd 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> ( 0 + 1 ) <_ ( N + 1 ) )
31 27 30 eqbrtrrid 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> 1 <_ ( N + 1 ) )
32 simpr 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> ( N + 1 ) <_ j )
33 21 24 26 31 32 letrd 
 |-  ( ( ( N e. NN0 /\ j e. ZZ ) /\ ( N + 1 ) <_ j ) -> 1 <_ j )
34 33 ex 
 |-  ( ( N e. NN0 /\ j e. ZZ ) -> ( ( N + 1 ) <_ j -> 1 <_ j ) )
35 34 pm4.71rd 
 |-  ( ( N e. NN0 /\ j e. ZZ ) -> ( ( N + 1 ) <_ j <-> ( 1 <_ j /\ ( N + 1 ) <_ j ) ) )
36 20 35 bitr4d 
 |-  ( ( N e. NN0 /\ j e. ZZ ) -> ( ( 1 <_ j /\ -. j e. ( 1 ... N ) ) <-> ( N + 1 ) <_ j ) )
37 36 pm5.32da 
 |-  ( N e. NN0 -> ( ( j e. ZZ /\ ( 1 <_ j /\ -. j e. ( 1 ... N ) ) ) <-> ( j e. ZZ /\ ( N + 1 ) <_ j ) ) )
38 eldif 
 |-  ( j e. ( NN \ ( 1 ... N ) ) <-> ( j e. NN /\ -. j e. ( 1 ... N ) ) )
39 elnnz1 
 |-  ( j e. NN <-> ( j e. ZZ /\ 1 <_ j ) )
40 39 anbi1i 
 |-  ( ( j e. NN /\ -. j e. ( 1 ... N ) ) <-> ( ( j e. ZZ /\ 1 <_ j ) /\ -. j e. ( 1 ... N ) ) )
41 anass 
 |-  ( ( ( j e. ZZ /\ 1 <_ j ) /\ -. j e. ( 1 ... N ) ) <-> ( j e. ZZ /\ ( 1 <_ j /\ -. j e. ( 1 ... N ) ) ) )
42 38 40 41 3bitri 
 |-  ( j e. ( NN \ ( 1 ... N ) ) <-> ( j e. ZZ /\ ( 1 <_ j /\ -. j e. ( 1 ... N ) ) ) )
43 42 a1i 
 |-  ( N e. NN0 -> ( j e. ( NN \ ( 1 ... N ) ) <-> ( j e. ZZ /\ ( 1 <_ j /\ -. j e. ( 1 ... N ) ) ) ) )
44 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
45 44 nn0zd 
 |-  ( N e. NN0 -> ( N + 1 ) e. ZZ )
46 eluz1 
 |-  ( ( N + 1 ) e. ZZ -> ( j e. ( ZZ>= ` ( N + 1 ) ) <-> ( j e. ZZ /\ ( N + 1 ) <_ j ) ) )
47 45 46 syl 
 |-  ( N e. NN0 -> ( j e. ( ZZ>= ` ( N + 1 ) ) <-> ( j e. ZZ /\ ( N + 1 ) <_ j ) ) )
48 37 43 47 3bitr4d 
 |-  ( N e. NN0 -> ( j e. ( NN \ ( 1 ... N ) ) <-> j e. ( ZZ>= ` ( N + 1 ) ) ) )
49 48 eqrdv 
 |-  ( N e. NN0 -> ( NN \ ( 1 ... N ) ) = ( ZZ>= ` ( N + 1 ) ) )