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