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

Metamath Proof Explorer

Theorem zmodidfzoimp

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

Ref Expression
Assertion zmodidfzoimp 
|- ( M e. ( 0 ..^ N ) -> ( M mod N ) = M )

Proof

Step Hyp Ref Expression
1 elfzo0 
 |-  ( M e. ( 0 ..^ N ) <-> ( M e. NN0 /\ N e. NN /\ M < N ) )
2 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
3 2 anim1i 
 |-  ( ( M e. NN0 /\ N e. NN ) -> ( M e. ZZ /\ N e. NN ) )
4 3 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN /\ M < N ) -> ( M e. ZZ /\ N e. NN ) )
5 1 4 sylbi 
 |-  ( M e. ( 0 ..^ N ) -> ( M e. ZZ /\ N e. NN ) )
6 zmodidfzo 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( ( M mod N ) = M <-> M e. ( 0 ..^ N ) ) )
7 6 biimprd 
 |-  ( ( M e. ZZ /\ N e. NN ) -> ( M e. ( 0 ..^ N ) -> ( M mod N ) = M ) )
8 5 7 mpcom 
 |-  ( M e. ( 0 ..^ N ) -> ( M mod N ) = M )