Theorem elfzodif0

Description: If an integer M is in an open interval starting at 0 , except 0 , then ( M - 1 ) is also in that interval. (Contributed by Thierry Arnoux, 19-Oct-2025)

	Ref	Expression
Hypotheses	elfzodif0.m	|- ( ph -> M e. ( ( 0 ..^ N ) \ { 0 } ) )
	elfzodif0.n	|- ( ph -> N e. NN0 )
Assertion	elfzodif0	|- ( ph -> ( M - 1 ) e. ( 0 ..^ N ) )

Proof

Step	Hyp	Ref	Expression
1		elfzodif0.m	|- ( ph -> M e. ( ( 0 ..^ N ) \ { 0 } ) )
2		elfzodif0.n	|- ( ph -> N e. NN0 )
3	2	nn0zd	|- ( ph -> N e. ZZ )
4		fzossrbm1	|- ( N e. ZZ -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
5	3 4	syl	|- ( ph -> ( 0 ..^ ( N - 1 ) ) C_ ( 0 ..^ N ) )
6		fzossz	|- ( 0 ..^ N ) C_ ZZ
7	1	eldifad	|- ( ph -> M e. ( 0 ..^ N ) )
8	6 7	sselid	|- ( ph -> M e. ZZ )
9		eldifsni	|- ( M e. ( ( 0 ..^ N ) \ { 0 } ) -> M =/= 0 )
10	1 9	syl	|- ( ph -> M =/= 0 )
11		fzo1fzo0n0	|- ( M e. ( 1 ..^ N ) <-> ( M e. ( 0 ..^ N ) /\ M =/= 0 ) )
12	7 10 11	sylanbrc	|- ( ph -> M e. ( 1 ..^ N ) )
13		elfzom1b	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ( 1 ..^ N ) <-> ( M - 1 ) e. ( 0 ..^ ( N - 1 ) ) ) )
14	13	biimpa	|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ M e. ( 1 ..^ N ) ) -> ( M - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
15	8 3 12 14	syl21anc	|- ( ph -> ( M - 1 ) e. ( 0 ..^ ( N - 1 ) ) )
16	5 15	sseldd	|- ( ph -> ( M - 1 ) e. ( 0 ..^ N ) )