Theorem elfzm12

Description: Membership in a curtailed finite sequence of integers. (Contributed by Paul Chapman, 17-Nov-2012)

	Ref	Expression
Assertion	elfzm12	|- ( N e. NN -> ( M e. ( 1 ... ( N - 1 ) ) -> M e. ( 1 ... N ) ) )

Proof

Step	Hyp	Ref	Expression
1		nnz	|- ( N e. NN -> N e. ZZ )
2		zre	|- ( N e. ZZ -> N e. RR )
3	2	lem1d	|- ( N e. ZZ -> ( N - 1 ) <_ N )
4		peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
5		eluz	|- ( ( ( N - 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( N - 1 ) ) <-> ( N - 1 ) <_ N ) )
6	4 5	mpancom	|- ( N e. ZZ -> ( N e. ( ZZ>= ` ( N - 1 ) ) <-> ( N - 1 ) <_ N ) )
7	3 6	mpbird	|- ( N e. ZZ -> N e. ( ZZ>= ` ( N - 1 ) ) )
8		fzss2	|- ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
9	1 7 8	3syl	|- ( N e. NN -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
10	9	sseld	|- ( N e. NN -> ( M e. ( 1 ... ( N - 1 ) ) -> M e. ( 1 ... N ) ) )