Metamath Proof Explorer

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 ⊢ φ → M ∈ 0 ..^ N ∖ 0
elfzodif0.n ⊢ φ → N ∈ ℕ 0
Assertion elfzodif0 ⊢ φ → M − 1 ∈ 0 ..^ N

Proof

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