Theorem elfzlble

Description: Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018)

	Ref	Expression
Assertion	elfzlble	|- ( ( N e. ZZ /\ M e. NN0 ) -> N e. ( ( N - M ) ... N ) )

Proof

Step	Hyp	Ref	Expression
1		nn0z	|- ( M e. NN0 -> M e. ZZ )
2		zsubcl	|- ( ( N e. ZZ /\ M e. ZZ ) -> ( N - M ) e. ZZ )
3	1 2	sylan2	|- ( ( N e. ZZ /\ M e. NN0 ) -> ( N - M ) e. ZZ )
4		simpl	|- ( ( N e. ZZ /\ M e. NN0 ) -> N e. ZZ )
5		nn0ge0	|- ( M e. NN0 -> 0 <_ M )
6	5	adantl	|- ( ( N e. ZZ /\ M e. NN0 ) -> 0 <_ M )
7		zre	|- ( N e. ZZ -> N e. RR )
8		nn0re	|- ( M e. NN0 -> M e. RR )
9		subge02	|- ( ( N e. RR /\ M e. RR ) -> ( 0 <_ M <-> ( N - M ) <_ N ) )
10	7 8 9	syl2an	|- ( ( N e. ZZ /\ M e. NN0 ) -> ( 0 <_ M <-> ( N - M ) <_ N ) )
11	6 10	mpbid	|- ( ( N e. ZZ /\ M e. NN0 ) -> ( N - M ) <_ N )
12		eluz2	|- ( N e. ( ZZ>= ` ( N - M ) ) <-> ( ( N - M ) e. ZZ /\ N e. ZZ /\ ( N - M ) <_ N ) )
13	3 4 11 12	syl3anbrc	|- ( ( N e. ZZ /\ M e. NN0 ) -> N e. ( ZZ>= ` ( N - M ) ) )
14		eluzfz2	|- ( N e. ( ZZ>= ` ( N - M ) ) -> N e. ( ( N - M ) ... N ) )
15	13 14	syl	|- ( ( N e. ZZ /\ M e. NN0 ) -> N e. ( ( N - M ) ... N ) )