Theorem fz1fzo0m1

Description: Translation of one between closed and open integer ranges. (Contributed by Thierry Arnoux, 28-Jul-2020)

	Ref	Expression
Assertion	fz1fzo0m1	|- ( M e. ( 1 ... N ) -> ( M - 1 ) e. ( 0 ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		elfzmlbm	|- ( M e. ( 1 ... N ) -> ( M - 1 ) e. ( 0 ... ( N - 1 ) ) )
2		elfzel2	|- ( M e. ( 1 ... N ) -> N e. ZZ )
3		fzoval	|- ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
4	2 3	syl	|- ( M e. ( 1 ... N ) -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
5	1 4	eleqtrrd	|- ( M e. ( 1 ... N ) -> ( M - 1 ) e. ( 0 ..^ N ) )