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 
|- ( M e. ( 0 ... K ) -> ( -. M e. ( 1 ..^ K ) <-> ( M = 0 \/ M = K ) ) )

Proof

Step Hyp Ref Expression
1 elfznelfzo 
 |-  ( ( M e. ( 0 ... K ) /\ -. M e. ( 1 ..^ K ) ) -> ( M = 0 \/ M = K ) )
2 1 ex 
 |-  ( M e. ( 0 ... K ) -> ( -. M e. ( 1 ..^ K ) -> ( M = 0 \/ M = K ) ) )
3 elfzole1 
 |-  ( M e. ( 1 ..^ K ) -> 1 <_ M )
4 elfzolt2 
 |-  ( M e. ( 1 ..^ K ) -> M < K )
5 elfzoel2 
 |-  ( M e. ( 1 ..^ K ) -> K e. ZZ )
6 elfzoelz 
 |-  ( M e. ( 1 ..^ K ) -> M e. ZZ )
7 0lt1 
 |-  0 < 1
8 breq1 
 |-  ( M = 0 -> ( M < 1 <-> 0 < 1 ) )
9 7 8 mpbiri 
 |-  ( M = 0 -> M < 1 )
10 zre 
 |-  ( M e. ZZ -> M e. RR )
11 10 adantl 
 |-  ( ( ( M < K /\ K e. ZZ ) /\ M e. ZZ ) -> M e. RR )
12 1red 
 |-  ( ( ( M < K /\ K e. ZZ ) /\ M e. ZZ ) -> 1 e. RR )
13 11 12 ltnled 
 |-  ( ( ( M < K /\ K e. ZZ ) /\ M e. ZZ ) -> ( M < 1 <-> -. 1 <_ M ) )
14 9 13 syl5ib 
 |-  ( ( ( M < K /\ K e. ZZ ) /\ M e. ZZ ) -> ( M = 0 -> -. 1 <_ M ) )
15 14 con2d 
 |-  ( ( ( M < K /\ K e. ZZ ) /\ M e. ZZ ) -> ( 1 <_ M -> -. M = 0 ) )
16 zre 
 |-  ( K e. ZZ -> K e. RR )
17 ltlen 
 |-  ( ( M e. RR /\ K e. RR ) -> ( M < K <-> ( M <_ K /\ K =/= M ) ) )
18 10 16 17 syl2anr 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( M < K <-> ( M <_ K /\ K =/= M ) ) )
19 necom 
 |-  ( K =/= M <-> M =/= K )
20 df-ne 
 |-  ( M =/= K <-> -. M = K )
21 19 20 sylbb 
 |-  ( K =/= M -> -. M = K )
22 21 adantl 
 |-  ( ( M <_ K /\ K =/= M ) -> -. M = K )
23 18 22 syl6bi 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( M < K -> -. M = K ) )
24 23 ex 
 |-  ( K e. ZZ -> ( M e. ZZ -> ( M < K -> -. M = K ) ) )
25 24 com23 
 |-  ( K e. ZZ -> ( M < K -> ( M e. ZZ -> -. M = K ) ) )
26 25 impcom 
 |-  ( ( M < K /\ K e. ZZ ) -> ( M e. ZZ -> -. M = K ) )
27 26 imp 
 |-  ( ( ( M < K /\ K e. ZZ ) /\ M e. ZZ ) -> -. M = K )
28 15 27 jctird 
 |-  ( ( ( M < K /\ K e. ZZ ) /\ M e. ZZ ) -> ( 1 <_ M -> ( -. M = 0 /\ -. M = K ) ) )
29 4 5 6 28 syl21anc 
 |-  ( M e. ( 1 ..^ K ) -> ( 1 <_ M -> ( -. M = 0 /\ -. M = K ) ) )
30 3 29 mpd 
 |-  ( M e. ( 1 ..^ K ) -> ( -. M = 0 /\ -. M = K ) )
31 ioran 
 |-  ( -. ( M = 0 \/ M = K ) <-> ( -. M = 0 /\ -. M = K ) )
32 30 31 sylibr 
 |-  ( M e. ( 1 ..^ K ) -> -. ( M = 0 \/ M = K ) )
33 32 a1i 
 |-  ( M e. ( 0 ... K ) -> ( M e. ( 1 ..^ K ) -> -. ( M = 0 \/ M = K ) ) )
34 33 con2d 
 |-  ( M e. ( 0 ... K ) -> ( ( M = 0 \/ M = K ) -> -. M e. ( 1 ..^ K ) ) )
35 2 34 impbid 
 |-  ( M e. ( 0 ... K ) -> ( -. M e. ( 1 ..^ K ) <-> ( M = 0 \/ M = K ) ) )