Metamath Proof Explorer

Theorem nelfzo

Description: An integer not being a member of a half-open finite set of integers. (Contributed by AV, 29-Apr-2020)

Ref Expression
Assertion nelfzo ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∉ M ..^ N ↔ K < M ∨ N ≤ K

Proof

Step Hyp Ref Expression
1 df-nel ⊢ K ∉ M ..^ N ↔ ¬ K ∈ M ..^ N
2 ianor ⊢ ¬ M ≤ K ∧ K < N ↔ ¬ M ≤ K ∨ ¬ K < N
3 2 a1i ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ M ≤ K ∧ K < N ↔ ¬ M ≤ K ∨ ¬ K < N
4 elfzo ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M ..^ N ↔ M ≤ K ∧ K < N
5 4 notbid ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ K ∈ M ..^ N ↔ ¬ M ≤ K ∧ K < N
6 zre ⊢ K ∈ ℤ → K ∈ ℝ
7 zre ⊢ M ∈ ℤ → M ∈ ℝ
8 6 7 anim12i ⊢ K ∈ ℤ ∧ M ∈ ℤ → K ∈ ℝ ∧ M ∈ ℝ
9 8 3adant3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℝ ∧ M ∈ ℝ
10 ltnle ⊢ K ∈ ℝ ∧ M ∈ ℝ → K < M ↔ ¬ M ≤ K
11 9 10 syl ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K < M ↔ ¬ M ≤ K
12 zre ⊢ N ∈ ℤ → N ∈ ℝ
13 6 12 anim12ci ⊢ K ∈ ℤ ∧ N ∈ ℤ → N ∈ ℝ ∧ K ∈ ℝ
14 13 3adant2 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → N ∈ ℝ ∧ K ∈ ℝ
15 lenlt ⊢ N ∈ ℝ ∧ K ∈ ℝ → N ≤ K ↔ ¬ K < N
16 14 15 syl ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → N ≤ K ↔ ¬ K < N
17 11 16 orbi12d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K < M ∨ N ≤ K ↔ ¬ M ≤ K ∨ ¬ K < N
18 3 5 17 3bitr4d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ K ∈ M ..^ N ↔ K < M ∨ N ≤ K
19 1 18 bitrid ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∉ M ..^ N ↔ K < M ∨ N ≤ K