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 
|- ( 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 ) )