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)

Ref Expression
Assertion congr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → A mod M = B mod M ↔ ∃ n ∈ ℤ n ⋅ M = A − B

Proof

Step Hyp Ref Expression
1 moddvds ⊢ M ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ → A mod M = B mod M ↔ M ∥ A − B
2 1 3coml ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → A mod M = B mod M ↔ M ∥ A − B
3 simp3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → M ∈ ℕ
4 3 nnzd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → M ∈ ℤ
5 zsubcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A − B ∈ ℤ
6 5 3adant3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → A − B ∈ ℤ
7 divides ⊢ M ∈ ℤ ∧ A − B ∈ ℤ → M ∥ A − B ↔ ∃ n ∈ ℤ n ⋅ M = A − B
8 4 6 7 syl2anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → M ∥ A − B ↔ ∃ n ∈ ℤ n ⋅ M = A − B
9 2 8 bitrd ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ M ∈ ℕ → A mod M = B mod M ↔ ∃ n ∈ ℤ n ⋅ M = A − B