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 )