# 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 e. ( 1 ..^ M ) <-> ( N e. NN /\ M e. NN /\ N < M ) )`

### Proof

Step Hyp Ref Expression
1 fzossnn
` |-  ( 1 ..^ M ) C_ NN`
2 1 sseli
` |-  ( N e. ( 1 ..^ M ) -> N e. NN )`
3 elfzouz2
` |-  ( N e. ( 1 ..^ M ) -> M e. ( ZZ>= ` N ) )`
4 eluznn
` |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> M e. NN )`
5 2 3 4 syl2anc
` |-  ( N e. ( 1 ..^ M ) -> M e. NN )`
6 elfzolt2
` |-  ( N e. ( 1 ..^ M ) -> N < M )`
7 2 5 6 3jca
` |-  ( N e. ( 1 ..^ M ) -> ( N e. NN /\ M e. NN /\ N < M ) )`
8 nnuz
` |-  NN = ( ZZ>= ` 1 )`
9 8 eqimssi
` |-  NN C_ ( ZZ>= ` 1 )`
10 9 sseli
` |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )`
11 nnz
` |-  ( M e. NN -> M e. ZZ )`
12 id
` |-  ( N < M -> N < M )`
13 10 11 12 3anim123i
` |-  ( ( N e. NN /\ M e. NN /\ N < M ) -> ( N e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ N < M ) )`
14 elfzo2
` |-  ( N e. ( 1 ..^ M ) <-> ( N e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ N < M ) )`
15 13 14 sylibr
` |-  ( ( N e. NN /\ M e. NN /\ N < M ) -> N e. ( 1 ..^ M ) )`
16 7 15 impbii
` |-  ( N e. ( 1 ..^ M ) <-> ( N e. NN /\ M e. NN /\ N < M ) )`