Theorem uzsubfz0

Description: Membership of an integer greater than L decreased by L in a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 16-Sep-2018)

	Ref	Expression
Assertion	uzsubfz0	|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> ( N - L ) e. ( 0 ... N ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> L e. NN0 )
2		eluznn0	|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> N e. NN0 )
3		eluzle	|- ( N e. ( ZZ>= ` L ) -> L <_ N )
4	3	adantl	|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> L <_ N )
5		elfz2nn0	|- ( L e. ( 0 ... N ) <-> ( L e. NN0 /\ N e. NN0 /\ L <_ N ) )
6	1 2 4 5	syl3anbrc	|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> L e. ( 0 ... N ) )
7		fznn0sub2	|- ( L e. ( 0 ... N ) -> ( N - L ) e. ( 0 ... N ) )
8	6 7	syl	|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> ( N - L ) e. ( 0 ... N ) )