This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑀 ∈ ( ( 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 ..^ 𝑁 ) )