Metamath Proof Explorer

Theorem 0nelfz1

Description: 0 is not an element of a finite interval of integers starting at 1. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion 0nelfz1 
|- 0 e/ ( 1 ... N )

Proof

Step Hyp Ref Expression
1 0lt1 
 |-  0 < 1
2 0re 
 |-  0 e. RR
3 1re 
 |-  1 e. RR
4 2 3 ltnlei 
 |-  ( 0 < 1 <-> -. 1 <_ 0 )
5 1 4 mpbi 
 |-  -. 1 <_ 0
6 5 intnanr 
 |-  -. ( 1 <_ 0 /\ 0 <_ N )
7 6 intnan 
 |-  -. ( ( 1 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 1 <_ 0 /\ 0 <_ N ) )
8 df-nel 
 |-  ( 0 e/ ( 1 ... N ) <-> -. 0 e. ( 1 ... N ) )
9 elfz2 
 |-  ( 0 e. ( 1 ... N ) <-> ( ( 1 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 1 <_ 0 /\ 0 <_ N ) ) )
10 8 9 xchbinx 
 |-  ( 0 e/ ( 1 ... N ) <-> -. ( ( 1 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) /\ ( 1 <_ 0 /\ 0 <_ N ) ) )
11 7 10 mpbir 
 |-  0 e/ ( 1 ... N )