Metamath Proof Explorer

Theorem zmodidfzo

Description: Identity law for modulo restricted to integers. (Contributed by AV, 27-Oct-2018)

Ref Expression
Assertion zmodidfzo 
|- ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <-> M e. ( 0 ..^ N ) ) )

Proof

Step Hyp Ref Expression
1 zmodid2 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <-> M e. ( 0 ... ( N - 1 ) ) ) )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 fzoval 
 |-  ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
4 2 3 syl 
 |-  ( N e. NN -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
5 4 adantl 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
6 5 eqcomd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( 0 ... ( N - 1 ) ) = ( 0 ..^ N ) )
7 6 eleq2d 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M e. ( 0 ... ( N - 1 ) ) <-> M e. ( 0 ..^ N ) ) )
8 1 7 bitrd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <-> M e. ( 0 ..^ N ) ) )