# Metamath Proof Explorer

## Theorem elfzo1

Description: Membership in a half-open integer range based at 1. (Contributed by Thierry Arnoux, 14-Feb-2017)

Ref Expression
Assertion elfzo1 ${⊢}{N}\in \left(1..^{M}\right)↔\left({N}\in ℕ\wedge {M}\in ℕ\wedge {N}<{M}\right)$

### Proof

Step Hyp Ref Expression
1 fzossnn ${⊢}\left(1..^{M}\right)\subseteq ℕ$
2 1 sseli ${⊢}{N}\in \left(1..^{M}\right)\to {N}\in ℕ$
3 elfzouz2 ${⊢}{N}\in \left(1..^{M}\right)\to {M}\in {ℤ}_{\ge {N}}$
4 eluznn ${⊢}\left({N}\in ℕ\wedge {M}\in {ℤ}_{\ge {N}}\right)\to {M}\in ℕ$
5 2 3 4 syl2anc ${⊢}{N}\in \left(1..^{M}\right)\to {M}\in ℕ$
6 elfzolt2 ${⊢}{N}\in \left(1..^{M}\right)\to {N}<{M}$
7 2 5 6 3jca ${⊢}{N}\in \left(1..^{M}\right)\to \left({N}\in ℕ\wedge {M}\in ℕ\wedge {N}<{M}\right)$
8 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
9 8 eqimssi ${⊢}ℕ\subseteq {ℤ}_{\ge 1}$
10 9 sseli ${⊢}{N}\in ℕ\to {N}\in {ℤ}_{\ge 1}$
11 nnz ${⊢}{M}\in ℕ\to {M}\in ℤ$
12 id ${⊢}{N}<{M}\to {N}<{M}$
13 10 11 12 3anim123i ${⊢}\left({N}\in ℕ\wedge {M}\in ℕ\wedge {N}<{M}\right)\to \left({N}\in {ℤ}_{\ge 1}\wedge {M}\in ℤ\wedge {N}<{M}\right)$
14 elfzo2 ${⊢}{N}\in \left(1..^{M}\right)↔\left({N}\in {ℤ}_{\ge 1}\wedge {M}\in ℤ\wedge {N}<{M}\right)$
15 13 14 sylibr ${⊢}\left({N}\in ℕ\wedge {M}\in ℕ\wedge {N}<{M}\right)\to {N}\in \left(1..^{M}\right)$
16 7 15 impbii ${⊢}{N}\in \left(1..^{M}\right)↔\left({N}\in ℕ\wedge {M}\in ℕ\wedge {N}<{M}\right)$