This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )