Metamath Proof Explorer


Theorem fzp1nel

Description: One plus the upper bound of a finite set of integers is not a member of that set. (Contributed by Scott Fenton, 16-Dec-2017)

Ref Expression
Assertion fzp1nel
|- -. ( N + 1 ) e. ( M ... N )

Proof

Step Hyp Ref Expression
1 zre
 |-  ( N e. ZZ -> N e. RR )
2 ltp1
 |-  ( N e. RR -> N < ( N + 1 ) )
3 id
 |-  ( N e. RR -> N e. RR )
4 peano2re
 |-  ( N e. RR -> ( N + 1 ) e. RR )
5 3 4 ltnled
 |-  ( N e. RR -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
6 2 5 mpbid
 |-  ( N e. RR -> -. ( N + 1 ) <_ N )
7 1 6 syl
 |-  ( N e. ZZ -> -. ( N + 1 ) <_ N )
8 7 intnand
 |-  ( N e. ZZ -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) )
9 8 3ad2ant2
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) )
10 elfz2
 |-  ( ( N + 1 ) e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) /\ ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) )
11 10 notbii
 |-  ( -. ( N + 1 ) e. ( M ... N ) <-> -. ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) /\ ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) )
12 imnan
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) <-> -. ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) /\ ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) )
13 11 12 bitr4i
 |-  ( -. ( N + 1 ) e. ( M ... N ) <-> ( ( M e. ZZ /\ N e. ZZ /\ ( N + 1 ) e. ZZ ) -> -. ( M <_ ( N + 1 ) /\ ( N + 1 ) <_ N ) ) )
14 9 13 mpbir
 |-  -. ( N + 1 ) e. ( M ... N )