Theorem dvdsmod0

Description: If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022)

	Ref	Expression
Assertion	dvdsmod0	|- ( ( M e. NN /\ M || N ) -> ( N mod M ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		dvdszrcl	|- ( M || N -> ( M e. ZZ /\ N e. ZZ ) )
2	1	adantl	|- ( ( M e. NN /\ M || N ) -> ( M e. ZZ /\ N e. ZZ ) )
3		dvdsval3	|- ( ( M e. NN /\ N e. ZZ ) -> ( M || N <-> ( N mod M ) = 0 ) )
4	3	biimpd	|- ( ( M e. NN /\ N e. ZZ ) -> ( M || N -> ( N mod M ) = 0 ) )
5	4	expcom	|- ( N e. ZZ -> ( M e. NN -> ( M || N -> ( N mod M ) = 0 ) ) )
6	5	impd	|- ( N e. ZZ -> ( ( M e. NN /\ M || N ) -> ( N mod M ) = 0 ) )
7	6	adantl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M e. NN /\ M || N ) -> ( N mod M ) = 0 ) )
8	2 7	mpcom	|- ( ( M e. NN /\ M || N ) -> ( N mod M ) = 0 )