# 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}\in \left({M}..^{N}\right)↔\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {K}<{N}\right)$

### Proof

Step Hyp Ref Expression
1 an4 ${⊢}\left(\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {N}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}<{N}\right)\right)↔\left(\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {M}\le {K}\right)\wedge \left({N}\in ℤ\wedge {K}<{N}\right)\right)$
2 df-3an ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)↔\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {N}\in ℤ\right)$
3 2 anbi1i ${⊢}\left(\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}<{N}\right)\right)↔\left(\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {N}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}<{N}\right)\right)$
4 eluz2 ${⊢}{K}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {K}\in ℤ\wedge {M}\le {K}\right)$
5 3ancoma ${⊢}\left({M}\in ℤ\wedge {K}\in ℤ\wedge {M}\le {K}\right)↔\left({K}\in ℤ\wedge {M}\in ℤ\wedge {M}\le {K}\right)$
6 df-3an ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {M}\le {K}\right)↔\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {M}\le {K}\right)$
7 4 5 6 3bitri ${⊢}{K}\in {ℤ}_{\ge {M}}↔\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {M}\le {K}\right)$
8 7 anbi1i ${⊢}\left({K}\in {ℤ}_{\ge {M}}\wedge \left({N}\in ℤ\wedge {K}<{N}\right)\right)↔\left(\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {M}\le {K}\right)\wedge \left({N}\in ℤ\wedge {K}<{N}\right)\right)$
9 1 3 8 3bitr4i ${⊢}\left(\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}<{N}\right)\right)↔\left({K}\in {ℤ}_{\ge {M}}\wedge \left({N}\in ℤ\wedge {K}<{N}\right)\right)$
10 elfzoelz ${⊢}{K}\in \left({M}..^{N}\right)\to {K}\in ℤ$
11 elfzoel1 ${⊢}{K}\in \left({M}..^{N}\right)\to {M}\in ℤ$
12 elfzoel2 ${⊢}{K}\in \left({M}..^{N}\right)\to {N}\in ℤ$
13 10 11 12 3jca ${⊢}{K}\in \left({M}..^{N}\right)\to \left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)$
14 elfzo ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}..^{N}\right)↔\left({M}\le {K}\wedge {K}<{N}\right)\right)$
15 13 14 biadanii ${⊢}{K}\in \left({M}..^{N}\right)↔\left(\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}<{N}\right)\right)$
16 3anass ${⊢}\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {K}<{N}\right)↔\left({K}\in {ℤ}_{\ge {M}}\wedge \left({N}\in ℤ\wedge {K}<{N}\right)\right)$
17 9 15 16 3bitr4i ${⊢}{K}\in \left({M}..^{N}\right)↔\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\wedge {K}<{N}\right)$