Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  congr Unicode version

Theorem congr 11770
 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 is congruent to an integer modulo if their difference is a multiple of . See also the definition in [ApostolNT] p. 104: "... is congruent to modulo , and we write (mod ) if divides the difference ", 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.)
Assertion
Ref Expression
congr
Distinct variable groups:   ,   ,   ,

Proof of Theorem congr
StepHypRef Expression
1 moddvds 11491 . . 3
213coml 1188 . 2
3 simp3 983 . . . 4
43nnzd 9165 . . 3
5 zsubcl 9088 . . . 4