Metamath Proof Explorer

Theorem elfzo2

Description: Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015)

Ref Expression
Assertion elfzo2 ⊢ K ∈ M ..^ N ↔ K ∈ ℤ ≥ M ∧ N ∈ ℤ ∧ K < N

Proof

Step Hyp Ref Expression
1 an4 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K < N ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ M ≤ K ∧ N ∈ ℤ ∧ K < N
2 df-3an ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ
3 2 anbi1i ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K < N ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K < N
4 eluz2 ⊢ K ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K
5 3ancoma ⊢ M ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ M ≤ K
6 df-3an ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ M ≤ K ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ M ≤ K
7 4 5 6 3bitri ⊢ K ∈ ℤ ≥ M ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ M ≤ K
8 7 anbi1i ⊢ K ∈ ℤ ≥ M ∧ N ∈ ℤ ∧ K < N ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ M ≤ K ∧ N ∈ ℤ ∧ K < N
9 1 3 8 3bitr4i ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K < N ↔ K ∈ ℤ ≥ M ∧ N ∈ ℤ ∧ K < N
10 elfzoelz ⊢ K ∈ M ..^ N → K ∈ ℤ
11 elfzoel1 ⊢ K ∈ M ..^ N → M ∈ ℤ
12 elfzoel2 ⊢ K ∈ M ..^ N → N ∈ ℤ
13 10 11 12 3jca ⊢ K ∈ M ..^ N → K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ
14 elfzo ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M ..^ N ↔ M ≤ K ∧ K < N
15 13 14 biadanii ⊢ K ∈ M ..^ N ↔ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K < N
16 3anass ⊢ K ∈ ℤ ≥ M ∧ N ∈ ℤ ∧ K < N ↔ K ∈ ℤ ≥ M ∧ N ∈ ℤ ∧ K < N
17 9 15 16 3bitr4i ⊢ K ∈ M ..^ N ↔ K ∈ ℤ ≥ M ∧ N ∈ ℤ ∧ K < N