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

Metamath Proof Explorer

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 )