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	⊢ ( 𝜑 → 𝑀 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 0 } ) )
	elfzodif0.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	elfzodif0	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ( 0 ..^ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzodif0.m	⊢ ( 𝜑 → 𝑀 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 0 } ) )
2		elfzodif0.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3	2	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4		fzossrbm1	⊢ ( 𝑁 ∈ ℤ → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
5	3 4	syl	⊢ ( 𝜑 → ( 0 ..^ ( 𝑁 − 1 ) ) ⊆ ( 0 ..^ 𝑁 ) )
6		fzossz	⊢ ( 0 ..^ 𝑁 ) ⊆ ℤ
7	1	eldifad	⊢ ( 𝜑 → 𝑀 ∈ ( 0 ..^ 𝑁 ) )
8	6 7	sselid	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9		eldifsni	⊢ ( 𝑀 ∈ ( ( 0 ..^ 𝑁 ) ∖ { 0 } ) → 𝑀 ≠ 0 )
10	1 9	syl	⊢ ( 𝜑 → 𝑀 ≠ 0 )
11		fzo1fzo0n0	⊢ ( 𝑀 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑀 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑀 ≠ 0 ) )
12	7 10 11	sylanbrc	⊢ ( 𝜑 → 𝑀 ∈ ( 1 ..^ 𝑁 ) )
13		elfzom1b	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ( 1 ..^ 𝑁 ) ↔ ( 𝑀 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) ) )
14	13	biimpa	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ∈ ( 1 ..^ 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
15	8 3 12 14	syl21anc	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ( 0 ..^ ( 𝑁 − 1 ) ) )
16	5 15	sseldd	⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ( 0 ..^ 𝑁 ) )