Metamath Proof Explorer

Theorem congr

Description: Definition of congruence by integer multiple (see ProofWiki "Congruence (Number Theory)", 11-Jul-2021, https://proofwiki.org/wiki/Definition:Congruence_(Number_Theory) ): An integer A is congruent to an integer B modulo M if their difference is a multiple of M . See also the definition in ApostolNT p. 104: "... a is congruent to b modulo m , and we write a == b (mod m ) if m divides the difference a - b ", or Wikipedia "Modular arithmetic - Congruence", https://en.wikipedia.org/wiki/Modular_arithmetic#Congruence , 11-Jul-2021,: "Given an integer n > 1, called a modulus, two integers are said to be congruent modulo n, if n is a divisor of their difference (i.e., if there is an integer k such that a-b = kn)". (Contributed by AV, 11-Jul-2021)

|- ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> ( ( A mod M ) = ( B mod M ) <-> E. n e. ZZ ( n x. M ) = ( A - B ) ) )

 |-  ( ( M e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( ( A mod M ) = ( B mod M ) <-> M || ( A - B ) ) )

 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> ( ( A mod M ) = ( B mod M ) <-> M || ( A - B ) ) )

 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> M e. NN )

 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> M e. ZZ )

 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A - B ) e. ZZ )

 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> ( A - B ) e. ZZ )

 |-  ( ( M e. ZZ /\ ( A - B ) e. ZZ ) -> ( M || ( A - B ) <-> E. n e. ZZ ( n x. M ) = ( A - B ) ) )

 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> ( M || ( A - B ) <-> E. n e. ZZ ( n x. M ) = ( A - B ) ) )

 |-  ( ( A e. ZZ /\ B e. ZZ /\ M e. NN ) -> ( ( A mod M ) = ( B mod M ) <-> E. n e. ZZ ( n x. M ) = ( A - B ) ) )