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 )