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 )