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 ∈ 0 … K → ¬ M ∈ 1 ..^ K ↔ M = 0 ∨ M = K

Proof

Step Hyp Ref Expression
1 elfznelfzo ⊢ M ∈ 0 … K ∧ ¬ M ∈ 1 ..^ K → M = 0 ∨ M = K
2 1 ex ⊢ M ∈ 0 … K → ¬ M ∈ 1 ..^ K → M = 0 ∨ M = K
3 elfzole1 ⊢ M ∈ 1 ..^ K → 1 ≤ M
4 elfzolt2 ⊢ M ∈ 1 ..^ K → M < K
5 elfzoel2 ⊢ M ∈ 1 ..^ K → K ∈ ℤ
6 elfzoelz ⊢ M ∈ 1 ..^ K → M ∈ ℤ
7 0lt1 ⊢ 0 < 1
8 breq1 ⊢ M = 0 → M < 1 ↔ 0 < 1
9 7 8 mpbiri ⊢ M = 0 → M < 1
10 zre ⊢ M ∈ ℤ → M ∈ ℝ
11 10 adantl ⊢ M < K ∧ K ∈ ℤ ∧ M ∈ ℤ → M ∈ ℝ
12 1red ⊢ M < K ∧ K ∈ ℤ ∧ M ∈ ℤ → 1 ∈ ℝ
13 11 12 ltnled ⊢ M < K ∧ K ∈ ℤ ∧ M ∈ ℤ → M < 1 ↔ ¬ 1 ≤ M
14 9 13 imbitrid ⊢ M < K ∧ K ∈ ℤ ∧ M ∈ ℤ → M = 0 → ¬ 1 ≤ M
15 14 con2d ⊢ M < K ∧ K ∈ ℤ ∧ M ∈ ℤ → 1 ≤ M → ¬ M = 0
16 zre ⊢ K ∈ ℤ → K ∈ ℝ
17 ltlen ⊢ M ∈ ℝ ∧ K ∈ ℝ → M < K ↔ M ≤ K ∧ K ≠ M
18 10 16 17 syl2anr ⊢ K ∈ ℤ ∧ M ∈ ℤ → 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 biimtrdi ⊢ K ∈ ℤ ∧ M ∈ ℤ → M < K → ¬ M = K
24 23 ex ⊢ K ∈ ℤ → M ∈ ℤ → M < K → ¬ M = K
25 24 com23 ⊢ K ∈ ℤ → M < K → M ∈ ℤ → ¬ M = K
26 25 impcom ⊢ M < K ∧ K ∈ ℤ → M ∈ ℤ → ¬ M = K
27 26 imp ⊢ M < K ∧ K ∈ ℤ ∧ M ∈ ℤ → ¬ M = K
28 15 27 jctird ⊢ M < K ∧ K ∈ ℤ ∧ M ∈ ℤ → 1 ≤ M → ¬ M = 0 ∧ ¬ M = K
29 4 5 6 28 syl21anc ⊢ M ∈ 1 ..^ K → 1 ≤ M → ¬ M = 0 ∧ ¬ M = K
30 3 29 mpd ⊢ M ∈ 1 ..^ K → ¬ M = 0 ∧ ¬ M = K
31 ioran ⊢ ¬ M = 0 ∨ M = K ↔ ¬ M = 0 ∧ ¬ M = K
32 30 31 sylibr ⊢ M ∈ 1 ..^ K → ¬ M = 0 ∨ M = K
33 32 a1i ⊢ M ∈ 0 … K → M ∈ 1 ..^ K → ¬ M = 0 ∨ M = K
34 33 con2d ⊢ M ∈ 0 … K → M = 0 ∨ M = K → ¬ M ∈ 1 ..^ K
35 2 34 impbid ⊢ M ∈ 0 … K → ¬ M ∈ 1 ..^ K ↔ M = 0 ∨ M = K