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 ( 𝑀 ∈ ( 0 ... 𝐾 ) → ( ¬ 𝑀 ∈ ( 1 ..^ 𝐾 ) ↔ ( 𝑀 = 0 ∨ 𝑀 = 𝐾 ) ) )

Proof

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