Metamath Proof Explorer


Theorem elfznelfzob

Description: A value in a finite set of sequential integers is a border value if and only if it is not contained in the half-open integer range contained in the finite set of sequential integers. (Contributed by Alexander van der Vekens, 17-Jan-2018) (Revised by Thierry Arnoux, 22-Dec-2021)

Ref Expression
Assertion elfznelfzob M0K¬M1..^KM=0M=K

Proof

Step Hyp Ref Expression
1 elfznelfzo M0K¬M1..^KM=0M=K
2 1 ex M0K¬M1..^KM=0M=K
3 elfzole1 M1..^K1M
4 elfzolt2 M1..^KM<K
5 elfzoel2 M1..^KK
6 elfzoelz M1..^KM
7 0lt1 0<1
8 breq1 M=0M<10<1
9 7 8 mpbiri M=0M<1
10 zre MM
11 10 adantl M<KKMM
12 1red M<KKM1
13 11 12 ltnled M<KKMM<1¬1M
14 9 13 syl5ib M<KKMM=0¬1M
15 14 con2d M<KKM1M¬M=0
16 zre KK
17 ltlen MKM<KMKKM
18 10 16 17 syl2anr KMM<KMKKM
19 necom KMMK
20 df-ne MK¬M=K
21 19 20 sylbb KM¬M=K
22 21 adantl MKKM¬M=K
23 18 22 syl6bi KMM<K¬M=K
24 23 ex KMM<K¬M=K
25 24 com23 KM<KM¬M=K
26 25 impcom M<KKM¬M=K
27 26 imp M<KKM¬M=K
28 15 27 jctird M<KKM1M¬M=0¬M=K
29 4 5 6 28 syl21anc M1..^K1M¬M=0¬M=K
30 3 29 mpd M1..^K¬M=0¬M=K
31 ioran ¬M=0M=K¬M=0¬M=K
32 30 31 sylibr M1..^K¬M=0M=K
33 32 a1i M0KM1..^K¬M=0M=K
34 33 con2d M0KM=0M=K¬M1..^K
35 2 34 impbid M0K¬M1..^KM=0M=K